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.1For 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 ofCoq < 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) ofCoq < (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 < endCoq < end.Warning: the variable M starts with upper case in a pattern
Warning: the variable N starts with upper case in a pattern
dec is recursively defined
In general, consider the terms e1... en, where the type of ei is an instance of a family type [vec(di):vec(Di)]Ti (1£ i £ n). Then to write < P>Cases e1... en of ...end, the elimination predicate P should be of the form: [vec(d1):vec(D1)][x1:T1]... [vec(dn):vec(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.