The Coq mailing list

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

2018-04-30 11:54 GMT+02:00 Soegtrop, Michael 
<michael.soegtrop AT intel.com>:
> Dear Pierre,
>
>> I think that would make a good feature wish.
>
> fine, I will create one.

I will try to find some time to implement it :-).

> Does the syntax you outlined work for eapply?

No because eapply makes evars with all uninstantiated variables anyway
so there is no need to have an explicit syntax for that. But
specialize has one more degree of freedom: one can chose to let some
parameters uninstantiated. See below.

> I am not such a fan of the "with" syntax and would like to write:

There is one general advantage to "with": you can omit completely
parameters that will be found by unification (you don't need to put
the right number of "_").
There is one particular advantage to "with" when used on "specialize":
you can also omit parameters that will not be found by unification:
they will be left in place.

For instance if you have a big hypothesis with several dependent
hypothesis and you would like to instantiate what can currently be:

...
H: forall (nme : name) (v : value) (addr_nme load_addr_nme : expr)
(vaddr : Values.val) (typ_nme : type) (cm_typ_nme : Ctypes.type),
                   transl_name st CE nme = Errors.OK addr_nme
                   → eval_expr g sp locenv m addr_nme vaddr
                     → evalName st s nme (OK v)
                       → transl_type st typ_nme = Errors.OK cm_typ_nme
                         → type_of_name st nme = Errors.OK typ_nme
                          → make_load addr_nme cm_typ_nme = Errors.OK
load_addr_nme
                           → ∃ v_t : Values.val, transl_value v v_t ∧
eval_expr g sp locenv m load_addr_nme v_t
...
Htrsl : transl_type st typ_nme = Errors.OK cm_typ_nme  (* I know this
must be my 4th dep hyp in H *)
...
==================
...

I like to write:

specialize H with (4:=Htrsl).

which will also instantiate (typ_nme : type) (cm_typ_nme :
Ctypes.type) and leave all other parameters of H unchanged.

Doing the same without "with" would be awful:

specialize (fun nme v addr_nme load_addr_nme vaddr h1 h2 h3 =>
h_stk_mtch_s_m nme v addr_nme load_addr_nme vaddr _ _ h1 h2 h3 Htrsl).

>         especialize (H t u _ ?[h2])
>
> in the case you outlined, assuming H has parameters x y and two hypothesis.
> Not sure if the ?[name] syntax works for eapply, though. I tend to use it 
> only with refine.

it seems so:

Lemma foo:forall n m , (forall a b:nat, a < m -> n = m -> False) -> False.
  intros n m H.
  eapply (H 1 2 ?[h] ?[h']).

The new feature should allow both syntaxes imho.

> I think one should keep the syntax and options identical to eapply - in the 
> end it is not that much of a difference if one tries to solve the current 
> goal or a prerequisite of a hypothesis.

I think [eapply t] means "I want to instantiate all hypothesis of t,
make evars with unsolved parameters". But with specialize there is one
more level of freedom as I said above: leave some hypothesis
uninstantiated. We should have a way to tell that to especialize imho.

P.


> Best regards,
>
> Michael