The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

Le Tue, 20 Jul 2010 13:18:12 +0900,
Gyesik Lee 
<gslee AT ropas.snu.ac.kr>
 a écrit :

> Hi Marthe,
> 
> sorry for being not so exact with my question.
> 
> My problem is to write a (personal) tactic which behaves like "apply
> ... with..."
> Assume that I would like to always perform the "simpl" tactic before
> "apply":
> 
> Ltac sapply H := simpl; apply H.
> 
> But how can I am wondering if it is also possible to combine "simpl"
> with "apply ... with ...".
> If possible, I would like to know what to write in the "?(some binding
> list" part below:
> 
> Tactic Notation "sapply" constr(H) "with" ?(some binding list) :=
> simpl; apply  H with ?(some binding list)
> 
> I hope my problem is clear now.
> 
> Gyesik
> 
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.