The Coq mailing list

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

Nice, thanks Jonathan!

One small glitch yet: the name of the re-asbtracted hypothesis are not kept the same. I guess it is hard to keep them around.

P.

2016-01-09 18:22 GMT+01:00 Jonathan Leivent <jonikelee AT gmail.com>:

Attached.  Example usage at the end of abstractedas.v.  I haven't tested any other cases - so caveats apply.  Let me know if it needs fixing.

The one undocumented v8.5 feature it uses is named evars in numbergoals.v (?[__Number_Goals]) - but this can be removed in the case of the abstracted as tactic if necessary (by using an evar created in abstracted as prior to the "unshelve tac" call).

-- Jonathan

On 01/08/2016 07:14 PM, Pierre Courtieu wrote:

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