The Coq mailing list

[Robert R Schneck <schneck AT math.berkeley.edu>]

On Tue, 1 Jul 2003 
dachuan.yu AT yale.edu
 wrote:
> I have something like this:
> precond : nat -> Type.
> g : (precond O).
> H2: (G_Weaken g (baseG O a1 g1)).
>
> where G_Weaken is some relation defined between (precond O).
>
> When I tried to do induction on g, it says "Cannot solve a second-
> order unification problem". Is this something fundamentally not
> doable, or could I get around this somehow? Doing inversion on H2 does
> not help because that way I don't get an induction hypothesis. Doing
> induction on H2 is not what I want because I need the fact that the
> second argument of G_Weaken is (baseG ...).

I've run into similar problems countless times, and expressed my
frustration in the same way: I want something that combines the best of
the Inversion and Induction tactics!

That said, I don't have a cookbook solution.  Try something like
  H2: (G_Weaken g x)
  -----------------------------
  (x = (baseG O a1 g1)) -> Goal
and then use Induction.

Robert