Hi,

I would like a simple example of a tactic with an optional argument (or specification). I regretfully didn't find any in the refman although the topic seems to be addressed.

Here is the kind of setting I'm thinking of.

I have a very useful lemma `foo`

which has a predicate `P : A -> Prop`

as a parameter.

I want to define a tactic `blut`

such as:

`blut.`

does`intros ; destruct_paris ; eapply foo.`

`blut with (P:= P_0).`

does`intros ; destruct_paris ; eapply foo with (P := P0).`

What should I write?

I guess you could do it with `Tactic Notation`

.

Something like

```
Tactic Notation "blut" := blut_0.
Tactic Notation "blut" "with" t := blut_1 t.
```

But I don't know if you can pass `(P := P_0)`

this way.

https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Tactic-Notation

Maybe

```
Tactic Notation "blut" "with" ident(P) ":=" constr(t) := eapply foo with (P := t).
```

Thanks, but I guess that if ever, for another predicate, I would like sometimes specify `P`

or sometimes something else or sometimes both, I would be limited by this approach (btw, `P0`

is not a unique constant in practice).

I'll see if someone has another more general suggestion

aaah, yes, that should work

It seems to work:

```
From Coq Require Import Utf8.
Definition foo : ∀ (n : nat), n = n.
Proof.
reflexivity.
Qed.
Tactic Notation "blut" :=
idtac.
Tactic Notation "blut" "with" ident(P) ":=" constr(t) :=
eapply foo with (P := t).
Goal ∀ (n : nat), n = n.
Proof.
intro k.
blut.
blut with n := k.
Qed.
```

If you want parentheses, it seems you can simply add them:

```
Tactic Notation "blut" "with" "(" ident(P) ":=" constr(t) ")" :=
eapply foo with (P := t).
```

This will only work for one argument though. You could overload for 2, 3 etc.

This does work, thanks a lot!

mmh, actually, I have problem related to both syntax and semantic with this solution.

For instance:

```
blut with (P := fun _ => True).
```

gives me `Syntax error: [constr] expected after ':=' (in [simple_tactic]).`

Moreover:

```
blut with (P := (fun _ => True)).
```

`Cannot infer the type of this anonymous binder in environment:`

whereas this works fine when I use `eapply`

Moreover, I would like Coq to behave intelligently (as in the case of `eapply`

) if I just write `blut with with (P := (fun _ => True)).`

If you replace `constr`

by `uconstr`

do you have the same issue?

The second problem is solved but not the first one.

I think I'll give up `Tactic Notation`

s for now

Which one remains?

I still have the syntax error if I don't put parentheses around the argument.

I reverted to a former commit, but I also think that it was also incompatible with destructing directly the parameter of a predicate, i.e., writing `blut with (P := (fun '(_ , n ) => Q n))`

didn't work.

Well the parentheses are not so bad I would say, but I understand. I also don't know if there is way to avoid them.

Making P implicit works around this specific problem.

because `foo (P := arg)`

becomes a legal term.

Not a great solution but ltac1 tactic notations are what they are, and we're missing one piece to use ltac2 notations here conveniently.

Last updated: Sep 30 2023 at 07:01 UTC