Test PR related to Issue 228 (#229)

* relicense to MPL-2.0 using a script * changing license field in opam file, thx to @Zimmi48 * renamed MPL-2.0 license file for GitHub automatic recognition * try some changes of priority for notation with a trailing terminal symbol * moved the vec_pos and vec_change notations into the Module vec_notations which is imported where needed. The Reserved Notations _ #> _ and _ [ _ / _ ] are not global anymore ... * update L_computable_closed_to_MMA_computable.v * solved issue related to level 0 bi-closed notations * added a local warning suppression for the "terminates" notation "_ // _ ↓" which is postfix so expected at level 1 by Coq/Rocq --------- Co-authored-by: Andrej Dudenhefner <[email protected]>
uds-psl · Jan 22, 2025 · 6eae942 · 6eae942
1 parent ccb6e86
commit 6eae942
Show file tree

Hide file tree

Showing 45 changed files with 104 additions and 133 deletions.
diff --git a/theories/FOL/TRAKHTENBROT/discrete.v b/theories/FOL/TRAKHTENBROT/discrete.v
@@ -18,13 +18,10 @@ From Undecidability.Shared.Libs.DLW.Vec
 From Undecidability.FOL.TRAKHTENBROT
   Require Import notations decidable gfp fol_ops fo_sig fo_terms fo_logic fo_definable fo_sat.
 
-Import fol_notations.
+Import fol_notations vec_notations.
 
 Set Implicit Arguments.
 
-Local Notation " e '#>' x " := (vec_pos e x).
-Local Notation " e [ v / x ] " := (vec_change e x v).
-
 (* ∈ and ⊆ are already used for object level syntax at too low level 59 *)
 
 Local Infix "∊" := In (at level 70, no associativity).
@@ -646,7 +643,7 @@ Section counter_model_to_class_FO_definability.
 
   (* A projection of M onto itself which swaps α/β *)
 
-  Let f : @fo_projection Σ [] [tt] _ M _ M.
+  Let f : @fo_projection Σ nil (tt::nil) _ M _ M.
   Proof.
     exists negb negb; simpl.
     + abstract now intros [].
@@ -662,7 +659,7 @@ Section counter_model_to_class_FO_definability.
     all: intros []; simpl; auto.
   Qed.
 
-  Infix "≐" := (fo_bisimilar (Σ := Σ) nil [tt] M) (at level 70, no associativity).
+  Infix "≐" := (fo_bisimilar (Σ := Σ) nil (tt::nil) M) (at level 70, no associativity).
 
   Hint Resolve finite_t_bool : core.
 
@@ -700,12 +697,12 @@ Section counter_model_to_class_FO_definability.
 
   Theorem FO_does_not_characterize_classes :
      exists (M : fo_model Σ bool) (_ : fo_model_dec M) (a b : bool), 
-              (forall x y, fo_bisimilar (Σ := Σ) nil [tt] M x y <-> x = y)
+              (forall x y, fo_bisimilar (Σ := Σ) nil (tt::nil) M x y <-> x = y)
            /\ (forall x y φ ρ, fol_vars φ ⊑ [0] -> M,x·ρ ⊨ φ <-> M,y·ρ ⊨ φ)
            /\ exists ξ, fol_vars ξ ⊑ [0;1] /\ forall ρ, M,a·a·ρ ⊨ ξ /\ ~ M,b·a·ρ ⊨ ξ.
   Proof. 
     exists M, M_dec, true, false; msplit 2; auto. 
-    exists (fo_bisimilar_formula (Σ := Σ) nil [tt] finite_t_bool M_dec); split.
+    exists (fo_bisimilar_formula (Σ := Σ) nil (tt::nil) finite_t_bool M_dec); split.
     + apply fo_bisimilar_formula_vars.
     + intro; rewrite !fo_bisimilar_formula_sem; split; auto; intro; tauto.
   Qed.

diff --git a/theories/FRACTRAN/FRACTRAN/mm_fractran.v b/theories/FRACTRAN/FRACTRAN/mm_fractran.v
@@ -22,13 +22,12 @@ From Undecidability.Shared.Libs.DLW
 From Undecidability.MinskyMachines.MM Require Import mm_defs mm_no_self.
 From Undecidability.FRACTRAN Require Import FRACTRAN fractran_utils prime_seq FRACTRAN_sss.
 
+Import vec_notations.
+
 Set Implicit Arguments.
 
 Tactic Notation "rew" "length" := autorewrite with length_db. 
 
-Local Notation "e #> x" := (vec_pos e x).
-Local Notation "e [ v / x ]" := (vec_change e x v).
-
 Local Notation "I // s -1> t" := (mm_sss I s t).
 Local Notation "P /MM/ s → t" := (sss_step (@mm_sss _) P s t) (at level 70, no associativity). 
 Local Notation "P /MM/ s -[ k ]-> t" := (sss_steps (@mm_sss _) P k s t) (at level 70, no associativity).

diff --git a/theories/FRACTRAN/Util/prime_seq.v b/theories/FRACTRAN/Util/prime_seq.v
@@ -16,10 +16,7 @@ From Stdlib Require Import List Arith Lia Bool Permutation.
 From Undecidability.Shared.Libs.DLW 
   Require Import utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec.
 
-Set Implicit Arguments.
-
-Local Notation "e #> x" := (vec_pos e x).
-Local Notation "e [ v / x ]" := (vec_change e x v).
+Import vec_notations.
 
 Set Implicit Arguments.
 

diff --git a/theories/H10/Dio/dio_logic.v b/theories/H10/Dio/dio_logic.v
@@ -95,7 +95,7 @@ Local Notation "x ≐ y ⨢ z" := (df_add x y z)
 Local Notation "x ≐ y ⨰ z" := (df_mul x y z) 
       (at level 49, no associativity, y at next level, format "x  ≐  y  ⨰  z").
 
-Local Reserved Notation "'⟦' t '⟧'" (at level 1, format "⟦ t ⟧").
+Local Reserved Notation "'⟦' t '⟧'" (at level 0, format "⟦ t ⟧").
 Local Reserved Notation "f '⦃' σ '⦄'" (at level 1, format "f ⦃ σ ⦄").
 
 Section diophantine_logic_basics.

diff --git a/theories/H10/Fractran/fractran_dio.v b/theories/H10/Fractran/fractran_dio.v
@@ -122,7 +122,7 @@ Section exp_diophantine.
      has a diophantine representation *)
 
   Fact fractran_exp_diophantine n : 𝔻F (fun ν => ps 1 * exp 1 (fun2vec 0 n ν)).
