The Coq mailing list

[Andrew McCreight <andrew.mccreight AT yale.edu>]

The way I prove things like this is to make sure that all of the arguments 
to the thing I'm inducting on are "simple" and not compound, so Coq 
doesn't forget that the argument of the structure I'm inducting on.

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).


Require Omega.


Lemma bar : forall n m, foo (n, m) -> m <= n.
Proof.
  intros n m F.
  assert (exists x, x = (n, m)).
  econstructor; reflexivity.
  destruct H as [x R]; rewrite <- R in F.
  generalize dependent m.
  induction F; intros m R; injection R; clear R.

  omega.

  intros; subst i j.
  assert (m + k <= n).
  apply IHF; reflexivity.
  omega.

Qed.


On Wed, 8 Nov 2006, Aaron Bohannon wrote:

> 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
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club