The Coq mailing list

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

Hi, Aaron,

In fact, induction is not necessary. Once you have proved your first 
version of bar, the second version
follows immediately.

Pierre



Lemma bar : forall n p, foo (n, p) -> p <= n.
(* same as before *)

Hint Resolve bar.
Hint Constructors foo.

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

Pierre



Pierre Casteran wrote:

> (************************************)
>
> 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
>
>
>
> --------------------------------------------------------
> 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