Louise Dubois de Prisque (Oct 24 2022 at 09:29): Louise Dubois de Prisque (Oct 24 2022 at 09:29):Hello ! I have a question about tmLemma. When I try to create a proposition by using tmLemma, I get a proof obligation which is not exactly what I wanted because some intros are performed implicitely (and in this dummy case I also get silent simplifications) :
From MetaCoq Require Import All.
MetaCoq Run (tmLemma "foo"%bs (forall (A : Type), A = A -> False)).
Next Obligation.
(* 1 goal
A : Type
______________________________________(1/1)
False *)
Is there any way to avoid this behaviour ? In particular, I want to control what I have introduced because I may have an automatic tactic dealing with the proof.
Kenji Maillard (Oct 24 2022 at 10:13):You could modify the obligation tactic:
Obligation Tactic := idtac.
MetaCoq Run (tmLemma "foo"%bs (forall (A : Type), A = A -> False)).
Next Obligation.
(*forall A : Type, A = A -> False*)
Or set it to the tactic that you plan to use to solve that goal.
Théo Winterhalter (Oct 24 2022 at 10:19):Do you think we could do something on the MetaCoq side to avoid having to mess with globals like Obligation Tactic? I think ideally we would like to open a proof mode rather than obligations but I understand it is maybe too complicated.
Kenji Maillard (Oct 24 2022 at 10:33):I didn't know until 15min ago that MetaCoq was using the obligation mechanism this way... Opening a proof mode would require to merge all the obligations of a metacoq run(there might be multiple calls to tmLemma) and to dispatch them correctly which sounds tricky. I don't think we can reasonably modify the obligation tactic from within the metacoq program since there is no notion of tactic at that level.
One thing that is possible in order to delimit the modification of the obligation tactic is to scope this modification to a section or module., e.g
Module Foo.
#[local]
Obligation Tactic := idtac.
Show Obligation Tactic.
MetaCoq Run (tmLemma "bat"%bs (forall (A : Type), A = A -> False)).
Next Obligation.
Admitted.
End Foo.
Show Obligation Tactic.
Does the local attribute work for Obligation Tactic, last I tried it did not work. Requiring a module that changed it was enough to change it if I remember correctly.
Anyway, you are right for the proof mode, but for obligations, Equations can change the obligation tactic locally to be something else, maybe we could provide a shorthand to use idtac. We would have tmLemma for the version with Obligation Tactic, and tmLemmaIdtac for the version with idtac (presumably with a better naming convention).
Théo Winterhalter (Oct 24 2022 at 10:40):For me this prints:
Program obligation tactic is idtac (locally defined)
Program obligation tactic is idtac (globally defined)
what does it print before the module?
Kenji Maillard (Oct 24 2022 at 10:42):Théo Winterhalter said:
Does the local attribute work for
Obligation Tactic, last I tried it did not work. Requiring a module that changed it was enough to change it if I remember correctly.
Possibly, I don't know anything about the module system... Prefer a Section then ?
Théo Winterhalter (Oct 24 2022 at 10:43):Ok, it also prints idtac even though in a fresh file… :face_with_raised_eyebrow:
Théo Winterhalter (Oct 24 2022 at 10:45):Ok, the local attribute seems to work if I change to auto instead.
Gaëtan Gilbert (Oct 24 2022 at 10:55):idtac is the default
require program changes it
Louise Dubois de Prisque (Oct 24 2022 at 11:15):Thank you everyone for your detailled answers !
Notification Bot (Oct 24 2022 at 11:16):Louise Dubois de Prisque has marked this topic as resolved.
Last updated: May 31 2023 at 03:30 UTC