The Coq mailing list

[jean-francois.monin AT imag.fr]

Hello,

You can actually use your own script with a small and natural
change.  The point is that induction is carried out over (n,m);
then just replace, in your goal, occurrences of n (and of m) by
appropriate functions of (n,m).

Lemma bar : forall n m, foo (n, m) -> m <= n.
Proof.
  intros n m H.
  change (snd (n,m) <= fst (n,m)).  (* 2 *)
  induction H; simpl in *|-*.
  rewrite H; auto with arith.
  eauto with arith.
Qed.

PS. Wish to the attention of the Coq development team.
We still lack a conversion tactic similar to "replace... with..."
I would prefer to express line (* 2 *) above in the following
way:
  convert n to (fst (n,m)) and m to (fst (n,m)).  (* 2' *)
(Note that simultaneous conversion is needed, hence the "and")

I very often need this, and claim that most uses of "change" (if
not all) can be advantageously be replaced by convert: "change"
is bad for the robustness of scripts.  Using "replace... with..." 
is robust but not satisfactory for 2 reasons at least:
  - no parallel replace is available;
  - equality is heavier than conversion.

Cheers, 
  JF


Aaron Bohannon a ecrit :
 > 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.
 > 
 > However, I have not found any way to make the induction work.  I run
 > into different problems depending on what I try, and all of my
 > attempts have looked rather ugly.  So I am wondering what the "right"
 > way to prove this is.
 > 
 > Of course, it is trivial proof if we use the "curried" form of the 
 > definition:
 > 
 > 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.
 > Proof.
 >   intros n m H.
 >   induction H.
 >   rewrite H; auto with arith.
 >   eauto with arith.
 > Qed.
 > 
 > But, for the sake of argument, let's say that I can't or don't want to
 > write the definition in that way.
 > 
 > Thanks in advance for any help.
 > 
 > -Aaron

Thery Laurent a ecrit :
 > 
 > 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