The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

No there is not afaik. But if the predicate you want is your goal+beta expansion then you can use “pattern r n b” to do the beta expansion.

P

Le ven. 18 mai 2018 à 02:18, Joachim Breitner <mail AT joachim-breitner.de> a écrit :

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/