From 381567c58edf15bc2d4121f85251e44aceec95d8 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 14 May 2024 23:53:54 -0400
Subject: [PATCH] intermediate commit

---
 theories/Core/Completeness/LogicalRelation.v  |  2 +-
 theories/Core/Semantic/PER/Definitions.v      |  3 +-
 theories/Core/Semantic/PER/Lemmas.v           |  3 +-
 theories/Core/Semantic/Readback/Definitions.v |  2 +-
 theories/Core/Semantic/Readback/Lemmas.v      |  3 +-
 theories/Core/Semantic/Realizability.v        |  4 +-
 theories/Extraction/Evaluation.v              | 88 ++++++++++++++-----
 theories/_CoqProject                          |  1 +
 8 files changed, 75 insertions(+), 31 deletions(-)

diff --git a/theories/Core/Completeness/LogicalRelation.v b/theories/Core/Completeness/LogicalRelation.v
index c71c7c24..e13e3a51 100644
--- a/theories/Core/Completeness/LogicalRelation.v
+++ b/theories/Core/Completeness/LogicalRelation.v
@@ -1,6 +1,6 @@
 From Coq Require Import Relations.
 From Mcltt Require Import Base.
-From Mcltt Require Export Evaluation PER.
+From Mcltt.Core Require Export Evaluation PER.
 Import Domain_Notations.
 
 Inductive rel_exp (R : relation domain) M p M' p' : Prop :=
diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index 1323d94c..be76cff2 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -1,6 +1,7 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
-From Mcltt Require Import Base Evaluation LibTactics Readback.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Evaluation Readback.
 From Mcltt Require Export Domain.
 Import Domain_Notations.
 
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index 9be5418a..9018b381 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -1,5 +1,6 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
-From Mcltt Require Import Axioms Base Evaluation LibTactics PER.Definitions Readback.
+From Mcltt Require Import Axioms Base LibTactics.
+From Mcltt.Core Require Import Evaluation PER.Definitions Readback.
 Import Domain_Notations.
 
 Lemma per_bot_sym : forall m n,
diff --git a/theories/Core/Semantic/Readback/Definitions.v b/theories/Core/Semantic/Readback/Definitions.v
index ba94c3e0..86085756 100644
--- a/theories/Core/Semantic/Readback/Definitions.v
+++ b/theories/Core/Semantic/Readback/Definitions.v
@@ -1,4 +1,4 @@
-From Mcltt Require Import Base Evaluation.
+From Mcltt.Core Require Import Base Evaluation.
 From Mcltt Require Export Domain.
 Import Domain_Notations.
 
diff --git a/theories/Core/Semantic/Readback/Lemmas.v b/theories/Core/Semantic/Readback/Lemmas.v
index f4f3f870..dc94e60e 100644
--- a/theories/Core/Semantic/Readback/Lemmas.v
+++ b/theories/Core/Semantic/Readback/Lemmas.v
@@ -1,5 +1,6 @@
 From Coq Require Import Lia PeanoNat Relations.
-From Mcltt Require Import Base Evaluation LibTactics Readback.Definitions.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Evaluation Readback.Definitions.
 Import Domain_Notations.
 
 Section functional_read.
diff --git a/theories/Core/Semantic/Realizability.v b/theories/Core/Semantic/Realizability.v
index 54b0936a..9ea5064c 100644
--- a/theories/Core/Semantic/Realizability.v
+++ b/theories/Core/Semantic/Realizability.v
@@ -1,7 +1,7 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions.
 From Equations Require Import Equations.
-From Mcltt Require Import Base Evaluation LibTactics Readback.
-From Mcltt Require Export PER.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Export PER Evaluation Readback.
 Import Domain_Notations.
 
 Lemma per_nat_then_per_top : forall {n m},
diff --git a/theories/Extraction/Evaluation.v b/theories/Extraction/Evaluation.v
index b023db71..b9966837 100644
--- a/theories/Extraction/Evaluation.v
+++ b/theories/Extraction/Evaluation.v
@@ -1,5 +1,5 @@
-From Mcltt Require Import Base.
-From Mcltt Require Import Evaluation.Definitions.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Evaluation.
 Import Domain_Notations.
 
 Generalizable All Variables.