-  Proof. dio auto. Show Proof. Defined.
+  Proof. dio auto. Defined.
 
   Fact fractran_exp_diophantine' n : 𝔻F (fun ν => ps 1 * exp 2 (fun2vec 1 n ν⭳)).
   Proof. eapply dio_fun_mult. dio auto. eapply exp_dio_lift. Qed.

diff --git a/theories/ILL/Ll/ill.v b/theories/ILL/Ll/ill.v
@@ -143,7 +143,7 @@ Section trivial_phase_semantics.
 
   Variables (n : nat) (s : ill_vars -> vec nat n -> Prop).
 
-  Reserved Notation "'⟦' A '⟧'" (at level 65).
+  Reserved Notation "'⟦' A '⟧'" (at level 0).
 
   Definition ill_tps_imp (X Y : _ -> Prop) (v : vec _ n) := forall x, X x -> Y (vec_plus x v).
   Definition ill_tps_mult (X Y : _ -> Prop) (x : vec _ n) := exists a b, x = vec_plus a b /\ X a /\ Y b. 

diff --git a/theories/ILL/Ll/ill_cll.v b/theories/ILL/Ll/ill_cll.v
@@ -20,8 +20,8 @@ Section mapping_ill_to_cll.
 
   (* Syntatic translations from/to ILL and CLL formulas *)
 
