Pierre Vial (Nov 03 2022 at 12:57): Pierre Vial (Nov 03 2022 at 12:57):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?
Théo Winterhalter (Nov 03 2022 at 12:57):I guess you could do it with Tactic Notation.
Théo Winterhalter (Nov 03 2022 at 12:59):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.
Théo Winterhalter (Nov 03 2022 at 12:59):https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Tactic-Notation
Théo Winterhalter (Nov 03 2022 at 13:02):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
Pierre Vial (Nov 03 2022 at 13:04):aaah, yes, that should work
Théo Winterhalter (Nov 03 2022 at 13:05):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.
Pierre Vial (Nov 03 2022 at 13:11):This does work, thanks a lot!
Pierre Vial (Nov 03 2022 at 14:29):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)).
Théo Winterhalter (Nov 03 2022 at 14:40):If you replace constr by uconstr do you have the same issue?
Pierre Vial (Nov 03 2022 at 14:52):The second problem is solved but not the first one.
I think I'll give up Tactic Notations for now
Théo Winterhalter (Nov 03 2022 at 15:11):Which one remains?
Pierre Vial (Nov 03 2022 at 15:14):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.
Théo Winterhalter (Nov 03 2022 at 15:39):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.
Paolo Giarrusso (Nov 03 2022 at 22:56):Making P implicit works around this specific problem.
Paolo Giarrusso (Nov 03 2022 at 22:57):because foo (P := arg) becomes a legal term.
Paolo Giarrusso (Nov 03 2022 at 22:58):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: Apr 19 2024 at 09:01 UTC