From 6f029e3efe592a3f53217a29f57ffafc1c98f5fb Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Mon, 6 May 2024 13:53:57 -0400
Subject: [PATCH] Some refactoring (#62)

* Rename modules

* Change minor formatting
---
 theories/Core/Semantic/{Evaluate.v => Evaluation.v}       | 0
 .../Semantic/{EvaluateLemmas.v => EvaluationLemmas.v}     | 2 +-
 theories/Core/Semantic/PER.v                              | 2 +-
 theories/Core/Semantic/PERLemmas.v                        | 2 +-
 theories/Core/Semantic/Readback.v                         | 6 +-----
 theories/Core/Semantic/ReadbackLemmas.v                   | 2 +-
 theories/Core/Semantic/{Realize.v => Realizability.v}     | 8 +++++---
 theories/_CoqProject                                      | 6 +++---
 8 files changed, 13 insertions(+), 15 deletions(-)
 rename theories/Core/Semantic/{Evaluate.v => Evaluation.v} (100%)
 rename theories/Core/Semantic/{EvaluateLemmas.v => EvaluationLemmas.v} (98%)
 rename theories/Core/Semantic/{Realize.v => Realizability.v} (91%)

diff --git a/theories/Core/Semantic/Evaluate.v b/theories/Core/Semantic/Evaluation.v
similarity index 100%
rename from theories/Core/Semantic/Evaluate.v
rename to theories/Core/Semantic/Evaluation.v
diff --git a/theories/Core/Semantic/EvaluateLemmas.v b/theories/Core/Semantic/EvaluationLemmas.v
similarity index 98%
rename from theories/Core/Semantic/EvaluateLemmas.v
rename to theories/Core/Semantic/EvaluationLemmas.v
index fe19d14f..5f35068f 100644
--- a/theories/Core/Semantic/EvaluateLemmas.v
+++ b/theories/Core/Semantic/EvaluationLemmas.v
@@ -1,5 +1,5 @@
 From Coq Require Import Lia PeanoNat Relations.
-From Mcltt Require Import Base Domain Evaluate LibTactics Syntax System.
+From Mcltt Require Import Base Domain Evaluation LibTactics Syntax System.
 
 Section functional_eval.
   Let functional_eval_exp_prop M p m1 (_ : {{ ⟦ M ⟧ p ↘ m1 }}) : Prop := forall m2 (Heval2: {{ ⟦ M ⟧ p ↘ m2 }}), m1 = m2.
diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v
index 3306b417..47519369 100644
--- a/theories/Core/Semantic/PER.v
+++ b/theories/Core/Semantic/PER.v
@@ -1,6 +1,6 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
-From Mcltt Require Import Base Domain Evaluate LibTactics Readback Syntax System.
+From Mcltt Require Import Base Domain Evaluation LibTactics Readback Syntax System.
 
 Notation "'Dom' a ≈ b ∈ R" := ((R a b : Prop) : Prop) (in custom judg at level 90, a custom domain, b custom domain, R constr).
 Notation "'DF' a ≈ b ∈ R ↘ R'" := ((R a b R' : Prop) : Prop) (in custom judg at level 90, a custom domain, b custom domain, R constr, R' constr).
diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index 5d5ae200..35102bd5 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -1,5 +1,5 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
-From Mcltt Require Import Axioms Base Domain Evaluate EvaluateLemmas LibTactics PER Readback ReadbackLemmas Syntax System.
+From Mcltt Require Import Axioms Base Domain Evaluation EvaluationLemmas LibTactics PER Readback ReadbackLemmas Syntax System.
 
 (* Lemma rel_mod_eval_ex_pull : *)
 (*   forall (A : Type) (P : domain -> domain -> relation domain -> A -> Prop) {T p T' p'} R, *)
diff --git a/theories/Core/Semantic/Readback.v b/theories/Core/Semantic/Readback.v
index d9f809ee..ddd839ae 100644
--- a/theories/Core/Semantic/Readback.v
+++ b/theories/Core/Semantic/Readback.v
@@ -1,8 +1,4 @@
-From Mcltt Require Import Base.
-From Mcltt Require Import Domain.
-From Mcltt Require Import Evaluate.
-From Mcltt Require Import Syntax.
-From Mcltt Require Import System.
+From Mcltt Require Import Base Domain Evaluation Syntax System.
 
 Reserved Notation "'Rnf' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).
 Reserved Notation "'Rne' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).
diff --git a/theories/Core/Semantic/ReadbackLemmas.v b/theories/Core/Semantic/ReadbackLemmas.v
index 58470fff..d1909e7e 100644
--- a/theories/Core/Semantic/ReadbackLemmas.v
+++ b/theories/Core/Semantic/ReadbackLemmas.v
@@ -1,5 +1,5 @@
 From Coq Require Import Lia PeanoNat Relations.
-From Mcltt Require Import Base Domain Evaluate EvaluateLemmas LibTactics Readback Syntax System.
+From Mcltt Require Import Base Domain Evaluation EvaluationLemmas LibTactics Readback Syntax System.
 
 Section functional_read.
   Let functional_read_nf_prop s m M1 (_ : {{ Rnf m in s ↘ M1 }}) : Prop := forall M2 (Hread2: {{ Rnf m in s ↘ M2 }}), M1 = M2.
diff --git a/theories/Core/Semantic/Realize.v b/theories/Core/Semantic/Realizability.v
similarity index 91%
rename from theories/Core/Semantic/Realize.v
rename to theories/Core/Semantic/Realizability.v
index 83f85b98..5106d4e7 100644
--- a/theories/Core/Semantic/Realize.v
+++ b/theories/Core/Semantic/Realizability.v
@@ -1,6 +1,6 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions.
 From Equations Require Import Equations.
-From Mcltt Require Import Base Domain Evaluate EvaluateLemmas LibTactics PER PERLemmas Syntax System.
+From Mcltt Require Import Base Domain Evaluation EvaluationLemmas LibTactics PER PERLemmas Syntax System.
 
 Lemma per_nat_then_per_top : forall {n m},
     {{ Dom n ≈ m ∈ per_nat }} ->
@@ -17,7 +17,7 @@ Qed.
 #[export]
 Hint Resolve per_nat_then_per_top : mcltt.
 
-Lemma realize_per_univ_elem_gen : forall i a a' R,
+Lemma realize_per_univ_elem_gen : forall {i a a' R},
     {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
     {{ Dom a ≈ a' ∈ per_top_typ }}
     /\ (forall {c c'}, {{ Dom c ≈ c' ∈ per_bot }} -> {{ Dom ⇑ a c ≈ ⇑ a' c' ∈ R }})
@@ -69,7 +69,9 @@ Proof with (solve [try (try (eexists; split); econstructor); mauto]).
     specialize (H2 s) as [? []]...
 Qed.
 
-Lemma per_univ_then_per_top_typ : forall i a a' R, {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} -> {{ Dom a ≈ a' ∈ per_top_typ }}.
+Lemma per_univ_then_per_top_typ : forall {i a a' R},
+    {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
+    {{ Dom a ≈ a' ∈ per_top_typ }}.
 Proof.
   intros.
   eapply realize_per_univ_elem_gen; mauto.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index d927a428..92fc6677 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -5,13 +5,13 @@
 ./Core/Axioms.v
 ./Core/Base.v
 ./Core/Semantic/Domain.v
-./Core/Semantic/Evaluate.v
-./Core/Semantic/EvaluateLemmas.v
+./Core/Semantic/Evaluation.v
+./Core/Semantic/EvaluationLemmas.v
 ./Core/Semantic/PER.v
 ./Core/Semantic/PERLemmas.v
 ./Core/Semantic/Readback.v
 ./Core/Semantic/ReadbackLemmas.v
-./Core/Semantic/Realize.v
+./Core/Semantic/Realizability.v
 ./Core/Syntactic/CtxEquiv.v
 ./Core/Syntactic/Presup.v
 ./Core/Syntactic/Relations.v