The Coq mailing list

[jean-francois.monin AT imag.fr]

Proofs of inductive properties are finite.

Here is a somewhat generic strategy coping with exchanges.

Definition exch P  := fun (n m: nat) =>  P n m \/ P m n.

Inductive Bar : nat -> nat -> Prop := Bar_intro : Bar 0 1.

Lemma fool : forall n m p, Foo n m p -> exch Bar n m.
  induction 1 as [|m n p F E].
    left; constructor.
    case E; unfold exch; auto.
Qed.

Lemma not_Foo : ~ (Foo 1 2 3).
intro F; generalize (fool _ _ _ F); clear F.
intro E; case E; clear E; intro B.
  inversion B.
  inversion B.
Qed.


Hope this helps,
  JF

-- 
Jean-François 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

Edsko de Vries a ecrit :
 > Hi,
 > 
 > Sorry for replying to my own message, but here is a simplified (but
 > self-contained) example of what I'm trying to do:
 > 
 >      Inductive Foo : nat -> nat -> nat -> Prop :=
 >        | FooBase : Foo 0 1 2
 >        | FooExchange : forall (m n o:nat), Foo m n o -> Foo n m o.
 >      
 >      Lemma not_Foo : ~ (Foo 1 2 3).
 >      Proof.
 >      unfold not ; intros.
 > 
 > At this point, we get
 > 
 >      1 subgoal
 >      H : Foo 1 2 3
 >      ______________________________________(1/1)
 >      False
 > 
 > now when I do "inversion H; subst", we get
 > 
 >      1 subgoal
 >      H : Foo 1 2 3
 >      H0 : Foo 2 1 3
 >      ______________________________________(1/1)
 >      False
 > 
 > Now of course we can repeat this step as often we want, without getting any
 > further. How do I finish this proof?
 > 
 > Thank again,
 > 
 > Edsko