The Coq mailing list

[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