The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

There are several things here. Inversion doesn't do induction, and since you need an induction here (because of case c4 and c5), you need to change the statement a little. Indeed induction doesn't work well with non-variable indices. A first try would be

forall n m p x, n=0 -> m=0 -> p=S x -> R n m p -> False

Which is obviously equivalent to the statement you want to prove, but more compatible with induction. It's too weak though, and you won't be able to pass case c4. So you need to strengthen your induction hypothesis. I suggest

forall n m p x, p = S (n+m+x) -> R n m p -> False

And here is the full proof:

Theorem nullsum: forall x, R 0 0 (S x) -> False.
 assert (forall n m p x, p = S (n+m+x) -> R n m p -> False) as nullsum.
 { intros * hp h.
   induction h as [ | n m p h hh | n m p h hh | n m p h hh | n m p h hh ].
   + discriminate hp.
   + injection hp.
     auto.
   + injection hp.
     rewrite <- plus_n_Sm.
     auto.
   + apply hh. simpl.
     rewrite <- plus_n_Sm. simpl.
     rewrite hp.
     reflexivity.
   + rewrite (Plus.plus_comm m n) in hp.
     auto. }
 exact (fun x => nullsum 0 0 (S x) x (eq_refl (S x))).
Qed.

On 13 December 2013 13:54, Christopher Ernest Sally <christopherernestsally AT gmail.com> wrote:

Hi all

say we have a Inductive proposition, R ( yes, this is from sf, but the example is self contained.

Inductive R : nat -> nat -> nat -> Prop :=

| c1 : R 0 0 0

| c2 : forall m n o, R m n o -> R (S m) n (S o)

| c3 : forall m n o, R m n o -> R m (S n) (S o)

| c4 : forall m n o, R (S m) (S n) (S (S o)) -> R m n o

| c5 : forall m n o, R m n o -> R n m o.

Intuitively, we can see that R a b c iff a + b =c and indeed we can show this. (below)

However, How can I (or why can't I) show

Theorem nullsum: forall x, R 0 0 (S x) -> False.

without reflecting R into +. (i.e without using Rspec (below))

Thanks

Best
Chris

Lemma Rspec : forall x y z, R x y z -> x + y = z.

Proof with auto.

  intros.

  induction H.

  - simpl.

  - rewrite <- plus_n_Sm. apply f_equal...

  - rewrite <- plus_n_Sm in IHR. inversion IHR...

  - rewrite plus_comm...

Qed.

Lemma Rspeci : forall x y z, x + y = z -> R x y z.

Proof with auto.

 intros.

  destruct H.

  induction x, y; simpl; try constructor...

Qed.

Theorem nullsum: forall x, R 0 0 (S x) -> False.

Proof with auto.

  do 2 intro.

  inversion H.

  generalize (rspec 0 0 (S x) H); simpl; intro.

  inversion H0.

Qed.