The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

Hi Arthur,

it's wonderful to hear that someone else has already thought about my problem.
Indeed I have searched for anything similar in the libraries for
"Engineering Formal Metatheory".
I will have a look at the other homepage.

Many thanks,

Gyesik


2010/7/21 Arthur Charguéraud 
<arthur.chargueraud AT inria.fr>:
>> Tactic Notation "sapply" constr(H) "with" ?(some binding list) :=
>>  simpl; apply  H with ?(some binding list)
>
> Hi,
>
> I did encounter exactly the same problem as yours some time ago.
> Yet, since I wanted to build many tactics like your "sapply",
> the solution of copy-pasting were not acceptable for me.
>
> So, I did develop a general hack, implemented in Ltac,
> that lets you write an invokation of "apply" as folows:
>
> Â applys (>>> H E1 ... EN)
>
> where H is a lemma and Ei are some arguments.
> The tactic will instantiate the lemma H with the
> arguments Ei following a "first-match" rule, so
> you can skip some arguments of H and in general
> it will work just like you would expect.
>
> Note that the expression "(>>> H E1 ... EN)" is a Coq term,
> represented as a list of values of different types, and this list
> is parsed using a special notation introduced by the symbol ">>>".
> Therefore, you can easily build other tactics based on "applys".
> or example, in your case, you may want to write:
>
> Â Ltac sapply T := simpl; applys T.
> Â ...
> Â sapply (>>> H a b c).
>
>
> You can find the source code of my tactic, and the code
> of many other Ltac hacks, from the following url:
>
> http://arthur.chargueraud.org/projects/proofs/tactics/
>
> The files come with documentation and demos. To use them,
> it suffices to compile the library and import to it in
> your development. Don't hesitate to contact me in case you
> need any further information.
>
> +
> Arthur
>
>
>> Hi,
>>
>>> That is not very satisfying, but isn't it possible to do something
> like:
>>>
>>> Tactic Notation "sapply" constr(H) "with" ?a :=
>>> simpl; apply  H with ?a.
>>>
>>> Tactic Notation "sapply" constr(H) "with" ?a ?b :=
>>> simpl; apply  H with ?a ?b.
>>>
>>> Tactic Notation "sapply" constr(H) "with" ?a ?b ?c :=
>>> simpl; apply  H with ?a ?b ?c.
>>>
>>> Tactic Notation "sapply" constr(H) "with" ?a ?b ?c ?d :=
>>> simpl; apply  H with ?a ?b ?c ?d.
>>>
>>> Tactic Notation "sapply" constr(H) "with" ?a ?b ?c ?d ?e :=
>>> simpl; apply  H with ?a ?b ?c ?d ?e.
>>>
>>> So that you can use list of at most 5 parameters.
>>> I know it shouldn't be the right way to do this, but also consider that
>>> having a list of more than 6 terms could mean that a dedicated tactic
>>> is welcome.
>>
>> many thanks for the suggestion. It provides a reasonable solution to
>> my problems.
>>
>> Gyesik
>