The Coq mailing list

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

Thanks for the answers. This is also the solution I came up with, more
or less. But what one really want is to use the unification stuff
during the process, so that instantiating one argument also
instantiates some other (prvious) arguments.

Suppose you have

H0: Q a b c
H: forall x t y z, P x t -> Q x y z -> R.
======
...

Then "specialize with (2:=H0)" should actually instantiate x y and z:
H0: Q a b c
H: forall t, P a t -> R.
======
...

P.



2015-12-23 19:15 GMT+01:00 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/