From 5ee6cf522564d6cde81674cc7f7748a3c9a07e5b Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Tue, 30 Apr 2024 02:03:27 -0400
Subject: [PATCH] Fix errors in Semantics

---
 theories/Core/Semantic/Domain.v   |  2 +-
 theories/Core/Semantic/Evaluate.v | 13 +++++++++----
 theories/_CoqProject              |  2 ++
 3 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/theories/Core/Semantic/Domain.v b/theories/Core/Semantic/Domain.v
index 4813dd28..4abd670f 100644
--- a/theories/Core/Semantic/Domain.v
+++ b/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.
diff --git a/theories/Core/Semantic/Evaluate.v b/theories/Core/Semantic/Evaluate.v
index c40c3d07..ef8acfe1 100644
--- a/theories/Core/Semantic/Evaluate.v
+++ b/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,8 +49,8 @@ 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 :
@@ -58,7 +58,7 @@ with eval_app : domain -> domain -> domain -> Prop :=
      {{ $| λ 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.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index 82f5e936..741ddd62 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -5,6 +5,8 @@
 ./Core/Base.v
 ./Core/Semantic/Domain.v
 ./Core/Semantic/Evaluate.v
+./Core/Semantic/PER.v
+./Core/Semantic/PERLemmas.v
 ./Core/Semantic/Readback.v
 ./Core/Syntactic/CtxEquiv.v
 ./Core/Syntactic/Presup.v