Stream: Coq users

Topic: Overriding reflexivity tactic


view this post on Zulip Ali Caglayan (Mar 24 2021 at 19:35):

I want to override the reflexivity tactic so that it does a bit more. This tactic is defined in the Ltac ML module. If I write Print Ltac I can see that reflexivity has the tactic value <ltac_plugin::reflexivity@0> but I can't seem to access this myself?

I want to essentially rename the old reflexivity to something else so I can still use it.

view this post on Zulip Jason Gross (Mar 24 2021 at 22:11):

I think you can do Ltac old_reflexivity := reflexivity. Tactic Notation "reflexivity" := ... and it should work correctly.

view this post on Zulip Jason Gross (Mar 24 2021 at 22:12):

Or even Ltac old_reflexivity := reflexivity. Ltac reflexivity := ... might work

view this post on Zulip Ali Caglayan (Mar 24 2021 at 23:15):

Huh weird, I had initially tried your second suggestion, but I kept running into a stackoverflow. Now however, everything seems to work fine...

view this post on Zulip Ali Caglayan (Mar 24 2021 at 23:25):

Oh wait this is still a problem

view this post on Zulip Ali Caglayan (Mar 24 2021 at 23:26):

When I do your second suggestion and then do Print Ltac reflexivity. it shows the plugin definition (at least outside the file)

view this post on Zulip Ali Caglayan (Mar 24 2021 at 23:27):

If I instead use ::= instead of := for the new reflexivity I get stackoverflow, since I am guessing the old_reflexivity now points to the new one.

view this post on Zulip Ali Caglayan (Mar 24 2021 at 23:30):

Here is what I am trying to do:

Ltac old_reflexivity := reflexivity.
Ltac reflexivity := old_reflexivity
|| (intros;
  let R := match goal with |- ?R ?x ?y => constr:(R) end in
  let pre_proof_term_head := constr:(@reflexivity _ R _) in
  let proof_term_head := (eval cbn in pre_proof_term_head) in
  apply (proof_term_head : forall x, R x x)).

view this post on Zulip Ali Caglayan (Mar 24 2021 at 23:31):

In a file that imports this, I do Print Ltac reflexivity and I get the original definition (which is wrong?)

view this post on Zulip Ali Caglayan (Mar 24 2021 at 23:31):

But as I mentioned if I use ::= then this also changes the definition of old_reflexivity to be circular

view this post on Zulip Ali Caglayan (Mar 24 2021 at 23:35):

but the tactic notation seems to work!

view this post on Zulip Jason Gross (Mar 25 2021 at 12:18):

Ali Caglayan said:

In a file that imports this, I do Print Ltac reflexivity and I get the original definition (which is wrong?)

Sounds like a bug, try making a stand-alone test-case and reporting it?

view this post on Zulip Jason Gross (Mar 25 2021 at 12:18):

(Alternatively, you're running into an issue with import order)

view this post on Zulip Enrico Tassi (Mar 25 2021 at 12:19):

May I ask why your improved-reflexivity tactic needs to be called exactly reflexivity?

view this post on Zulip Ali Caglayan (Mar 25 2021 at 16:35):

Well I'm working on removing the copy of the coq prelude that the HoTT library has. One of the things the HoTT library does is redefine the reflexivity tactic. At the moment, this is done with a little bit of hackery.

view this post on Zulip Ali Caglayan (Mar 25 2021 at 16:35):

I also can't seem to recreate this bug on its own.


Last updated: Mar 29 2024 at 04:02 UTC