The Coq mailing list

[Jean-Francois Monin <Jean-Francois.Monin AT imag.fr>]

There is a big difference between AA1 end AA2 : only AA1
requires the decidability of equality (on nat).
Here is an elementary proof of a generalization of AA2.

Variable A : Set

Lemma AA2: forall (s s1 o o1 x x1:A),
           (s<>s1)\/(o<>o1)\/(x<>x1) -> (s,o,x)<>(s1,o1,x1).
Proof.
intros s s1 o o1 x x1 [diff | [diff |diff ]] eq.
  apply diff. change (fst (fst (s, o, x)) = s1). rewrite eq. reflexivity.
  apply diff. change (snd (fst (s, o, x)) = o1). rewrite eq. reflexivity.
  apply diff. change (snd (s, o, x) = x1). rewrite eq. reflexivity.
Qed.

An alternative to "change + rewrite + reflexivity" is to use injection
or even congruence, at once :

Proof.
  intros s s1 o o1 x x1 [diff | [diff |diff ]] eq; congruence.
Qed.


  JF


On Tue, Nov 27, 2007 at 10:57:41AM +0000, Edsko de Vries wrote:
> On Tue, Nov 27, 2007 at 02:20:03PM +0800, 
> judy AT mail.ccnu.edu.cn
>  wrote:
> > Dear Professor:
> > 
> > how to prove:
> > 
> > 
> > Lemma AA1:forall (s s1 o o1 x x1:nat),
> > (s,o,x)<>(s1,o1,x1)->(s<>s1)\/(o<>o1)\/(x<>x1).
> 
> One possibility is to use case analysis on whether s = s1, o = o1, x = x1:
> 
> Lemma AA1:forall (s s1 o o1 x x1:nat),
> (s,o,x)<>(s1,o1,x1)->(s<>s1)\/(o<>o1)\/(x<>x1).
> Proof.
>   intros.
>   elim (eq_nat_dec s s1) ; elim (eq_nat_dec o o1) ; elim (eq_nat_dec x x1) 
> ; auto.
>   intros.
>   subst x1 o1 s1.
>   apply False_ind ; apply H ; reflexivity.
> Qed.
> 
> The 'auto' tactic solves the goal in all but one case (the case where s = 
> s1, o
> = o1 and x = x1); in that case, there is a contradiction amongst the 
> hypothesis
> and we can finish the proof using False_ind.
> 
> The other lemma can probably be solved using a similar technique.
> 
> Edsko
> 

-- 
Jean-Francois Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46