The Coq mailing list

[jean-francois.monin AT imag.fr]

You still have a direct proof along the lines given yesterday:
just remark that m = m+p-p.

Note you can easily cook the tactic I asked for yesterday,
at least for a fixed number of rewritings (2 in the present case).

(* converts l1 to r1 and l2 to r2 *)
Ltac convert2 l1 r1 l2 r2 :=
  pattern l1, l2;
  match goal with [|- ?g ?x ?y] => change (g r1 r2) end;
  cbv beta.

Then the solution (using omega for instance).

Lemma bar : forall n m p, foo (n, m + p) -> m <= n.
Proof.
  intros n m p H.
  replace m with (m+p-p); [idtac | omega].
  convert2 n (fst(n, m+p)) (m+p) (snd(n, m+p)).
  induction H; simpl in *|-*; omega.
Qed.


  JF


Aaron Bohannon a ecrit :
 > On 11/8/06, Aaron Bohannon 
 > <bohannon AT cis.upenn.edu>
 >  wrote:
 > > 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.
 > 
 > 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.
 > 
 > Am I correct in assuming that I need to take one of the longer
 > approaches when dealing with a lemma like this?
 > 
 > -Aaron