Skip to Content.
Sympa Menu

coq-club - [Coq-Club]How do I prove this simple fact?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]How do I prove this simple fact?


chronological Thread 
  • From: "Aaron Bohannon" <bohannon AT cis.upenn.edu>
  • To: "Coq List" <coq-club AT pauillac.inria.fr>
  • Subject: [Coq-Club]How do I prove this simple fact?
  • Date: Wed, 8 Nov 2006 12:17:40 -0500
  • Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:sender:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition:x-google-sender-auth; b=njaMe1LHStNt+IS9lvrwXymgJn8m7sxlfCz3/bleAPOm1kBYczfQ78dzdmoYgouM1EKBQpSBmlU06lpBPx+VSEVaacryRjP4aMwzkUfA1rngOHSVV3/u2/o0B87eHOMN7cTAVnqerUI7B8JudO15D2TlgcTsewgvuceNYW+NiOU=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page