Stream: Coq users

Topic: Overriding reflexivity tactic

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.

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.

Jason Gross (Mar 24 2021 at 22:12):

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

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

Ali Caglayan (Mar 24 2021 at 23:25):

Oh wait this is still a problem

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)

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.

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

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

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

Ali Caglayan (Mar 24 2021 at 23:35):

but the tactic notation seems to work!

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?

Jason Gross (Mar 25 2021 at 12:18):

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

Enrico Tassi (Mar 25 2021 at 12:19):

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

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.

Ali Caglayan (Mar 25 2021 at 16:35):

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

Last updated: Oct 03 2023 at 19:01 UTC