Merge pull request #232 from DmxLarchey/notation-overridden-2

mrhaandi · web-flow · commit 3edeccf86593 · 2025-04-12T10:40:27.000+02:00
Cleanup for overridden notations
diff --git a/theories/FOL/FOL.v b/theories/FOL/FOL.v
@@ -19,11 +19,13 @@ From Undecidability.FOL Require Deduction.FullND.
   | quant {b} : quantop -> form b -> form b.    
 *)
 
-
+(*
 
 Import FragmentSyntax.
 Export FragmentSyntax.
 
+*)
+
 (* ** Instantiation to signature with 1 constant, 2 unary functions, 1 prop constant, 1 binary relation *)
 
 Inductive syms_func := s_f : bool -> syms_func | s_e.
@@ -66,7 +68,7 @@ Definition FOL_prv_class := @prv _ _ falsity_on class nil.
 
 (* ** List of decision problems concerning validity, satisfiability and provability *)
 
-Import BinSig Semantics.Tarski.FullCore. 
+Import BinSig (* Semantics.Tarski.FullCore *) .
 
 (* Validity of formulas with falsity in Tarski semantics *)
 Definition binFOL_valid := @FullCore.valid sig_empty sig_binary falsity_on.
diff --git a/theories/FOL/Reductions/H10UPC_to_FOL_friedman.v b/theories/FOL/Reductions/H10UPC_to_FOL_friedman.v
@@ -53,7 +53,11 @@ Section Fr_validity.
       - exact (H10UPC_SAT h10).
       - exact (dom_rel' (Vector.hd v) (Vector.hd (Vector.tl v))).
     Defined.
+
+    (* [DLW] This one is overridden by a new definition, may be change the notation slightly
+             would be better? *)
     #[local] Notation "rho ⊨ phi" := (sat rho (Fr phi)) (at level 20).
+
     (* Now we need rewrite helpers which transform our syntactic sugar into useful statements in the model *)
     Lemma IB_sFalse rho : rho ⊨ (∀ ∀ Pr $0 $1) <-> H10UPC_SAT h10.
     Proof.
diff --git a/theories/FOL/Reductions/H10p_to_FA.v b/theories/FOL/Reductions/H10p_to_FA.v
@@ -96,7 +96,7 @@ Section FA_ext_Model.
   Hypothesis ext_model : extensional I.
   Hypothesis FA_model : forall ax rho, In ax FA -> rho ⊨ ax.
 
-  Notation "'iO'" := (i_func (f:=Zero) (Vector.nil D)) (at level 2) : PA_Notation.
+  (* Notation "'iO'" := (i_func (f:=Zero) (Vector.nil D)) (at level 2) : PA_Notation. *)
   
   Fact eval_poly sigma p : eval (sigma >> iμ) (embed_poly p) = iμ (dp_eval_pfree sigma p).
     Proof using ext_model FA_model.
@@ -137,7 +137,7 @@ Section FA_Model.
 
   Hypothesis FA_model : forall rho ax, In ax FAeq -> rho ⊨ ax.
 
-  Notation "'iO'" := (i_func (f:=Zero) (Vector.nil D)) (at level 2) : PA_Notation.
+  (* Notation "'iO'" := (i_func (f:=Zero) (Vector.nil D)) (at level 2) : PA_Notation. *)
   
   Lemma problem_to_model E sigma : H10p_sem E sigma -> (sigma >> iμ) ⊨ embed_problem E.
   Proof using FA_model.
diff --git a/theories/FOL/Reductions/PCPb_to_FSTD.v b/theories/FOL/Reductions/PCPb_to_FSTD.v
@@ -26,7 +26,7 @@ Section FST.
 
 Context { p : peirce }.
 
-Close Scope sem.
+Close Scope FSTsem.
 
 Lemma FST_eset x :
   FSTeq ⊢ ¬ (x ∈ ∅).
diff --git a/theories/FOL/Reductions/PCPb_to_HF.v b/theories/FOL/Reductions/PCPb_to_HF.v
@@ -15,8 +15,6 @@ Import ListAutomationNotations ListAutomationHints.
 Local Set Implicit Arguments.
 Local Unset Strict Implicit.
 
-
-
 (* ** Reduction function *)
 
 Local Definition BSRS := list(card bool).
diff --git a/theories/FOL/Reductions/PCPb_to_HFD.v b/theories/FOL/Reductions/PCPb_to_HFD.v
@@ -26,7 +26,7 @@ Section HF.
 
 Context { p : peirce }.
 
-Close Scope sem.
+Close Scope HFsem.
 
 Lemma HF_eset x :
   HFeq ⊢ ¬ (x ∈ ∅).
diff --git a/theories/FOL/Reductions/PCPb_to_ZF.v b/theories/FOL/Reductions/PCPb_to_ZF.v
@@ -16,7 +16,6 @@ Import ListAutomationNotations ListAutomationHints.
 Local Set Implicit Arguments.
 Local Unset Strict Implicit.
 
-
 (* ** Reduction function *)
 
 Local Definition BSRS := list(card bool).
diff --git a/theories/FOL/Reductions/PCPb_to_ZFD.v b/theories/FOL/Reductions/PCPb_to_ZFD.v
@@ -26,7 +26,7 @@ Section ZF.
 
 Context { p : peirce }.
 
-Close Scope sem.
+Close Scope ZFsem.
 
 Lemma ZF_eset x :
   ZFeq' ⊢ ¬ (x ∈ ∅).
diff --git a/theories/FOL/Reductions/PCPb_to_binZF.v b/theories/FOL/Reductions/PCPb_to_binZF.v
@@ -152,7 +152,7 @@ From Undecidability.FOL Require Import Reductions.PCPb_to_ZFeq.
 
 Section Model.
 
-  Open Scope sem.
+  Open Scope ZFsem.
 
   Context {V : Type} {I : interp V}.
 
@@ -218,7 +218,7 @@ Section Model.
     erewrite sat_comp, sat_ext. reflexivity. now intros [].
   Qed.
 
-  Notation "x ≈ y" := (forall z, (x ∈ z -> y ∈ z) /\ (y ∈ z -> x ∈ z)) (at level 35) : sem.
+  Notation "x ≈ y" := (forall z, (x ∈ z -> y ∈ z) /\ (y ∈ z -> x ∈ z)) (at level 35) : ZFsem.
 
   Lemma eq_equiv x y :
     x ≈ y <-> x ≡ y.
diff --git a/theories/FOL/Reductions/PCPb_to_minZF.v b/theories/FOL/Reductions/PCPb_to_minZF.v
@@ -129,7 +129,7 @@ Qed.
 
 Section Model.
 
-  Open Scope sem.
+  Open Scope ZFsem.
 
   Context {V : Type} {I : interp V}.
 
diff --git a/theories/FOL/Reductions/PCPb_to_minZFeq.v b/theories/FOL/Reductions/PCPb_to_minZFeq.v
@@ -23,7 +23,7 @@ Local Notation vec := Vector.t.
 
 Section Model.
 
-  Open Scope sem.
+  Open Scope ZFsem.
 
   Context {V : Type} {I : interp V}.
 
diff --git a/theories/FOL/Reductions/ZF_to_FST.v b/theories/FOL/Reductions/ZF_to_FST.v
@@ -129,7 +129,7 @@ End IM.
 
 Section Model.
 
-  Open Scope sem.
+  Open Scope ZFsem.
 
   Context {V : Type} {I : interp V}.
 
diff --git a/theories/FOL/Semantics/Tarski/FragmentCore.v b/theories/FOL/Semantics/Tarski/FragmentCore.v
@@ -59,9 +59,13 @@ End Tarski.
 Arguments sat {_ _ _ _ _} _ _, {_ _ _} _ {_} _ _.
 Arguments interp {_ _} _, _ _ _.
 
-Notation "p ⊨ phi" := (sat _ p phi) (at level 20).
-Notation "I ⊨= phi" := (forall p, sat I p phi) (at level 20).
-Notation "p ⊫ A" := (forall psi, psi el A -> sat _ p psi) (at level 20).
+Declare Scope fragment_notations.
+
+Notation "p ⊨ phi" := (sat _ p phi) (at level 20) : fragment_notations.
+Notation "I ⊨= phi" := (forall p, sat I p phi) (at level 20) : fragment_notations.
+Notation "p ⊫ A" := (forall psi, psi el A -> sat _ p psi) (at level 20) : fragment_notations.
+
+Open Scope fragment_notations.
 
 Section Defs.
 
diff --git a/theories/FOL/Semantics/Tarski/FullCore.v b/theories/FOL/Semantics/Tarski/FullCore.v
@@ -63,9 +63,13 @@ End Tarski.
 Arguments sat {_ _ _ _ _} _ _, {_ _ _} _ {_} _ _.
 Arguments interp {_ _} _, _ _ _.
 
-Notation "p ⊨ phi" := (sat _ p phi) (at level 20).
-Notation "I ⊨= phi" := (forall p, sat I p phi) (at level 20).
-Notation "p ⊫ A" := (forall psi, psi el A -> sat _ p psi) (at level 20).
+Declare Scope full_notations.
+
+Notation "p ⊨ phi" := (sat _ p phi) (at level 20) : full_notations.
+Notation "I ⊨= phi" := (forall p, sat I p phi) (at level 20) : full_notations.
+Notation "p ⊫ A" := (forall psi, psi el A -> sat _ p psi) (at level 20) : full_notations.
+
+Open Scope full_notations.
 
 Section Defs.
 
diff --git a/theories/FOL/Sets/FST.v b/theories/FOL/Sets/FST.v
@@ -14,21 +14,21 @@ From Stdlib Require Import List.
 Import FSTSignature.
 Export FSTSignature.
 
-Declare Scope syn.
-Open Scope syn.
+Declare Scope FSTsyn.
+Open Scope FSTsyn.
 
 (* ** Axioms *)
 
-Notation "x ∈ y" := (atom _ ZFSignature.ZF_pred_sig elem ([x; y])) (at level 35) : syn.
-Notation "x ≡ y" := (atom (Σ_preds := ZFSignature.ZF_pred_sig) equal ([x; y])) (at level 35) : syn.
+Notation "x ∈ y" := (atom _ ZFSignature.ZF_pred_sig elem ([x; y])) (at level 35) : FSTsyn.
+Notation "x ≡ y" := (atom (Σ_preds := ZFSignature.ZF_pred_sig) equal ([x; y])) (at level 35) : FSTsyn.
 
-Notation "∅" := (func FST_func_sig eset ([])) : syn.
-Notation "x ::: y" := (func FST_func_sig adj ([x; y])) (at level 31) : syn.
+Notation "∅" := (func FST_func_sig eset ([])) : FSTsyn.
+Notation "x ::: y" := (func FST_func_sig adj ([x; y])) (at level 31) : FSTsyn.
 
 Definition sub x y :=
   ∀ $0 ∈ x`[↑] → $0 ∈ y`[↑].
 
-Notation "x ⊆ y" := (sub x y) (at level 34) : syn.
+Notation "x ⊆ y" := (sub x y) (at level 34) : FSTsyn.
 
 Definition ax_ext :=
   ∀ ∀ $1 ⊆ $0 → $0 ⊆ $1 → $1 ≡ $0.
@@ -73,5 +73,3 @@ Definition FSTeq :=
 Inductive FSTIeq : form -> Prop :=
 | FSTeq_base phi : In phi FSTeq -> FSTIeq phi
 | FSTeq_ind phi : FSTIeq (ax_ind phi).
-
-
diff --git a/theories/FOL/Sets/Models/FST_model.v b/theories/FOL/Sets/Models/FST_model.v
@@ -12,21 +12,21 @@ From Stdlib Require Import Lia.
 
 (* ** ZF-Models *)
 
-Declare Scope sem.
-Open Scope sem.
+Declare Scope FSTsem.
+Open Scope FSTsem.
 
 Arguments Vector.nil {_}, _.
 Arguments Vector.cons {_} _ {_} _, _ _ _ _.
 
-Notation "x ∈ y" := (@i_atom _ _ _ _ elem (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : sem.
-Notation "x ≡ y" := (@i_atom _ _ _ _ equal (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : sem.
-Notation "x ⊆ y" := (forall z, z ∈ x -> z ∈ y) (at level 34) : sem.
+Notation "x ∈ y" := (@i_atom _ _ _ _ elem (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : FSTsem.
+Notation "x ≡ y" := (@i_atom _ _ _ _ equal (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : FSTsem.
+Notation "x ⊆ y" := (forall z, z ∈ x -> z ∈ y) (at level 34) : FSTsem.
 
-Notation "∅" := (@i_func FST_func_sig ZFSignature.ZF_pred_sig _ _ eset Vector.nil) : sem.
-Notation "x ::: y " := (@i_func FST_func_sig _ _ _ adj (Vector.cons x (Vector.cons y Vector.nil))) (at level 31) : sem.
+Notation "∅" := (@i_func FST_func_sig ZFSignature.ZF_pred_sig _ _ eset Vector.nil) : FSTsem.
+Notation "x ::: y " := (@i_func FST_func_sig _ _ _ adj (Vector.cons x (Vector.cons y Vector.nil))) (at level 31) : FSTsem.
 
-Notation "{ x ; y }" := (x ::: (y ::: ∅)) (at level 31) : sem.
-Notation "'σ' x" := (x ::: x) (at level 32) : sem.
+Notation "{ x ; y }" := (x ::: (y ::: ∅)) (at level 31) : FSTsem.
+Notation "'σ' x" := (x ::: x) (at level 32) : FSTsem.
 
 
 
@@ -257,7 +257,7 @@ Proof.
     + intros v. exact (Vector.hd v = Vector.hd (Vector.tl v)).
 Defined.
 
-Open Scope sem.
+Open Scope FSTsem.
 
 Lemma hfs_model :
   forall rho, rho ⊫ FST.
diff --git a/theories/FOL/Sets/Models/HF_model.v b/theories/FOL/Sets/Models/HF_model.v
@@ -68,23 +68,23 @@ Defined.
 
 (* ** ZF-Models *)
 
-Declare Scope sem.
-Open Scope sem.
+Declare Scope HFsem.
+Open Scope HFsem.
 
 Arguments Vector.nil {_}, _.
 Arguments Vector.cons {_} _ {_} _, _ _ _ _.
 
-Notation "x ∈ y" := (@i_atom _ _ _ _ elem (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : sem.
-Notation "x ≡ y" := (@i_atom _ _ _ _ equal (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : sem.
-Notation "x ⊆ y" := (forall z, z ∈ x -> z ∈ y) (at level 34) : sem.
+Notation "x ∈ y" := (@i_atom _ _ _ _ elem (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : HFsem.
+Notation "x ≡ y" := (@i_atom _ _ _ _ equal (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : HFsem.
+Notation "x ⊆ y" := (forall z, z ∈ x -> z ∈ y) (at level 34) : HFsem.
 
-Notation "∅" := (@i_func ZF_func_sig ZF_pred_sig _ _ eset Vector.nil) : sem.
-Notation "{ x ; y }" := (@i_func ZF_func_sig _ _ _ pair (Vector.cons x (Vector.cons y Vector.nil))) (at level 31) : sem.
-Notation "⋃ x" := (@i_func ZF_func_sig _ _ _ union (Vector.cons x Vector.nil)) (at level 32) : sem.
-Notation "'PP' x" := (@i_func ZF_func_sig _ _ _ power (Vector.cons x Vector.nil)) (at level 31) : sem.
+Notation "∅" := (@i_func ZF_func_sig ZF_pred_sig _ _ eset Vector.nil) : HFsem.
+Notation "{ x ; y }" := (@i_func ZF_func_sig _ _ _ pair (Vector.cons x (Vector.cons y Vector.nil))) (at level 31) : HFsem.
+Notation "⋃ x" := (@i_func ZF_func_sig _ _ _ union (Vector.cons x Vector.nil)) (at level 32) : HFsem.
+Notation "'PP' x" := (@i_func ZF_func_sig _ _ _ power (Vector.cons x Vector.nil)) (at level 31) : HFsem.
 
-Notation "x ∪ y" := (⋃ {x; y}) (at level 32) : sem.
-Notation "'σ' x" := (x ∪ {x; x}) (at level 32) : sem.
+Notation "x ∪ y" := (⋃ {x; y}) (at level 32) : HFsem.
+Notation "'σ' x" := (x ∪ {x; x}) (at level 32) : HFsem.
 
 
 
diff --git a/theories/FOL/Sets/Models/ZF_conservativity.v b/theories/FOL/Sets/Models/ZF_conservativity.v
@@ -14,7 +14,7 @@ Import ListAutomationNotations ListAutomationHints ListAutomationInstances.
 Local Set Implicit Arguments.
 Local Unset Strict Implicit.
 
-Open Scope syn.
+Open Scope ZFsyn.
 
 Local Hint Constructors prv : core.
 
diff --git a/theories/FOL/Sets/Models/ZF_model.v b/theories/FOL/Sets/Models/ZF_model.v
@@ -8,24 +8,24 @@ From Stdlib Require Import Lia.
 
 (* ** ZF-Models *)
 
-Declare Scope sem.
-Open Scope sem.
+Declare Scope ZFsem.
+Open Scope ZFsem.
 
 Arguments Vector.nil {_}, _.
 Arguments Vector.cons {_} _ {_} _, _ _ _ _.
 
-Notation "x ∈ y" := (@i_atom _ _ _ _ elem (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : sem.
-Notation "x ≡ y" := (@i_atom _ _ _ _ equal (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : sem.
-Notation "x ⊆ y" := (forall z, z ∈ x -> z ∈ y) (at level 34) : sem.
+Notation "x ∈ y" := (@i_atom _ _ _ _ elem (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : ZFsem.
+Notation "x ≡ y" := (@i_atom _ _ _ _ equal (Vector.cons x (Vector.cons y Vector.nil))) (at level 35) : ZFsem.
+Notation "x ⊆ y" := (forall z, z ∈ x -> z ∈ y) (at level 34) : ZFsem.
 
-Notation "∅" := (@i_func ZF_func_sig ZF_pred_sig _ _ ZFSignature.eset Vector.nil) : sem.
-Notation "'ω'" := (@i_func ZF_func_sig _ _ _ ZFSignature.om Vector.nil) : sem.
-Notation "{ x ; y }" := (@i_func ZF_func_sig _ _ _ ZFSignature.pair (Vector.cons x (Vector.cons y Vector.nil))) (at level 31) : sem.
-Notation "⋃ x" := (@i_func ZF_func_sig _ _ _ ZFSignature.union (Vector.cons x Vector.nil)) (at level 32) : sem.
-Notation "'PP' x" := (@i_func ZF_func_sig _ _ _ ZFSignature.power (Vector.cons x Vector.nil)) (at level 31) : sem.
+Notation "∅" := (@i_func ZF_func_sig ZF_pred_sig _ _ ZFSignature.eset Vector.nil) : ZFsem.
+Notation "'ω'" := (@i_func ZF_func_sig _ _ _ ZFSignature.om Vector.nil) : ZFsem.
+Notation "{ x ; y }" := (@i_func ZF_func_sig _ _ _ ZFSignature.pair (Vector.cons x (Vector.cons y Vector.nil))) (at level 31) : ZFsem.
+Notation "⋃ x" := (@i_func ZF_func_sig _ _ _ ZFSignature.union (Vector.cons x Vector.nil)) (at level 32) : ZFsem.
+Notation "'PP' x" := (@i_func ZF_func_sig _ _ _ ZFSignature.power (Vector.cons x Vector.nil)) (at level 31) : ZFsem.
 
-Notation "x ∪ y" := (⋃ {x; y}) (at level 32) : sem.
-Notation "'σ' x" := (x ∪ {x; x}) (at level 32) : sem.
+Notation "x ∪ y" := (⋃ {x; y}) (at level 32) : ZFsem.
+Notation "'σ' x" := (x ∪ {x; x}) (at level 32) : ZFsem.
 
 
 
diff --git a/theories/FOL/Sets/ZF.v b/theories/FOL/Sets/ZF.v
@@ -6,8 +6,8 @@ Require Export Undecidability.FOL.Sets.Signatures.
 Import Vector.VectorNotations.
 From Stdlib Require Import List.
 
-Declare Scope syn.
-Open Scope syn.
+Declare Scope ZFsyn.
+Open Scope ZFsyn.
 
 (* ** Signature for ZF axiomatisation, containing function symbols for set operations *)
 
@@ -17,21 +17,21 @@ Export ZFSignature.
 
 (* ** Axioms *)
 
-Notation "x ∈ y" := (atom _ ZF_pred_sig elem ([x; y])) (at level 35) : syn.
-Notation "x ≡ y" := (atom (Σ_preds := ZF_pred_sig) equal ([x; y])) (at level 35) : syn.
+Notation "x ∈ y" := (atom _ ZF_pred_sig elem ([x; y])) (at level 35) : ZFsyn.
+Notation "x ≡ y" := (atom (Σ_preds := ZF_pred_sig) equal ([x; y])) (at level 35) : ZFsyn.
 
-Notation "∅" := (func ZF_func_sig eset ([])) : syn.
-Notation "'ω'" := (func ZF_func_sig om ([])) : syn.
-Notation "{ x ; y }" := (func ZF_func_sig pair ([x; y])) (at level 31) : syn.
-Notation "⋃ x" := (func ZF_func_sig union ([x])) (at level 32) : syn.
-Notation "'PP' x" := (func ZF_func_sig power ([x])) (at level 31) : syn.
-Notation "x ∪ y" := (⋃ {x; y}) (at level 32) : syn.
-Notation  "'σ' x" := (x ∪ {x; x}) (at level 32) : syn.
+Notation "∅" := (func ZF_func_sig eset ([])) : ZFsyn.
+Notation "'ω'" := (func ZF_func_sig om ([])) : ZFsyn.
+Notation "{ x ; y }" := (func ZF_func_sig pair ([x; y])) (at level 31) : ZFsyn.
+Notation "⋃ x" := (func ZF_func_sig union ([x])) (at level 32) : ZFsyn.
+Notation "'PP' x" := (func ZF_func_sig power ([x])) (at level 31) : ZFsyn.
+Notation "x ∪ y" := (⋃ {x; y}) (at level 32) : ZFsyn.
+Notation  "'σ' x" := (x ∪ {x; x}) (at level 32) : ZFsyn.
 
 Definition sub x y :=
   ∀ $0 ∈ x`[↑] → $0 ∈ y`[↑].
 
-Notation "x ⊆ y" := (sub x y) (at level 34) : syn.
+Notation "x ⊆ y" := (sub x y) (at level 34) : ZFsyn.
 
 Definition ax_ext :=
   ∀ ∀ $1 ⊆ $0 → $0 ⊆ $1 → $1 ≡ $0.
@@ -132,5 +132,3 @@ Inductive ZFeq : form -> Prop :=
 | ZFeq_base phi : In phi ZFeq' -> ZFeq phi
 | ZFeq_sep phi : ZFeq (ax_sep phi)
 | ZFeq_rep phi : ZFeq (ax_rep phi).
-
-
diff --git a/theories/FOL/Sets/binFST.v b/theories/FOL/Sets/binFST.v
diff --git a/theories/FOL/Sets/binZF.v b/theories/FOL/Sets/binZF.v
diff --git a/theories/FOL/Sets/minZF.v b/theories/FOL/Sets/minZF.v
diff --git a/theories/FOL/Syntax/Core.v b/theories/FOL/Syntax/Core.v
diff --git a/theories/FOL/Utils/FriedmanTranslation.v b/theories/FOL/Utils/FriedmanTranslation.v
diff --git a/theories/FOL/Utils/FriedmanTranslationFragment.v b/theories/FOL/Utils/FriedmanTranslationFragment.v
diff --git a/theories/FOL/ZF_undec.v b/theories/FOL/ZF_undec.v
diff --git a/theories/FOL/binZF.v b/theories/FOL/binZF.v
diff --git a/theories/_CoqProject b/theories/_CoqProject
