The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hi, Pierre --

I had a half-completed email with the same solution. I'm not familiar with any tactic that would let you do this in general, though I imagine there is a horrible implementation that looks something like:

Ltac specialize_n H n v :=

  match n with

  | 2 => first [ specialize (H _ v) | specialize (fun x => H x v) ]

  | ...

end.

The general solution seems like it would require a plugin, but someone else might have a cleaner solution.

On Wed, Dec 23, 2015 at 10:10 AM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Here is a workaround that I use.

Goal False.

assert (forall (A B C:Type), A->B->C) as H by admit.

specialize (fun A a C => H A nat C a O).

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Dec 23, 2015 at 10:36 AM, Pierre Courtieu <Pierre.Courtieu AT cnam.fr> wrote:

Hi,

[specialize] is kind of useful but it needs a list of concrete terms
for a *prefix* of list of premisses of a hypothesis.

AFAIK you cannot give only, say, 3rd and 5th arguments. Sometime this
would be useful (because the hypothesis has independent premisses and
no particular order in the hyps is better than another).

Is there something to do so? I have a Ltac piece of code which does
roughly this in a naive way, but it is limited to one argument at a
time.

Idealy I would like to write:

generalize H with (x:=0) (3:=H2)(5:=H6).

Is this creatively hackable in ltac :) ?

Best regards,
Pierre

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/