The Coq mailing list

["Aaron Bohannon" <bohannon AT cis.upenn.edu>]

Given the simple inductive definition here, I would like to prove the
simple lemma below it.

Inductive foo : nat * nat -> Prop :=
| foo1 : forall i j k, i = j + k -> foo (i, j)
| foo2 : forall i j k, foo (i, j + k) -> foo (i, j).

Lemma bar : forall n m, foo (n, m) -> m <= n.

However, I have not found any way to make the induction work.  I run
into different problems depending on what I try, and all of my
attempts have looked rather ugly.  So I am wondering what the "right"
way to prove this is.

Of course, it is trivial proof if we use the "curried" form of the definition:

Inductive foo : nat -> nat -> Prop :=
| foo1 : forall i j k, i = j + k -> foo i j
| foo2 : forall i j k, foo i (j + k) -> foo i j.

Lemma bar : forall n m, foo n m -> m <= n.
Proof.
 intros n m H.
 induction H.
 rewrite H; auto with arith.
 eauto with arith.
Qed.

But, for the sake of argument, let's say that I can't or don't want to
write the definition in that way.

Thanks in advance for any help.

-Aaron