The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Peter Hawkins wrote:
> 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.

I'm not aware of any automatic workaround.  'induction' generalizes all 
arguments as variables, dropping any information about structure.  The 
standard fix is to first prove a lemma whose statement gives those 
hypotheses explicitly.