-  Reserved Notation "[ f ]" (at level 1).
-  Reserved Notation "⟨ f ⟩" (at level 1).
+  Reserved Notation "[ f ]" (at level 0).
+  Reserved Notation "⟨ f ⟩" (at level 0).
 
   Fixpoint ill_cll f :=
     match f with

diff --git a/theories/ILL/Ll/imsell.v b/theories/ILL/Ll/imsell.v
@@ -23,7 +23,7 @@ Local Infix "~p" := (@Permutation _) (at level 70).
 Local Notation "X ⊆ Y" := (forall a, X a -> Y a : Prop) (at level 70).
 Local Infix "∊" := In (at level 70).
 
-Local Reserved Notation "'⟦' A '⟧'" (at level 1, format "⟦ A ⟧").
+Local Reserved Notation "'⟦' A '⟧'" (at level 0, format "⟦ A ⟧").
 
 Section IMSELL.
 
@@ -158,7 +158,7 @@ Section IMSELL.
         * intros ->; auto.
     Qed.
 
-    Reserved Notation "⟪ Γ ⟫" (at level 1, format "⟪ Γ ⟫").
+    Reserved Notation "⟪ Γ ⟫" (at level 0, format "⟪ Γ ⟫").
 
     Fixpoint imsell_tps_list Γ :=
       match Γ with
@@ -208,7 +208,7 @@ Section IMSELL.
 
     Definition imsell_sequent_tps Γ A := ⟪Γ⟫ -⊛ ⟦A⟧.
 
-    Notation "'[<' Γ '|-' A '>]'" := (imsell_sequent_tps Γ A) (at level 1, format "[<  Γ  |-  A  >]").
+    Notation "'[<' Γ '|-' A '>]'" := (imsell_sequent_tps Γ A) (at level 0, format "[<  Γ  |-  A  >]").
 
     Fact imsell_sequent_tps_mono Γ A B :
            ⟦A⟧ ⊆ ⟦B⟧ -> [< Γ |- A >] ⊆ [< Γ |- B >].

diff --git a/theories/ILL/Reductions/ndMM2_IMSELL.v b/theories/ILL/Reductions/ndMM2_IMSELL.v
@@ -27,7 +27,7 @@ Local Infix "~p" := (@Permutation _) (at level 70).
 Local Notation "X ⊆ Y" := (forall a, X a -> Y a : Prop) (at level 70).
 Local Infix "∊" := In (at level 70).
 
