Stream: Coq users

Topic: Tactic with optional parameter


view this post on Zulip 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:

What should I write?

view this post on Zulip Théo Winterhalter (Nov 03 2022 at 12:57):

I guess you could do it with Tactic Notation.

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (Nov 03 2022 at 12:59):

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

view this post on Zulip Théo Winterhalter (Nov 03 2022 at 13:02):

Maybe

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

view this post on Zulip Pierre Vial (Nov 03 2022 at 13:02):

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

view this post on Zulip Pierre Vial (Nov 03 2022 at 13:04):

aaah, yes, that should work

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (Nov 03 2022 at 13:06):

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

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

view this post on Zulip Théo Winterhalter (Nov 03 2022 at 13:07):

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

view this post on Zulip Pierre Vial (Nov 03 2022 at 13:11):

This does work, thanks a lot!

view this post on Zulip 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)).

view this post on Zulip Théo Winterhalter (Nov 03 2022 at 14:40):

If you replace constr by uconstr do you have the same issue?

view this post on Zulip 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

view this post on Zulip Théo Winterhalter (Nov 03 2022 at 15:11):

Which one remains?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 03 2022 at 22:56):

Making P implicit works around this specific problem.

view this post on Zulip Paolo Giarrusso (Nov 03 2022 at 22:57):

because foo (P := arg) becomes a legal term.

view this post on Zulip 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: Feb 06 2023 at 13:03 UTC