Stream: MetaCoq

Topic: Implicits intros in tmLemma


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

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

view this post on Zulip Kenji Maillard (Oct 24 2022 at 10:14):

Or set it to the tactic that you plan to use to solve that goal.

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

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

view this post on Zulip Théo Winterhalter (Oct 24 2022 at 10:39):

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).

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

view this post on Zulip Gaëtan Gilbert (Oct 24 2022 at 10:41):

what does it print before the module?

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

view this post on Zulip Théo Winterhalter (Oct 24 2022 at 10:43):

Ok, it also prints idtac even though in a fresh file… :face_with_raised_eyebrow:

view this post on Zulip Théo Winterhalter (Oct 24 2022 at 10:45):

Ok, the local attribute seems to work if I change to auto instead.

view this post on Zulip Gaëtan Gilbert (Oct 24 2022 at 10:55):

idtac is the default
require program changes it


Last updated: Feb 04 2023 at 02:03 UTC