The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

Hi,

Pierre writes in another thread:

> 2) I would expect (P x (foo x)) for the conclusion of foo_ind_aux instead
> of (P (foo x)). Did you just simplify your example or do you manage to use
> it like that?

and of course he is right. But now I am running into problems with
higher-order unification when I try to apply the custom induction rule:

   Unable to unify "?P (take n b) n b" with
   "length (take n b) = Init.Nat.min n (length b)".

I can work around by instantiating P explicitly, with

   apply take_ind where (P := fun r n b => … ).

but I wonder if I can do better. Is there a trick that would make Coq
figure out P on its own? Maybe some particular order of arguments of P,
or a different tactic?

(I know that higher order unification is in general undecidable, and
that this instance admits multiple solutions… but still, hope dies
last.)

Cheers,
Joachim


-- 
Joachim Breitner
  
mail AT joachim-breitner.de
  http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part