The Coq mailing list

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

Aaron Bohannon 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.

You have here a classic problem resulting from the 'induction' tactic's 
excessive optimism.  It drops all facts about the structure of the 
arguments to the inductive type whose derivations you want to induct 
over.  Instead, it perhaps should fail or at least raise a warning when 
the inductee has some argument that isn't a variable.  Here's an 
instantiation of the standard workaround:

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).

Ltac injecter :=
  match goal with
    | [ H : (_, _) = (_, _) |- _ ] =>
      injection H; clear H; intros; subst
  end.

Lemma bar' : forall nm, foo nm
  -> forall n m, nm = (n, m)
    -> m <= n.
  induction 1; intuition; injecter; subst;
    eauto with arith.
Qed.

Lemma bar : forall n m, foo (n, m)
  -> m <= n.
  intros.
  eapply bar'; eauto.
Qed.