uds-psl · DmxLarchey · Jan 22, 2025 · Oct 3, 2023 · Oct 6, 2023 · Oct 6, 2023
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/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/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/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).

diff --git a/theories/MinskyMachines/MMA/mma_utils_bsm.v b/theories/MinskyMachines/MMA/mma_utils_bsm.v
@@ -15,14 +15,13 @@ 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 "!".
 
 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).
 #[local] Notation "P // s ->> t" := (sss_compute (@mma_sss _) P s t).
 

diff --git a/theories/MinskyMachines/MMenv/env.v b/theories/MinskyMachines/MMenv/env.v
@@ -13,9 +13,9 @@ From Undecidability.Shared.Libs.DLW.Utils
 Set Implicit Arguments.
 
 Reserved Notation " e '⇢' x " (at level 58).
-Reserved Notation " e [ v / x ] " (at level 57, v at level 0, x at level 0, 
+Reserved Notation " e [ v / x ] " (at level 1, v at level 0, x at level 0, 
                                    left associativity, format "e [ v / x ]").
-Reserved Notation " e ⦃  x '⇠' v ⦄ " (at level 57, v at level 0, x at level 0, left associativity).
+Reserved Notation " e ⦃  x '⇠' v ⦄ " (at level 1, v at level 0, x at level 0, left associativity).
 
 Section env.
 

diff --git a/theories/MinskyMachines/Reductions/BSM_computable_to_MM_computable.v b/theories/MinskyMachines/Reductions/BSM_computable_to_MM_computable.v
@@ -45,9 +45,7 @@ Qed.
 Local Notation "P '/MM/' s '~~>' t" := (sss.sss_output (@mm_sss _) P s t) (at level 70, no associativity).
 Local Notation "P '/MM/' s '~~>' t" := (sss.sss_output (@mm_sss _) P s t) (at level 70, no associativity).
 
-
-Local Notation "e #> x" := (vec_pos e x).
-Local Notation "e [ v / x ]" := (vec_change e x v).
+Import vec_notations.
 
 Lemma vec_app_spec {X n m} (v : Vector.t X n) (w : Vector.t X m) :
   vec_app v w = Vector.append v w.

diff --git a/theories/MinskyMachines/Reductions/KrivineMclosed_HALT_to_MMA_HALTING.v b/theories/MinskyMachines/Reductions/KrivineMclosed_HALT_to_MMA_HALTING.v
@@ -30,6 +30,8 @@ From Stdlib Require Import ssreflect ssrbool ssrfun.
 
 Import L (term, var, app, lam).
 
+(* Import vec_notations. *)
+
 Set Default Goal Selector "!".
 
 Module Argument.
@@ -42,8 +44,6 @@ Module Argument.
 
 #[local] Notation "P // s ->> t" := (sss_compute (@mma_sss 5) P s t).
 #[local] Notation "P // s -+> t" := (sss_progress (@mma_sss 5) P s t).
-#[local] Notation "e #> x" := (vec_pos e x).
-#[local] Notation "e [ v / x ]" := (vec_change e x v).
 
 #[local] Arguments vec_change_neq {X n v p q x}.
 #[local] Arguments vec_change_eq {X n v p q x}.
@@ -120,22 +120,22 @@ Qed.
 (* uses uniform subproc concat structure *)
 Lemma concat_sss_compute_trans {Ps : list (list mm_instr)} {offset} (i : nat) {v st st'} :
   let j := length (concat (firstn i Ps)) in
-  (j + offset, nth i Ps []) // (j + offset, v) ->> st' ->
+  (j + offset, nth i Ps nil) // (j + offset, v) ->> st' ->
   (offset, concat Ps) // st' ->> st ->
   (offset, concat Ps) // (j + offset, v) ->> st.
 Proof.
   move=> j H. apply: sss_compute_trans.
   have : ({(j + offset, v) = st'} + {(j + offset, v) <> st'}).
   { do ? decide equality. apply: vec_eq_dec. by apply: Nat.eq_dec. }
   move=> [<-|H']. { by apply: sss_compute_refl. }
-  apply: (subcode_sss_compute (P := (_, nth i Ps []))).
+  apply: (subcode_sss_compute (P := (_, nth i Ps nil))).
   - exists (concat (firstn i Ps)), (concat (skipn (S i) Ps)).
     split; last done.
-    have -> : nth i Ps [] = concat [nth i Ps []].
+    have -> : nth i Ps nil = concat (nth i Ps nil :: nil).
     { by rewrite /concat app_nil_r. }
     rewrite -?concat_app. congr concat.
     rewrite [LHS](esym (firstn_skipn i Ps)). congr List.app.
-    have : nth i Ps [] <> [].
+    have : nth i Ps nil <> nil.
     { move=> H''. move: H. rewrite H''.
       move=> [[|k]].
       - by move=> /sss_steps_0_inv.