removed the (globality of the) notation "[ f ; v ] ▹ x" for (ra_bs f …

…v x)

(ie big step semantics for recalg) because of incompatibilities with
ListNotations. Notice that the notation is kept ONLY (locally) for
the definition of ra_bs to make it more readable.

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, 

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.

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.

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.