-Local Reserved Notation "'⟦' A '⟧'" (at level 1, format "⟦ A ⟧").
+Local Reserved Notation "'⟦' A '⟧'" (at level 0, format "⟦ A ⟧").
 
 Local Fact pair_plus x1 y1 x2 y2 : 
           vec_plus (x1##y1##vec_nil) (x2##y2##vec_nil) 

diff --git a/theories/MinskyMachines/MM.v b/theories/MinskyMachines/MM.v
@@ -50,10 +50,10 @@ Section Minsky_Machine.
 
   Definition mm_state := (nat*vec nat n)%type.
 
-  Local Notation "e #> x" := (vec_pos e x).
-  Local Notation "e [ x := v ]" := (vec_change e x v) (no associativity, at level 50).
+  Notation "e '#>' x" := (vec_pos e x) (at level 58, format "e #> x").
+  Notation "e [ x := v ]" := (vec_change e x v) (no associativity, at level 1).
 
-  Local Reserved Notation "P // e ▷ v" (at level 50, no associativity).
+  Reserved Notation "P // e ▷ v" (at level 50, no associativity).
 
   (* Minsky machine small step semantics *)
 

diff --git a/theories/MinskyMachines/MM/mm_comp.v b/theories/MinskyMachines/MM/mm_comp.v
@@ -19,16 +19,15 @@ From Undecidability.StackMachines.BSM
 From Undecidability.MinskyMachines.MM
   Require Import mm_defs mm_utils.
 
+Import vec_notations.
+
 Set Implicit Arguments.
 Set Default Goal Selector "!".
 
 (* ** BSM reduces to MM *)
 
 Tactic Notation "rew" "length" := autorewrite with length_db.
 
-Local Notation "e #> x" := (vec_pos e x).
-Local Notation "e [ v / x ]" := (vec_change e x v).
-
 Local Notation "I '/BSM/' s -1> t" := (bsm_sss I s t) (at level 70, no associativity).
 Local Notation "P '/BSM/' s -+> t" := (sss_progress (@bsm_sss _) P s t) (at level 70, no associativity).
 Local Notation "P '/BSM/' s ->> t" := (sss_compute (@bsm_sss _) P s t) (at level 70, no associativity).

diff --git a/theories/MinskyMachines/MM/mm_comp_strong.v b/theories/MinskyMachines/MM/mm_comp_strong.v
@@ -19,6 +19,8 @@ From Undecidability.StackMachines.BSM
 From Undecidability.MinskyMachines.MM
   Require Import mm_defs mm_utils. 
 
+Import vec_notations.
+
 Set Implicit Arguments.
 
 Set Default Proof Using "Type".
@@ -27,9 +29,6 @@ Set Default Proof Using "Type".
 
 Tactic Notation "rew" "length" := autorewrite with length_db.
 
-Local Notation "e #> x" := (vec_pos e x).
-Local Notation "e [ v / x ]" := (vec_change e x v).
-
 Local Notation "I '/BSM/' s -1> t" := (bsm_sss I s t) (at level 70, no associativity).
 Local Notation "P '/BSM/' s -+> t" := (sss_progress (@bsm_sss _) P s t) (at level 70, no associativity).
 Local Notation "P '/BSM/' s ->> t" := (sss_compute (@bsm_sss _) P s t) (at level 70, no associativity).

diff --git a/theories/MinskyMachines/MM/mm_defs.v b/theories/MinskyMachines/MM/mm_defs.v
@@ -15,13 +15,12 @@ From Undecidability.Shared.Libs.DLW
 From Undecidability.MinskyMachines
   Require Export MM MM_sss.
 
+Import vec_notations.
+
 Set Implicit Arguments.
 
 Tactic Notation "rew" "length" := autorewrite with length_db.
 
-Local Notation "e #> x" := (vec_pos e x).
-Local Notation "e [ v / x ]" := (vec_change e x v).
-
 Section Minsky_Machine.
 
   Variable (n : nat).

diff --git a/theories/MinskyMachines/MM/mm_no_self.v b/theories/MinskyMachines/MM/mm_no_self.v
@@ -18,13 +18,12 @@ From Undecidability.Shared.Libs.DLW
 From Undecidability.MinskyMachines.MM
   Require Import mm_defs.
 
+Import vec_notations.
+
 Set Implicit Arguments.
 
 Tactic Notation "rew" "length" := autorewrite with length_db.
 
-Local Notation "e #> x" := (vec_pos e x).
-Local Notation "e [ v / x ]" := (vec_change e x v).
-
 Local Notation "I // s -1> t" := (mm_sss I s t).
 Local Notation "P // s -[ k ]-> t" := (sss_steps (@mm_sss _) P k s t).
 Local Notation "P // s -+> t" := (sss_progress (@mm_sss _) P s t).

diff --git a/theories/MinskyMachines/MM/mm_utils.v b/theories/MinskyMachines/MM/mm_utils.v
@@ -15,13 +15,12 @@ From Undecidability.Shared.Libs.DLW
 From Undecidability.MinskyMachines.MM
   Require Import mm_defs. 
 
+Import vec_notations.
+
 Set Implicit Arguments.
 
 Tactic Notation "rew" "length" := autorewrite with length_db.
 
-Local Notation "e #> x" := (vec_pos e x).
-Local Notation "e [ v / x ]" := (vec_change e x v).
-
 Local Notation "P // s -[ k ]-> t" := (sss_steps (@mm_sss _) P k s t).
 Local Notation "P // s -+> t" := (sss_progress (@mm_sss _) P s t).
 Local Notation "P // s ->> t" := (sss_compute (@mm_sss _) P s t).

diff --git a/theories/MinskyMachines/MM2.v b/theories/MinskyMachines/MM2.v
@@ -45,7 +45,8 @@ Inductive mm2_instr : Set :=
 Reserved Notation "i '//' r '⇢' s" (at level 70, no associativity).
 Reserved Notation "P '//' r '→' s" (at level 70, no associativity).
 Reserved Notation "P '//' r '↠' s" (at level 70, no associativity).
-Reserved Notation "P '//' r ↓" (at level 70, no associativity).
+#[warning="-postfix-notation-not-level-1"]
+  Reserved Notation "P '//' r ↓" (at level 70, no associativity).
 
 #[local] Notation mm2_state := (nat*(nat*nat))%type.
 

diff --git a/theories/MinskyMachines/MMA.v b/theories/MinskyMachines/MMA.v
@@ -57,15 +57,15 @@ Section Minsky_Machine.
 
   Definition mm_state := (nat*vec nat n)%type.
 
-  Local Notation "e #> x" := (vec_pos e x).
-  Local Notation "e [ v / x ]" := (vec_change e x v).
+  Notation "e '#>' x" := (vec_pos e x) (at level 58, format "e #> x").
+  Notation "e [ x := v ]" := (vec_change e x v) (no associativity, at level 1).
 
   (* Minsky machine alternate small step semantics *)
 
   Inductive mma_sss : mm_instr (pos n) -> mm_state -> mm_state -> Prop :=
-    | in_mma_sss_inc   : forall i x v,                   INCₐ x   // (i,v) -1> (1+i,v[(S (v#>x))/x])
+    | in_mma_sss_inc   : forall i x v,                   INCₐ x   // (i,v) -1> (1+i,v[x:=S (v#>x)])
     | in_mma_sss_dec_0 : forall i x k v,   v#>x = O   -> DECₐ x k // (i,v) -1> (1+i,v)
-    | in_mma_sss_dec_1 : forall i x k v u, v#>x = S u -> DECₐ x k // (i,v) -1> (k,v[u/x])
+    | in_mma_sss_dec_1 : forall i x k v u, v#>x = S u -> DECₐ x k // (i,v) -1> (k,v[x:=u])
   where "i // s -1> t" := (mma_sss i s t).
 
 End Minsky_Machine.

diff --git a/theories/MinskyMachines/MMA/bsm_mma.v b/theories/MinskyMachines/MMA/bsm_mma.v
@@ -18,16 +18,15 @@ From Undecidability.StackMachines.BSM
 From Undecidability.MinskyMachines.MMA
   Require Import mma_defs mma_utils_bsm.
 
+Import vec_notations.
+
 Set Implicit Arguments.
 Set Default Goal Selector "!".
 
 (* ** BSM(n) reduces to MMA(1+n) *)
 
 Tactic Notation "rew" "length" := autorewrite with length_db.
 
-#[local] Notation "e #> x" := (vec_pos e x).
-#[local] Notation "e [ v / x ]" := (vec_change e x v).
-
 #[local] Notation "I '/BSM/' s -1> t" := (bsm_sss I s t) (at level 70, no associativity).
 #[local] Notation "P '/MMA/' s -+> t" := (sss_progress (@mma_sss _) P s t) (at level 70, no associativity).
 

diff --git a/theories/MinskyMachines/MMA/fractran_mma.v b/theories/MinskyMachines/MMA/fractran_mma.v
@@ -18,12 +18,12 @@ From Undecidability.MinskyMachines.MMA
 From Undecidability.FRACTRAN
   Require Import FRACTRAN fractran_utils.
 
+Import vec_notations.
+
 Set Implicit Arguments.
 
 Tactic Notation "rew" "length" := autorewrite with length_db.
 
-Local Notation "e #> x" := (vec_pos e x).
-Local Notation "e [ v / x ]" := (vec_change e x v).
 Local Notation ø := vec_nil.
 
 Local Notation "P //ₐ s -+> t" := (sss_progress (@mma_sss _) P s t) (at level 70, no associativity).

diff --git a/theories/MinskyMachines/MMA/mma3_mma2_compiler.v b/theories/MinskyMachines/MMA/mma3_mma2_compiler.v
@@ -15,9 +15,9 @@ From Undecidability.Shared.Libs.DLW
 From Undecidability.MinskyMachines.MMA
   Require Import mma_defs mma_k_mma_2_compiler.
 
-Set Default Goal Selector "!".
+Import vec_notations.
 
-#[local] Notation "e #> x" := (vec_pos e x).
+Set Default Goal Selector "!".
 
 Section mma3_mma2_compiler.
 

diff --git a/theories/MinskyMachines/MMA/mma_defs.v b/theories/MinskyMachines/MMA/mma_defs.v
@@ -14,13 +14,12 @@ From Undecidability.Shared.Libs.DLW
 
 From Undecidability.MinskyMachines Require Export MM MMA.
 
+Import vec_notations.
+
 Set Implicit Arguments.
 
 Tactic Notation "rew" "length" := autorewrite with length_db.
 
-Local Notation "e #> x" := (vec_pos e x).
-Local Notation "e [ v / x ]" := (vec_change e x v).
-
 Section Minsky_Machine_alternate.
 
   Variable (n : nat).

diff --git a/theories/MinskyMachines/MMA/mma_k_mma_2_compiler.v b/theories/MinskyMachines/MMA/mma_k_mma_2_compiler.v
@@ -15,12 +15,11 @@ From Undecidability.Shared.Libs.DLW
 From Undecidability.MinskyMachines.MMA
   Require Import mma_defs mma_utils.
 
+Import vec_notations.
+
 Set Implicit Arguments.
 Set Default Goal Selector "!".
 
-#[local] Notation "e #> x" := (vec_pos e x).
-#[local] Notation "e [ v / x ]" := (vec_change e x v).
-
 Section mma_k_mma_2_compiler.
 
   Variable (k : nat) (gc : godel_coding k) (n : nat).

diff --git a/theories/MinskyMachines/MMA/mma_simul.v b/theories/MinskyMachines/MMA/mma_simul.v
@@ -15,13 +15,12 @@ From Undecidability.Shared.Libs.DLW
 From Undecidability.MinskyMachines.MMA
   Require Import mma_defs mma_utils.
 
+Import vec_notations.
+
 Set Implicit Arguments.
 
 Tactic Notation "rew" "length" := autorewrite with length_db.
 
-Local Notation "e #> x" := (vec_pos e x).
-Local Notation "e [ v / x ]" := (vec_change e x v).
-
 Local Notation "P //ₐ s -+> t" := (sss_progress (@mma_sss _) P s t) (at level 70, no associativity).
 Local Notation "P //ₐ s ->> t" := (sss_compute (@mma_sss _) P s t) (at level 70, no associativity).
 Local Notation "P //ₐ s ~~> t" := (sss_output (@mma_sss _) P s t) (at level 70, no associativity).

diff --git a/theories/MinskyMachines/MMA/mma_utils.v b/theories/MinskyMachines/MMA/mma_utils.v
@@ -15,13 +15,12 @@ From Undecidability.Shared.Libs.DLW
 From Undecidability.MinskyMachines.MMA
   Require Import mma_defs.
 
+Import vec_notations.
+
 Set Implicit Arguments.
 
 Tactic Notation "rew" "length" := autorewrite with length_db.
 
-Local Notation "e #> x" := (vec_pos e x).
-Local Notation "e [ v / x ]" := (vec_change e x v).
-
 Local Notation "P // s -[ k ]-> t" := (sss_steps (@mma_sss _) P k s t).
 Local Notation "P // s -+> t" := (sss_progress (@mma_sss _) P s t).
 Local Notation "P // s ->> t" := (sss_compute (@mma_sss _) P s t).