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.
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.
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.
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).
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?
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 ?
Ok, it also prints idtac
even though in a fresh file… :face_with_raised_eyebrow:
Ok, the local
attribute seems to work if I change to auto instead.
idtac is the default
require program changes it
Thank you everyone for your detailled answers !
Louise Dubois de Prisque has marked this topic as resolved.
Last updated: May 31 2023 at 03:30 UTC