The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Aaron Bohannon wrote:

> 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.
For proving this new version of "bar", (which I renamed "bar3")  you can do
an induction on p, and use the preceding "bar".

Cheers,
Pierre


(************************************)

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 Import Arith.

Lemma bar1 : forall z, foo z -> snd z <= fst z.
Proof.
induction 1;simpl.
subst i;auto with arith.
simpl in *.
eapply le_trans;eauto with arith.
Qed.

Lemma bar : forall n p, foo (n, p) -> p <= n.
Proof.
intros n p; generalize (bar1 (n,p)).
simpl;auto.
Qed.

Hint Resolve bar.
Hint Constructors foo.

Lemma bar3 : forall n m p, foo (n, m + p) -> m <= n.
Proof.
induction p.
rewrite plus_0_r;eauto.
eauto.
Qed.








> Am I correct in assuming that I need to take one of the longer
> approaches when dealing with a lemma like this?
>
> -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