From 3b32b8b335264ab08c818b99c59f7a7443873f20 Mon Sep 17 00:00:00 2001
From: DmxLarchey <larchey@gmail.com>
Date: Thu, 23 Jan 2025 08:22:06 +0100
Subject: [PATCH] =?UTF-8?q?removed=20the=20(globality=20of=20the)=20notati?=
 =?UTF-8?q?on=20"[=20f=20;=20v=20]=20=E2=96=B9=20x"=20for=20(ra=5Fbs=20f?=
 =?UTF-8?q?=20v=20x)=20(ie=20big=20step=20semantics=20for=20recalg)=20beca?=
 =?UTF-8?q?use=20of=20incompatibilities=20with=20ListNotations.=20Notice?=
 =?UTF-8?q?=20that=20the=20notation=20is=20kept=20ONLY=20(locally)=20for?=
 =?UTF-8?q?=20the=20definition=20of=20ra=5Fbs=20to=20make=20it=20more=20re?=
 =?UTF-8?q?adable.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/MuRec/MuRec.v                 | 14 +++++++++-----
 theories/MuRec/Util/MuRec_computable.v |  1 -
 theories/MuRec/Util/ra_sem_eq.v        |  8 ++++----
 theories/MuRec/Util/recalg.v           |  4 ++--
 4 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/theories/MuRec/MuRec.v b/theories/MuRec/MuRec.v
index 8eb8448a0..974fe6992 100644
--- a/theories/MuRec/MuRec.v
+++ b/theories/MuRec/MuRec.v
@@ -1,4 +1,4 @@
-From Stdlib Require Import Arith Lia List Bool Eqdep_dec .
+From Stdlib Require Import Arith Lia List Bool Eqdep_dec.
 
 From Undecidability.Shared.Libs.DLW 
   Require Import utils_tac utils_nat utils_list finite pos vec.
@@ -24,9 +24,11 @@ Inductive recalg : nat -> Type :=
 
 Set Elimination Schemes.
 
-Reserved Notation "  '[' f ';' v ']' '▹' x " (at level 70).
+Section recalg_big_step_sem.
 
-Inductive ra_bs : forall k, recalg k -> vec nat k -> nat -> Prop :=
+  Reserved Notation "[ f ; v ] ▹ x " (at level 70, format "[ f ; v ]  ▹  x").
+
+  Inductive ra_bs : forall {k}, recalg k -> vec nat k -> nat -> Prop :=
     | in_ra_bs_cst  : forall n v,             [ra_cst n;        v] ▹ n
     | in_ra_bs_zero : forall v,               [ra_zero;         v] ▹ 0
     | in_ra_bs_succ : forall v,               [ra_succ;         v] ▹ S (vec_head v)
@@ -50,10 +52,12 @@ Inductive ra_bs : forall k, recalg k -> vec nat k -> nat -> Prop :=
                            (forall j : pos x, [f;    pos2nat j##v] ▹ S (vec_pos w j))
                                ->             [f;            x##v] ▹ 0
                                ->             [ra_min f;        v] ▹ x
-where " [ f ; v ] ▹ x " := (@ra_bs _ f v x).
+  where " [ f ; v ] ▹ x " := (@ra_bs _ f v x).
+
+End recalg_big_step_sem.
 
 Definition Halt_murec (a : { n : nat & recalg n & Vector.t nat n }) : Prop :=
-    let (n, f, v) := a in exists x, [f ; v ] ▹ x.
+  let (n, f, v) := a in exists x, ra_bs f v x.
 
 Definition MuRec_computable {k} (R : Vector.t nat k -> nat -> Prop) := 
   exists f : recalg k, forall v : Vector.t nat k, 
diff --git a/theories/MuRec/Util/MuRec_computable.v b/theories/MuRec/Util/MuRec_computable.v
index 2931255fe..54878eb58 100644
--- a/theories/MuRec/Util/MuRec_computable.v
+++ b/theories/MuRec/Util/MuRec_computable.v
@@ -1,7 +1,6 @@
 From Undecidability.MuRec Require Export MuRec.
 
 From Stdlib Require Import List Vector Nat.
-Import ListNotations Vector.VectorNotations.
 
 Definition functional {X Y} (R : X -> Y -> Prop) :=
   forall x y1 y2, R x y1 -> R x y2 -> y1 = y2.
diff --git a/theories/MuRec/Util/ra_sem_eq.v b/theories/MuRec/Util/ra_sem_eq.v
index 6d131d339..a74f3479f 100644
--- a/theories/MuRec/Util/ra_sem_eq.v
+++ b/theories/MuRec/Util/ra_sem_eq.v
@@ -15,13 +15,13 @@ From Undecidability.MuRec.Util
 
 Set Implicit Arguments.
 
-Notation "[| f |]" := (@ra_rel _ f) (at level 0).
+Local Notation "[| f |]" := (@ra_rel _ f) (at level 0).
 
 Section soundness_and_completeness.
 
   (* By induction on the ra_ca predicate *)
 
-  Lemma ra_ca_inc_bs k (f : recalg k) v x : (exists n, [f;v] -[n>> x) -> [f;v] ▹ x.
+  Lemma ra_ca_inc_bs k (f : recalg k) v x : (exists n, [f;v] -[n>> x) -> ra_bs f v x.
   Proof.
     intros (n & H); revert H.
     induction 1 as [ n v | v | v
@@ -37,7 +37,7 @@ Section soundness_and_completeness.
 
   (* By induction on the ra_bs predicate *)
 
-  Lemma ra_bs_inc_rel k (f : recalg k) v x : [f;v] ▹ x -> [|f|] v x.
+  Lemma ra_bs_inc_rel k (f : recalg k) v x : ra_bs f v x -> [|f|] v x.
   Proof.
     induction 1 as [ n v | v | v
                    | k v p 
@@ -109,7 +109,7 @@ Section soundness_and_completeness.
 
   Hint Resolve ra_ca_inc_bs ra_bs_inc_rel ra_rel_inc_ca : core.
   
-  Theorem ra_bs_correct k (f : recalg k) v x : [|f|] v x <-> [f;v] ▹ x.
+  Theorem ra_bs_correct k (f : recalg k) v x : [|f|] v x <-> ra_bs f v x.
   Proof. split; auto. Qed.
 
   Theorem ra_ca_correct k (f : recalg k) v x : [|f|] v x <-> exists n, [f;v] -[n>> x.
diff --git a/theories/MuRec/Util/recalg.v b/theories/MuRec/Util/recalg.v
index a3e7b63c6..0d9388b55 100644
--- a/theories/MuRec/Util/recalg.v
+++ b/theories/MuRec/Util/recalg.v
@@ -383,10 +383,10 @@ Section relational_semantics.
   Qed.
 
   Lemma ra_rel_spec {k} (f : recalg k) v m :
-    [| f |] v m <-> [f; v] ▹ m.
+    [| f |] v m <-> ra_bs f v m.
   Proof.
     split.
-    - revert k f v m. apply (recalg_ind (fun k f => forall v m, [|f|] v m -> [f; v] ▹ m)); cbn.
+    - revert k f v m. apply (recalg_ind (fun k f => forall v m, [|f|] v m -> ra_bs f v m)); cbn.
       + intros ??? <-. now constructor.
       + intros ?? ->. now constructor.
       + intros ?? ->. now constructor.