@@ -18,25 +18,65 @@ Inductive eval_exp_order : exp -> env -> Prop :=
   `( eval_exp_order {{{ M }}} p ->
      eval_exp_order {{{ succ M }}} p )
 | eeo_natrec :
-  `( {{ eval_exp_order M p }} ->
-     {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
-     eval_exp_order {{{ rec M return A | zero -> MZ | succ -> MS end }}} p ).
-
-| eval_exp_natrec :
-  `( {{ ⟦ M ⟧ p ↘ m }} ->
-     {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
-     {{ ⟦ rec M return A | zero -> MZ | succ -> MS end ⟧ p ↘ r }} )
-| eval_exp_pi :
-  `( {{ ⟦ A ⟧ p ↘ a }} ->
-     {{ ⟦ Π A B ⟧ p ↘ Π a p B }} )
-| eval_exp_fn :
-  `( {{ ⟦ λ A M ⟧ p ↘ λ p M }} )
-| eval_exp_app :
-  `( {{ ⟦ M ⟧ p ↘ m }} ->
-     {{ ⟦ N ⟧ p ↘ n }} ->
-     {{ $| m & n |↘ r }} ->
-     {{ ⟦ M N ⟧ p ↘ r }} )
-| eval_exp_sub :
-  `( {{ ⟦ σ ⟧s p ↘ p' }} ->
-     {{ ⟦ M ⟧ p' ↘ m }} ->
-     {{ ⟦ M[σ] ⟧ p ↘ m }} )
+  `( eval_exp_order M p ->
+     (forall m, {{ ⟦ M ⟧ p ↘ m }} -> eval_natrec_order A MZ MS m p) ->
+     eval_exp_order {{{ rec M return A | zero -> MZ | succ -> MS end }}} p )
+| eeo_pi :
+  `( eval_exp_order A p ->
+     eval_exp_order {{{ Π A B }}} p )
+| eeo_fn :
+  `( eval_exp_order {{{ λ A M }}} p )
+| eeo_app :
+  `( eval_exp_order M p ->
+     eval_exp_order N p ->
+     (forall m n, {{ ⟦ M ⟧ p ↘ m }} -> {{ ⟦ N ⟧ p ↘ n }} -> eval_app_order m n) ->
+     eval_exp_order {{{ M N }}} p )
+| eeo_sub :
+  `( eval_sub_order σ p ->
+     (forall p', {{ ⟦ σ ⟧s p ↘ p' }} -> eval_exp_order M p') ->
+     eval_exp_order {{{ M[σ] }}} p )
+
+with eval_natrec_order : exp -> exp -> exp -> domain -> env -> Prop :=
+| eno_zero :
+  `( eval_exp_order MZ p ->
+     eval_natrec_order A MZ MS zero p )
+| eno_succ :
+  `( eval_natrec_order A MZ MS b p ->
+     (forall r, {{ rec b ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} -> eval_exp_order {{{ MS }}} d{{{ p ↦ b ↦ r }}}) ->
+     eval_natrec_order A MZ MS d{{{ succ b }}} p )
+| eno_neut :
+  `( eval_exp_order MZ p ->
+     eval_exp_order A d{{{ p ↦ ⇑ ℕ m }}} ->
+     eval_natrec_order A MZ MS d{{{ ⇑ ℕ m }}} p )
+
+with eval_app_order : domain -> domain -> Prop :=
+| eao_fn :
+  `( eval_exp_order M d{{{ p ↦ n }}} ->
+     eval_app_order d{{{ λ p M }}} n )
+| eao_neut :
+  `( eval_exp_order B d{{{ p ↦ n }}} ->
+     eval_app_order d{{{ ⇑ (Π a p B) m }}} n )
+
+with eval_sub_order : sub -> env -> Prop :=
+| eso_id :
+  `( eval_sub_order {{{ Id }}} p )
+| eso_weaken :
+  `( eval_sub_order {{{ Wk }}} p )
+| eso_extend :
+  `( eval_sub_order σ p ->
+     eval_exp_order M p ->
+     eval_sub_order {{{ σ ,, M }}} p )
+| eso_compose :
+  `( eval_sub_order τ p ->
+     (forall p', {{ ⟦ τ ⟧s p ↘ p' }} -> eval_sub_order σ p') ->
+     eval_sub_order {{{ σ ∘ τ }}} p ).
+
+#[export]
+  Hint Constructors eval_exp_order eval_natrec_order eval_app_order eval_sub_order : mcltt.
+
+
+Lemma eval_exp_order_sound : forall m p a,
+    {{ ⟦ m ⟧ p ↘ a }} ->
+    eval_exp_order m p.
+Proof.
+  induction 1; econstructor; mauto.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index c3e016f1..5d1f352e 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -28,4 +28,5 @@
 ./Frontend/Elaborator.v
 ./Frontend/Parser.v
 ./Frontend/ParserExtraction.v
+./Extraction/Evaluation.v
 ./LibTactics.v