13.4 Using pattern matching to write proofs
In all the previous examples the elimination predicate does not depend
on the object(s) matched. The typical case where this is not possible
is when we write a proof by induction or a function that yields an
object of dependent type. An example of proof using Cases in
given in section 8.1
For example, we can write
the function buildlist that given a natural number
n builds a list length n containing zeros as follows:
Coq < Fixpoint buildlist [n:nat] : (listn n) :=
Coq < <[n:nat](listn n)>Cases n of
Coq < O => niln
Coq < | (S n) => (consn n O (buildlist n))
Coq < end.
buildlist is recursively defined
We can also use multiple patterns whenever the elimination predicate has
the correct arity.
Consider the following definition of the predicate less-equal
Le:
Coq < Inductive LE : nat->nat->Prop :=
Coq < LEO: (n:nat)(LE O n)
Coq < | LES: (n,m:nat)(LE n m) -> (LE (S n) (S m)).
LE_ind is defined
LE is defined
We can use multiple patterns to write the proof of the lemma
(n,m:nat) (LE n m)(LE m n):
Coq < Fixpoint dec [n:nat] : (m:nat)(LE n m) \/ (LE m n) :=
Coq < [m:nat] <[n,m:nat](LE n m) \/ (LE m n)>Cases n m of
Coq < O x => (or_introl ? (LE x O) (LEO x))
Coq < | x O => (or_intror (LE x O) ? (LEO x))
Coq < | ((S n) as N) ((S m) as M) =>
Coq < Cases (dec n m) of
Coq < (or_introl h) => (or_introl ? (LE M N) (LES n m h))
Coq < | (or_intror h) => (or_intror (LE N M) ? (LES m n h))
Coq < end
Coq < end.
Warning: the variable(s) N M start(s) with upper case in a pattern
dec is recursively defined
In the example of dec the elimination predicate is binary
because we destructure two arguments of nat that is a
non-dependent type. Note the first Cases is dependent while the
second is not.
In general, consider the terms e1... en,
where the type of ei is an instance of a family type
[di:Di]Ti (1£ i
£ n). Then to write < P>Cases e1...
en of ...end, the
elimination predicate P should be of the form:
[d1:D1][x1:T1]... [dn:Dn][xn:Tn]Q.
The user can also use Cases in combination with the tactic
Refine (see section 7.2.2) to build incomplete proofs
beginning with a Cases construction.