coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club]How do I prove this simple fact?, Aaron Bohannon
- Re: [Coq-Club]How do I prove this simple fact?, Adam Chlipala
- Re: [Coq-Club]How do I prove this simple fact?, Andrew McCreight
- Re: [Coq-Club]How do I prove this simple fact?, Thery Laurent
- Re: [Coq-Club]How do I prove this simple fact?, jean-francois . monin
- [Coq-Club]Re: How do I prove this simple fact?,
Aaron Bohannon
- Re: [Coq-Club]Re: How do I prove this simple fact?,
Pierre Casteran
- Re: [Coq-Club]Re: How do I prove this simple fact?, Pierre Casteran
- Re: [Coq-Club]Re: How do I prove this simple fact?, jean-francois . monin
- Re: [Coq-Club]Re: How do I prove this simple fact?, Thery Laurent
- Re: [Coq-Club]Re: How do I prove this simple fact?,
Pierre Casteran
Archive powered by MhonArc 2.6.16.