The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

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