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:
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 "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.
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.
blut with (P := fun _ => True).
Syntax error: [constr] expected after ':=' (in [simple_tactic]).
blut with (P := (fun _ => True)).
Cannot infer the type of this anonymous binder in environment:
whereas this works fine when I use
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
uconstr do you have the same issue?
The second problem is solved but not the first one.
I think I'll give up
Tactic Notations 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.
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