Some refactoring

theories/Core/Semantic/EvaluateLemmas.v → 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.

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).

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, *)

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).

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.

theories/Core/Semantic/Realize.v → 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.

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