# PatternMatching

See the official user manual for the most up-to-date version of the information on this page.

TODO

## `with` patterns

See section on "the with construct" in Ulf's tutorial http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

## `rewrite`

If eqn : a ≡ b, where _≡_ is the builtin equality you can write

```  f ps rewrite eqn = rhs
```

```  f ps with a | eqn
... | ._ | refl = rhs
```

The rewrite construct has the effect of rewriting the goal and the context by the given equation (left to right).

You can rewrite using several equations (in sequence) by separating them with vertical bars (|):

```  f ps rewrite eqn₁ | eqn₂ | � = rhs
```

It is also possible to add with clauses after rewriting:

```  f ps rewrite eqns with e
... | p = rhs
```

Note that pattern matching happens before rewriting�if you want to rewrite and then do pattern matching you can use a with after the rewrite.

TODO: cannot rewrite with looping rewrites, because works by unification.

TODO

## Reduction behavior

Consider the following two implementations of the less than function on natural numbers.

```  data Bool : Set where
true  : Bool
false : Bool

data Nat : Set where
zero : Nat
suc  : Nat -> Nat

-- First implementation
_<1_ : Nat -> Nat -> Bool
zero  <1 suc m = true
suc n <1 suc m = n <1 m
_     <1 zero  = false

-- Second implementation
_<2_ : Nat -> Nat -> Bool
_     <2 zero  = false
zero  <2 suc m = true
suc n <2 suc m = n <2 m
```

Perhaps surprisingly (since the two implementations have the same non-overlapping clauses), _<1_ and _<2_ does not have the same reduction behaviour. For neutral `n` we have that `n <1 zero` does not reduce, whereas `n <2 zero` reduces to `false`. The reason for this is explained below.

### Case tree equivalence

The set of defining equations for a functions are equivalent to a case tree, and the order of the equations determines which one. For `_<1_` the equivalent case tree is

```n <1 m = case n of
zero  -> case m of
suc m -> true
zero  -> false
suc n -> case m of
suc m -> n < m
zero  -> false
```

whereas for _<2_ it's

```n <2 m = case m of
zero  -> false
suc m -> case n of
zero  -> true
suc n -> n <2 m
```

Looking at the case tree it's clear that in the first case `n < zero` will not reduce to `false` for neutral `n`, but in the second case it will. Pattern matching always starts with the left-most constructor pattern in the first clause. For `_<1_` this is the first argument, whereas for `_<2_` it's the second argument.

### Operational view

An alternative more operational way of looking at what's going on is the following. When reducing an application of a function by pattern matching the clauses will be tried one at a time, from top to bottom. For each clause the arguments will be matched against the corresponding patterns from left to right. If there is a mismatch the next clause is tried. If there is an inconclusive match (e.g. matching a neutral term against a constructor pattern) the application won't reduce. For `_<1_` we can't see whether `n` matches `zero` or not, so the reduction is suspended.

### Berry's majority function

The reason for suspending reduction at the first sign of inconclusive matching is to keep the correspondence to a case tree. Consider Berry's majority function:

```data Bool : Set where
tt : Bool
ff : Bool

maj tt tt tt = tt
maj tt ff x  = x
maj ff x  tt = x
maj x  tt ff = x
maj ff ff ff = ff
```

Here, all clauses are disjoint, but there is no case tree which delivers all equations as definitional equalities. Following the rules for pattern matching given above you'll discover that with this definition you get all but `maj x tt ff = x`.