Fix errors in Semantics

theories/Core/Semantic/Domain.v

@@ -25,7 +25,7 @@ where "'env'" := (nat -> domain).
 #[global] Declare Custom Entry domain.
 #[global] Bind Scope exp_scope with domain.
 
-Notation "'d{{{' x '}}}'" := x (at level 0, x custom domain at level 99) : exp_scope.
+Notation "'d{{{' x '}}}'" := x (at level 0, x custom domain at level 99, format "'d{{{'  x  '}}}'") : exp_scope.
 Notation "( x )" := x (in custom domain at level 0, x custom domain at level 60) : exp_scope.
 Notation "~ x" := x (in custom domain at level 0, x constr at level 0) : exp_scope.
 Notation "x" := x (in custom domain at level 0, x global) : exp_scope.

theories/Core/Semantic/Evaluate.v

@@ -14,7 +14,7 @@ Inductive eval_exp : exp -> env -> domain -> Prop :=
 | eval_exp_typ :
   `( {{ ⟦ Type@i ⟧ p ↘ 𝕌@i }} )
 | eval_exp_nat :
-  `( {{ ⟦ ℕ ⟧ p ↘ 𝕟 }} )
+  `( {{ ⟦ ℕ ⟧ p ↘ ℕ }} )
 | eval_exp_zero :
   `( {{ ⟦ zero ⟧ p ↘ zero }} )
 | eval_exp_succ :
@@ -49,16 +49,16 @@ with eval_natrec : exp -> exp -> exp -> domain -> env -> domain -> Prop :=
      {{ rec succ b ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ms }} )
 | eval_natrec_neut :
   `( {{ ⟦ MZ ⟧ p ↘ mz }} ->
-     {{ ⟦ A ⟧ p ↦ ⇑ 𝕟 m ↘ a }} ->
-     {{ rec ⇑ 𝕟 m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ⇑ a (rec m under p return A | zero -> mz | succ -> MS end) }} )
+     {{ ⟦ A ⟧ p ↦ ⇑ ℕ m ↘ a }} ->
+     {{ rec ⇑ ℕ m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ⇑ a (rec m under p return A | zero -> mz | succ -> MS end) }} )
 where "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" := (eval_natrec A MZ MS m p r) (in custom judg)
 with eval_app : domain -> domain -> domain -> Prop :=
 | eval_app_fn :
   `( {{ ⟦ M ⟧ p ↦ n ↘ m }} ->
      {{ $| λ p M & n |↘ m }} )
 | eval_app_neut :
   `( {{ ⟦ B ⟧ p ↦ n ↘ b }} ->
-     {{ $| ⇑ (Π a p B) m & n |↘ ⇑ b (m (⇓ a N)) }} )
+     {{ $| ⇑ (Π a p B) m & n |↘ ⇑ b (m (⇓ a n)) }} )
 where "'$|' m '&' n '|↘' r" := (eval_app m n r) (in custom judg)
 with eval_sub : sub -> env -> env -> Prop :=
 | eval_sub_id :
@@ -75,3 +75,8 @@ with eval_sub : sub -> env -> env -> Prop :=
      {{ ⟦ σ ∘ τ ⟧s p ↘ p'' }} )
 where "'⟦' σ '⟧s' p '↘' p'" := (eval_sub σ p p') (in custom judg)
 .
+
+Scheme eval_exp_mut_ind := Induction for eval_exp Sort Prop
+with eval_natrec_mut_ind := Induction for eval_natrec Sort Prop
+with eval_app_mut_ind := Induction for eval_app Sort Prop
+with eval_sub_mut_ind := Induction for eval_sub Sort Prop.

theories/_CoqProject

@@ -5,6 +5,9 @@
 ./Core/Base.v
 ./Core/Semantic/Domain.v
 ./Core/Semantic/Evaluate.v
+./Core/Semantic/EvaluateLemma.v
+./Core/Semantic/PER.v
+./Core/Semantic/PERLemmas.v
 ./Core/Semantic/Readback.v
 ./Core/Syntactic/CtxEquiv.v
 ./Core/Syntactic/Presup.v