coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Thery Laurent <thery AT ns.di.univaq.it>
- To: Aaron Bohannon <bohannon AT cis.upenn.edu>
- Cc: Coq List <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club]How do I prove this simple fact?
- Date: Wed, 8 Nov 2006 19:02:35 +0100 (CET)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
the problem comes from the fact that you are using pairing.
You then need to tell Coq explicitly that
m <= n is the same than (fun p => snd p <= fst p) (n,m)
so that induction proceeds as expected:
Here it goes:
Require Omega.
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.
intros n m H; change ((fun p => snd p <= fst p) (n,m)).
elim H; simpl; intros; omega.
Qed.
--
Laurent
- [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.