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]Re: How do I prove this simple fact?
- Date: Thu, 9 Nov 2006 11:53:16 +0100 (CET)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Thanks for the helpful responses. I find the use of the "change"
tactic especially elegant. However, it does not seem applicaple to
the slightly more general case where I would like to prove:
Lemma bar : forall n m p, foo (n, m + p) -> m <= n.
Just to second jean-francois answer the problem is that you do induction on a term that does not contains only variables (there is a pair and a sum in (n, m+p)). The first way to go is to reshape your hypothesis on which you do induction so it contains only variables.
Example:
Require Import 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 p, foo (n, m + p) -> m <= n.
intros n m p H.
assert (Haux: forall u, foo u -> forall p, u = (n, m + p) -> m <= n).
intros u Hu; elim Hu; intros i j k.
intros Eq1 p1 Eq2; injection Eq2; intros; omega.
intros _ Hrec p1 Eq2; apply Hrec with (p1 + k).
apply f_equal2 with (f := @pair nat nat); injection Eq2; intros; omega.
apply Haux with (1 := H) (p := p); trivial.
Qed.
The second way to go is to reshape your conclusion so it explicitly
exhibits the dependancy with the term that is not a variable
in your case (n, m + p). Example:
Lemma bar1 : forall n m p, foo (n, m + p) -> m <= n.
intros n m p H.
replace m with ((m + p) - p); try omega.
change ((fun x => (snd x - p <= fst x)) (n, m + p)).
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.