13.4 Using pattern matching to write proofs
In all the previous examples the elimination predicate does not depend
on the object(s) matched. But it may depend and the typical case
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 of 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 is defined
LE_ind 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.
dec is recursively defined
In the example of dec the elimination predicate is binary
because we destructure two arguments of nat which is a
non-dependent type. Notice that 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, in expression < 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.