Stream: Coq users

Topic: ✔ Disabling Local Notation in a Coq file

Mukesh Tiwari (Jan 09 2023 at 05:39):

Hi everyone,

I am working with a Coq file with a lot of local notations and I find it hard to work with it when proving a lemma. Basically, during the proof, it shows the notation while I want to see the text part. Is there a way to do this? For example, the Coq file I am working roughly looks like this:

  Local Notation "x =S= y" := (eqSAP x y = true) (at level 70).
  Local Notation "[P1]" := (uop_manger_phase_1 eqA addP).  (* Phase 1 reduction *)
  Local Notation "[P2]" := (@uop_manger_phase_2 A P lteA). (* Phase 2 reduction *)

  Lemma that I want to prove is:
  Lemma P1_P2_commute : ∀ X, ([P2] ([P1] X)) =S= ([P1] ([P2] X)).

I want to set some flags such that when I start proving the P1_P2_commute, it should look like :

  Lemma P1_P2_commute : ∀ X, ([P2] ([P1] X)) =S= ([P1] ([P2] X)).
  Proof.
     At this point, if I am looking at the Coq goal it should appear like:

   ∀ X : finite_set (A * P),
     eqSAP (@uop_manger_phase_2 A P lteA (uop_manger_phase_1 eqA addP X))
     (uop_manger_phase_1 eqA addP (@uop_manger_phase_2 A P lteA X)) = true.

I have tried Set Printing All, suggested Stackoverflow, but it is not working for me.

Pierre Roux (Jan 09 2023 at 07:19):

Adding (only parsing) at the end of the Local Notation commands?

Mukesh Tiwari (Jan 09 2023 at 10:08):

Thank you very much @Pierre Roux ! This is what I was looking for.

Notification Bot (Jan 09 2023 at 10:08):

Mukesh Tiwari has marked this topic as resolved.

Paolo Giarrusso (Jan 09 2023 at 13:43):

FWIW, to disable all notations you want Set Printing Notations, or Unset Printing All if you want to disable even more sugar

Last updated: Apr 19 2024 at 06:02 UTC