The Coq mailing list

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

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



2010/7/20 Marthe Bonamy 
<marthe.bonamy AT ens-lyon.fr>:
> Hi Gyesik,
>
> I'm not quite sure of what you're trying to do exactly?
>
> What troubles you here?
>
> The fact that you don't know how to tell Coq "I know, a is not in the
> environment, but it's okay", or the fact that you don't know how to tell him
> to parse things of the pattern "a := x", or something else entirely?
>
> Could you please for example give an example of the kind of thing you try to
> put into a tactic?
>
> Thanks,
>
> Marthe
>
> On 19 July 2010 07:50, Gyesik Lee 
>Â <gslee AT ropas.snu.ac.kr>
>  wrote:
>>
>> Hi,
>>
>> How can I write a tactic with a binding list as in the case of "apply
>> ... with ..." ?
>>
>> I am wondering which tactic argument can be used in the following example
>> case:
>>
>> Tactic Notation "papply" constr(H) "with" ???(a:=x)
>> Â := simpl; apply H with (a:=x)
>>
>> Any help will be greatly appreciated.
>>
>> Gyesik
>
>