The Coq mailing list

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

That would be very nice. Thanks Jonathan!

Pierre

Le vendredi 8 janvier 2016, Jonathan Leivent <jonikelee AT gmail.com> a écrit :

On 01/08/2016 01:03 PM, Pierre Courtieu wrote:

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.

I think I can do this entirely in Ltac in v8.5 (but not v8.4). Briefly, it would start off with something like this:

Goal forall a b c, Q a b c ->
              (forall x t y z, P x t -> Q x y z -> R) -> False.
Proof.
  intros a b c H0 H.

  evar (T:Type).
  let p := constr:(ltac:(
                    intro Admit;
                    subst T;
                    unshelve eapply H with (2:=H0);
                    apply Admit): (forall T, T) -> T) in
  idtac p.

but would also use a goal numbering tactic I wrote to first number each of the subgoals generated by the eapply, then incorporate that number into the Admit so that the resulting subterm generated for each subgoal has something like a De Bruijn index in it.  Then parse that result with match/context replacement to change each of those Admit subterms into a variable bound in an outer fun.

I'll give it a try if you don't mind the fact that the result will contain a lot of Ltac hacking.  Also, unfortunately, because there is no Tactic Notation arg type for passing a "constr_with_bindings_arg_list" down to that eapply, you'd have to pass the eapply in as a tactic - so the top-level invocation would have to look at least something like:

  foo eapply H with (2:=H0)

But, it would be a general solution in as much as eapply is itself a general solution: any number of correct bindings would be allowed.

-- Jonathan

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/