The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

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.