The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On 20 mai 2005, Pierre Casteran wrote:

> Selon Serge Leblanc 
> <serge.leblanc AT wanadoo.fr>:
> 
> > I am trying to prove the the following trivial goal. I don't reach it,
> > can you show me how to make?
> >
> > Goal forall n m:Z, Zmin n m = Zmin m n.

> 
> Hi,
> 
>  There is a solution (attached) (with some non-trivial feature : the
> caseEq tactic)
> Perhaps one can give a simpler solution ???

Hi,

You can use " functional induction Zmin z z' " in place of " caseEq (z ?=
z')%Z. ". When you want to consider the different branches of a
pattern matching (and induction) inside a function, functional induction
(and Functional Scheme) is useful:


Require Export ZArith.
Transparent Zmin.
Open Scope Z_scope.

Lemma Zcompare_Gt_Lt : forall z z', (z ?= z')= Gt -> (z' ?= z)= Lt.
Proof.
 intros z z'; case (Zcompare_Gt_Lt_antisym z z');auto.
Qed.

Lemma Zcompare_Lt_Gt : forall z z', (z ?= z')= Lt -> (z' ?= z)= Gt.
Proof.
 intros z z'; case (Zcompare_Gt_Lt_antisym z' z);auto.
Qed.

Goal forall z z', Zmin z z' = Zmin z' z. 
  intros z z';unfold Zmin.
  functional induction Zmin z z'.  (* does the same as caseEq here *)
  rewrite (Zcompare_Eq_eq _ _ H_eq_).
  case (z' ?= z')%Z;auto.
  rewrite (Zcompare_Lt_Gt _ _ H_eq_);auto.
  rewrite (Zcompare_Gt_Lt _ _ H_eq_);auto.
Save.