coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Give scope annotations for arguments of Ltac-defined tactics?

From: Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Give scope annotations for arguments of Ltac-defined tactics?
Date: Tue, 4 Jan 2022 10:15:22 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=p.l.lumsdaine AT gmail.com; spf=Pass smtp.mailfrom=p.l.lumsdaine AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f41.google.com
Ironport-data: A9a23:kTf0uqiZzdXnmM1lNTqa2PmzX161DxEKZh0ujC45NGQNrF6WrkUHz2YfW2DUaPqPa2ameY1/bt/l8RsAuJTSz9BqTAs++FhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t51GAjX4wXFdokb0/n9BCZC86yksvU20buCkUrScY3gtHVYMpBoJ0HqPpcZp2uaEvvDiW2thifuqyyHuEAfNNwxcagr42IrfwP9bh8kejRtD1rAIiV+ni3eF/5UdJMp3yahctBIUSKEMdgKxb76rIL1UYgrkExkR5tONyt4Xc2UPS7/WeBeL0z9YB/HkjR9FqSg/lK08MZLwa28N02TPz403kY8d88DpIesqFvWkdOA1S19cVSVjOLZK8b7BLFCwtMWSywvNdH6EL/BGVRprZtBJpL0f7WZmrKREcljhdCurjOWvhbm/V+NEndUmNMCtPYUFu3gmwyuxMBqMaYSbFv+MussBiW923tQUSK6YPZtIMC40OUyGPgkQb34JLLk7uMuoolj2VQFCjGyUgL5uuz2LiFUqxNABK/LQc92OANpQxwOW+juA8GP+DRUXcteYzFK4HruXrrentUvGtEg6TuzQGj9WbFyvKqg7DRQXUR6kpKD8hBLnHd1YLEMQ92wlqq1aGImDJjXid0XQnZJGlkd0txls/ykS5wSEy66S6AGcboTBZiAUc8Qo7afaWhRzvmJkXLrV6fhHv7icSHbb/bCRxd93EUD5MkdaDRI5ocA5DxUPbW39Yt8jjjquLUJtsuDIJA==
Ironport-hdrordr: A9a23:qvtCbqOpZBDLIMBcTtyjsMiBIKoaSvp037BL7TETdfU7SL38qynDppomPHzP6Ar5JktQ++xoUZPoKRi3yXcS2+gs1NyZMDUO1lHEEGgb1+Tf/wE=
Ironport-phdr: A9a23:/cQ2yB383glhCxYCsmDOTgQyDhhOgF0UFjAc5pdvsb9SaKPrp82kYBaGo6w21xSQBs3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmTowZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsipyuy+4YDfbgtGiTayfL9/Igi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgINzA3/mLZhNFugq1Hux+uvQBzzpTObY2JKPZzfKXQds4aS2pbWcZRUjRMDJmiYIsTEeUBJ/tToY/jqFUOtxS+AxSsD/7pxD9Vg3/2xrA13P4gEQHAwgMrAtUDsGzOoNXxLqsSVf21zKzTzTredfxW2DH955bTfxAupPGDR7Nwcc7LxUYzEAPFi0ydpIr4NDyayuoDqXKU7/Z8Ve2xkW4nrRl8rzivyMswiITEiYEYxFDK+Ct5wos7K9m1RVB1b9OrEpZdtjyWOotoT84/XWxluik0x78EtJO/fCUHyooryh3RZvGBboOG4QrjWf6PLTtkgH9pYrGyihao/US91OHxVdO43VlXoidDj9LCrGoC1wbJ5ciCUvZ9/lmu2TKI1w3L7+FLO0E0la7CJ58vx748i4MfsUrMEyPrgkn2g6iWdkIr+uis9evreKnpppiZN4NsiwH+NLohmtCnDOgmLgQDW3KX9Oe82bH54EH1XrZHguc5n6XEqJzaIN4Upq+9Aw9byIYj7BO/Ai++0NgCmXkLNlZFeA+Cj4jyJl7BOvH4DfGhjFm3nzdrwurJPrzlApnXMnfDl7Lhca5n60FA0Aoz0cxf55VMB74dJ/LzQ1b9u8DcDh8kKAO52P3nCdV41oMGQ22DGK6ZMKXIsV+J/O0jOeeMZJVG8Ar6fvMi/rvliWIzsV4bZ6igm5UNO16iGfEzG0iFbGCkptovGGEX9i4jSffmgVyEXHYHfzC2GaYh4yo3AYOgAK/MQ4mshPqK2yLtTc4eXXxPFl3ZSSSgTI6DQfpZMEp6zedulzUFUf6qTIpzjHlGVSf/wrtja/XRo2gW6cul299y6One0xo18G4sZyx4+26IRmBw2GgPQm1utJ0=

Is there a way to give scope annotations to arguments of an Ltac-defined tactic (or a Tactic Notation), so that the argument is always parsed with the specified scope? I’m looking for something analogous to what you can give for tunctions using [Arguments]:

Arguments my_function _%nat.

but for tactics. If I define

Ltac apply_my_function p := apply (my_function p).

then the argument to [apply_my_function] will *not* automatically be parsed in nat_scope, even though in [apply (my_function p)] it would be.

I’ve tried a few things like

Tactic Notation "apply_my_function" uconstr(p) := apply (my_function p%nat).

but haven’t found anything that works.

A self-contained MWE for the problem follows below.

Best,

–Peter.

===============
Declare Scope my_nat_scope.
Notation "!1" := Nat.one : my_nat_scope.

Declare Scope my_bool_scope.
Notation "!1" := true : my_bool_scope.

Open Scope my_bool_scope.

Definition f : nat -> nat := fun x => x.
Arguments f _%my_nat.

Check (f !1).

Ltac apply_f p := apply (f p).

Goal nat.
Fail apply_f !1. (* How to define [apply_f] so that this succeeds? *)
apply_f !1%my_nat.
Qed.

===============

[Coq-Club] Give scope annotations for arguments of Ltac-defined tactics?, Peter LeFanu Lumsdaine, 01/04/2022
- Re: [Coq-Club] Give scope annotations for arguments of Ltac-defined tactics?, Jason Gross, 01/04/2022