The Coq mailing list

["Peter Hawkins" <hawkinsp AT cs.stanford.edu>]

Hi...

Suppose I have the following inductive type:
Inductive foo: (nat * nat) -> (nat * nat) -> Prop :=
 | foo_refl: forall s, foo s s
 | foo_trans: forall a1 b1 a2 b2 s3,
    (a2 = 2*a1)%nat -> (b2 = 3*b1)%nat -> foo (a2,b2) s3 .
    foo (a1,b1) s3.

Suppose I want to prove the first argument is non-decreasing. Here is
a proof that works:
Lemma foo_lem: forall s1 s2, foo s1 s2 -> (fst s1 <= fst s2)%nat.
Proof.
 induction 1; simpl in * |- *; omega.
Qed.

However, this seemingly identical statement is cannot be proved using
those tactics:
Lemma foo_lem2: forall a1 b1 a2 b2, foo (a1,b1) (a2,b2) .
 (a1 <= a2)%nat.
Proof.
 induction 1.

At this stage I have this goal:
2 subgoals

 a1 : nat
 b1 : nat
 a2 : nat
 b2 : nat
 s : nat * nat
 ============================
  (a1 <= a2)%nat

which obviously cannot be proved.

It seems the induction tactic didn't generate the hypotheses (s =
(a1,b1)) and (s = (a2,b2)). What's happening here, and how can I fix
it? I'm using Coq 8.1gamma.

Thanks,
Peter