From 75aaafec883de3196e102805be4fb6c2ca6b8b8e Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Mon, 6 May 2024 04:03:06 -0400
Subject: [PATCH 1/4] Finish Realizability for PER

---
 theories/Core/Semantic/PERLemmas.v |   9 +++
 theories/Core/Semantic/Realize.v   | 107 +++++++++++++++++++++++++++++
 theories/_CoqProject               |   1 +
 3 files changed, 117 insertions(+)
 create mode 100644 theories/Core/Semantic/Realize.v

diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index da0b3d87..5d5ae200 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -63,6 +63,15 @@ Qed.
 #[export]
 Hint Resolve per_bot_trans : mcltt.
 
+Lemma var_per_bot : forall {n},
+    {{ Dom !n ≈ !n ∈ per_bot }}.
+Proof.
+  intros n s. repeat econstructor.
+Qed.
+
+#[export]
+Hint Resolve var_per_bot : mcltt.
+
 Lemma per_top_sym : forall m n,
     {{ Dom m ≈ n ∈ per_top }} ->
     {{ Dom n ≈ m ∈ per_top }}.
diff --git a/theories/Core/Semantic/Realize.v b/theories/Core/Semantic/Realize.v
new file mode 100644
index 00000000..f1a78be6
--- /dev/null
+++ b/theories/Core/Semantic/Realize.v
@@ -0,0 +1,107 @@
+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.
+
+Lemma per_nat_then_per_top : forall {n m},
+    {{ Dom n ≈ m ∈ per_nat }} ->
+    {{ Dom ⇓ ℕ n ≈ ⇓ ℕ m ∈ per_top }}.
+Proof.
+  induction 1; simpl in *; intros.
+  - eexists; firstorder econstructor.
+  - specialize (IHper_nat s) as [? []].
+    eexists; firstorder (econstructor; eauto).
+  - specialize (H s) as [? []].
+    eexists; firstorder (econstructor; eauto).
+Qed.
+
+#[export]
+Hint Resolve per_nat_then_per_top : mcltt.
+
+Section Per_univ_elem_realize.
+  Variable (i : nat) (rec_per_univ_then_per_top_typ : forall j, j < i -> forall a a' R, {{ DF a ≈ a' ∈ per_univ_elem j ↘ R }} -> {{ Dom a ≈ a' ∈ per_top_typ }}).
+
+  Lemma realize_per_univ_elem_gen : forall 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 }})
+      /\ (forall {b b'}, {{ Dom b ≈ b' ∈ R }} -> {{ Dom ⇓ a b ≈ ⇓ a' b' ∈ per_top }}).
+  Proof with (solve [(((eexists; split) || idtac; econstructor) || idtac); mauto]) using i rec_per_univ_then_per_top_typ.
+    intros * H; simpl in H.
+    induction H using per_univ_elem_ind; repeat split; intros.
+    - subst; intro s...
+    - eexists.
+      per_univ_elem_econstructor.
+      eauto.
+    - intro s.
+      firstorder.
+      assert {{ Dom b ≈ b' ∈ per_top_typ }} as top_typ_b_b' by (eapply rec_per_univ_then_per_top_typ; eassumption).
+      specialize (top_typ_b_b' s); destruct_all...
+    - intro s...
+    - idtac...
+    - eauto using per_nat_then_per_top.
+    - specialize (IHper_univ_elem rec_per_univ_then_per_top_typ) as [? []].
+      intro s.
+      assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
+      destruct_rel_mod_eval.
+      specialize (H10 rec_per_univ_then_per_top_typ) as [? []].
+      specialize (H10 (S s)) as [? []].
+      specialize (H3 s) as [? []]...
+    - rewrite H2; clear H2.
+      intros c0 c0' equiv_c0_c0'.
+      specialize (IHper_univ_elem rec_per_univ_then_per_top_typ) as [? []].
+      destruct_rel_mod_eval.
+      specialize (H9 rec_per_univ_then_per_top_typ) as [? []].
+      econstructor; try solve [econstructor; eauto].
+      enough ({{ Dom c ⇓ A c0 ≈ c' ⇓ A' c0' ∈ per_bot }}) by mauto.
+      intro s.
+      specialize (H3 s) as [? [? ?]].
+      specialize (H5 _ _ equiv_c0_c0' s) as [? [? ?]]...
+    - rewrite H2 in *; clear H2.
+      specialize (IHper_univ_elem rec_per_univ_then_per_top_typ) as [? []].
+      intro s.
+      assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
+      destruct_rel_mod_eval.
+      specialize (H10 rec_per_univ_then_per_top_typ) as [? []].
+      destruct_rel_mod_app.
+      assert {{ Dom ⇓ a fa ≈ ⇓ a' f'a' ∈ per_top }} by mauto.
+      specialize (H2 s) as [? []].
+      specialize (H16 (S s)) as [? []]...
+    - intro s.
+      specialize (H s) as [? []]...
+    - idtac...
+    - intro s.
+      specialize (H s) as [? []].
+      inversion_clear H0.
+      specialize (H2 s) as [? []]...
+  Qed.
+End Per_univ_elem_realize.
+
+Equations per_univ_then_per_top_typ (i : nat) : forall a a' R, {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} -> {{ Dom a ≈ a' ∈ per_top_typ }} by wf i :=
+| i => fun _ _ _ H => proj1 (realize_per_univ_elem_gen i (fun {j} lt_j_i => per_univ_then_per_top_typ j) _ _ _ H).
+Arguments per_univ_then_per_top_typ {_ _ _ _}.
+
+#[export]
+Hint Resolve per_univ_then_per_top_typ : mcltt.
+
+Lemma per_bot_then_per_elem : forall {i a a' R c c'},
+    {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
+    {{ Dom c ≈ c' ∈ per_bot }} -> {{ Dom ⇑ a c ≈ ⇑ a' c' ∈ R }}.
+Proof.
+  intros.
+  eapply realize_per_univ_elem_gen; mauto.
+Qed.
+
+(** We cannot add [per_bot_then_per_elem] as a hint
+    because we don't know what "R" is (i.e. the pattern becomes higher-order.)
+    In fact, Coq complains it cannot add one if we try. *)
+
+Lemma per_elem_then_per_top : forall {i a a' R b b'},
+    {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
+    {{ Dom b ≈ b' ∈ R }} -> {{ Dom ⇓ a b ≈ ⇓ a' b' ∈ per_top }}.
+Proof.
+  intros.
+  eapply realize_per_univ_elem_gen; mauto.
+Qed.
+
+#[export]
+Hint Resolve per_elem_then_per_top : mcltt.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index 98ccc535..d927a428 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -11,6 +11,7 @@
 ./Core/Semantic/PERLemmas.v
 ./Core/Semantic/Readback.v
 ./Core/Semantic/ReadbackLemmas.v
+./Core/Semantic/Realize.v
 ./Core/Syntactic/CtxEquiv.v
 ./Core/Syntactic/Presup.v
 ./Core/Syntactic/Relations.v

From d25ed453190934fcb38503aecfac0442e9668f82 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 6 May 2024 11:20:26 -0400
Subject: [PATCH 2/4] remove unnecessary wf induction

---
 theories/Core/Semantic/Realize.v | 31 ++++++++++++++-----------------
 1 file changed, 14 insertions(+), 17 deletions(-)

diff --git a/theories/Core/Semantic/Realize.v b/theories/Core/Semantic/Realize.v
index f1a78be6..d8be0abe 100644
--- a/theories/Core/Semantic/Realize.v
+++ b/theories/Core/Semantic/Realize.v
@@ -18,50 +18,45 @@ Qed.
 Hint Resolve per_nat_then_per_top : mcltt.
 
 Section Per_univ_elem_realize.
-  Variable (i : nat) (rec_per_univ_then_per_top_typ : forall j, j < i -> forall a a' R, {{ DF a ≈ a' ∈ per_univ_elem j ↘ R }} -> {{ Dom a ≈ a' ∈ per_top_typ }}).
-
-  Lemma realize_per_univ_elem_gen : forall 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 }})
       /\ (forall {b b'}, {{ Dom b ≈ b' ∈ R }} -> {{ Dom ⇓ a b ≈ ⇓ a' b' ∈ per_top }}).
-  Proof with (solve [(((eexists; split) || idtac; econstructor) || idtac); mauto]) using i rec_per_univ_then_per_top_typ.
+  Proof with (solve [(((eexists; split) || idtac; econstructor) || idtac); mauto]).
     intros * H; simpl in H.
     induction H using per_univ_elem_ind; repeat split; intros.
     - subst; intro s...
     - eexists.
       per_univ_elem_econstructor.
       eauto.
-    - intro s.
-      firstorder.
-      assert {{ Dom b ≈ b' ∈ per_top_typ }} as top_typ_b_b' by (eapply rec_per_univ_then_per_top_typ; eassumption).
-      specialize (top_typ_b_b' s); destruct_all...
+    - destruct H2.
+      specialize (H1 _ _ _ H2) as [? [? ?]].
+      intro s.
+      specialize (H1 s) as [? [? ?]]...
     - intro s...
     - idtac...
     - eauto using per_nat_then_per_top.
-    - specialize (IHper_univ_elem rec_per_univ_then_per_top_typ) as [? []].
+    - destruct IHper_univ_elem as [? []].
       intro s.
       assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
       destruct_rel_mod_eval.
-      specialize (H10 rec_per_univ_then_per_top_typ) as [? []].
       specialize (H10 (S s)) as [? []].
       specialize (H3 s) as [? []]...
     - rewrite H2; clear H2.
       intros c0 c0' equiv_c0_c0'.
-      specialize (IHper_univ_elem rec_per_univ_then_per_top_typ) as [? []].
+      destruct IHper_univ_elem as [? []].
       destruct_rel_mod_eval.
-      specialize (H9 rec_per_univ_then_per_top_typ) as [? []].
       econstructor; try solve [econstructor; eauto].
       enough ({{ Dom c ⇓ A c0 ≈ c' ⇓ A' c0' ∈ per_bot }}) by mauto.
       intro s.
       specialize (H3 s) as [? [? ?]].
       specialize (H5 _ _ equiv_c0_c0' s) as [? [? ?]]...
     - rewrite H2 in *; clear H2.
-      specialize (IHper_univ_elem rec_per_univ_then_per_top_typ) as [? []].
+      destruct IHper_univ_elem as [? []].
       intro s.
       assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
       destruct_rel_mod_eval.
-      specialize (H10 rec_per_univ_then_per_top_typ) as [? []].
       destruct_rel_mod_app.
       assert {{ Dom ⇓ a fa ≈ ⇓ a' f'a' ∈ per_top }} by mauto.
       specialize (H2 s) as [? []].
@@ -76,9 +71,11 @@ Section Per_univ_elem_realize.
   Qed.
 End Per_univ_elem_realize.
 
-Equations per_univ_then_per_top_typ (i : nat) : forall a a' R, {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} -> {{ Dom a ≈ a' ∈ per_top_typ }} by wf i :=
-| i => fun _ _ _ H => proj1 (realize_per_univ_elem_gen i (fun {j} lt_j_i => per_univ_then_per_top_typ j) _ _ _ H).
-Arguments per_univ_then_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.
+Qed.
 
 #[export]
 Hint Resolve per_univ_then_per_top_typ : mcltt.

From ae57eb3ba5cba5d543c6bf743c47d16f0b80fe10 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Mon, 6 May 2024 11:52:02 -0400
Subject: [PATCH 3/4] Remove unneccesary section

---
 theories/Core/Semantic/Realize.v | 104 +++++++++++++++----------------
 1 file changed, 51 insertions(+), 53 deletions(-)

diff --git a/theories/Core/Semantic/Realize.v b/theories/Core/Semantic/Realize.v
index d8be0abe..5151b1bc 100644
--- a/theories/Core/Semantic/Realize.v
+++ b/theories/Core/Semantic/Realize.v
@@ -17,59 +17,57 @@ Qed.
 #[export]
 Hint Resolve per_nat_then_per_top : mcltt.
 
-Section Per_univ_elem_realize.
-  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 }})
-      /\ (forall {b b'}, {{ Dom b ≈ b' ∈ R }} -> {{ Dom ⇓ a b ≈ ⇓ a' b' ∈ per_top }}).
-  Proof with (solve [(((eexists; split) || idtac; econstructor) || idtac); mauto]).
-    intros * H; simpl in H.
-    induction H using per_univ_elem_ind; repeat split; intros.
-    - subst; intro s...
-    - eexists.
-      per_univ_elem_econstructor.
-      eauto.
-    - destruct H2.
-      specialize (H1 _ _ _ H2) as [? [? ?]].
-      intro s.
-      specialize (H1 s) as [? [? ?]]...
-    - intro s...
-    - idtac...
-    - eauto using per_nat_then_per_top.
-    - destruct IHper_univ_elem as [? []].
-      intro s.
-      assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
-      destruct_rel_mod_eval.
-      specialize (H10 (S s)) as [? []].
-      specialize (H3 s) as [? []]...
-    - rewrite H2; clear H2.
-      intros c0 c0' equiv_c0_c0'.
-      destruct IHper_univ_elem as [? []].
-      destruct_rel_mod_eval.
-      econstructor; try solve [econstructor; eauto].
-      enough ({{ Dom c ⇓ A c0 ≈ c' ⇓ A' c0' ∈ per_bot }}) by mauto.
-      intro s.
-      specialize (H3 s) as [? [? ?]].
-      specialize (H5 _ _ equiv_c0_c0' s) as [? [? ?]]...
-    - rewrite H2 in *; clear H2.
-      destruct IHper_univ_elem as [? []].
-      intro s.
-      assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
-      destruct_rel_mod_eval.
-      destruct_rel_mod_app.
-      assert {{ Dom ⇓ a fa ≈ ⇓ a' f'a' ∈ per_top }} by mauto.
-      specialize (H2 s) as [? []].
-      specialize (H16 (S s)) as [? []]...
-    - intro s.
-      specialize (H s) as [? []]...
-    - idtac...
-    - intro s.
-      specialize (H s) as [? []].
-      inversion_clear H0.
-      specialize (H2 s) as [? []]...
-  Qed.
-End Per_univ_elem_realize.
+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 }})
+    /\ (forall {b b'}, {{ Dom b ≈ b' ∈ R }} -> {{ Dom ⇓ a b ≈ ⇓ a' b' ∈ per_top }}).
+Proof with (solve [(((eexists; split) || idtac; econstructor) || idtac); mauto]).
+  intros * H; simpl in H.
+  induction H using per_univ_elem_ind; repeat split; intros.
+  - subst; intro s...
+  - eexists.
+    per_univ_elem_econstructor.
+    eauto.
+  - destruct H2.
+    specialize (H1 _ _ _ H2) as [? [? ?]].
+    intro s.
+    specialize (H1 s) as [? [? ?]]...
+  - intro s...
+  - idtac...
+  - eauto using per_nat_then_per_top.
+  - destruct IHper_univ_elem as [? []].
+    intro s.
+    assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
+    destruct_rel_mod_eval.
+    specialize (H10 (S s)) as [? []].
+    specialize (H3 s) as [? []]...
+  - rewrite H2; clear H2.
+    intros c0 c0' equiv_c0_c0'.
+    destruct IHper_univ_elem as [? []].
+    destruct_rel_mod_eval.
+    econstructor; try solve [econstructor; eauto].
+    enough ({{ Dom c ⇓ A c0 ≈ c' ⇓ A' c0' ∈ per_bot }}) by mauto.
+    intro s.
+    specialize (H3 s) as [? [? ?]].
+    specialize (H5 _ _ equiv_c0_c0' s) as [? [? ?]]...
+  - rewrite H2 in *; clear H2.
+    destruct IHper_univ_elem as [? []].
+    intro s.
+    assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
+    destruct_rel_mod_eval.
+    destruct_rel_mod_app.
+    assert {{ Dom ⇓ a fa ≈ ⇓ a' f'a' ∈ per_top }} by mauto.
+    specialize (H2 s) as [? []].
+    specialize (H16 (S s)) as [? []]...
+  - intro s.
+    specialize (H s) as [? []]...
+  - idtac...
+  - intro s.
+    specialize (H s) as [? []].
+    inversion_clear H0.
+    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 }}.
 Proof.

From 62b06f396c510c3e00e30d8fa87c0744b499bc1c Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Mon, 6 May 2024 11:54:07 -0400
Subject: [PATCH 4/4] Use "try" instead of "or idtac"

---
 theories/Core/Semantic/Realize.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Core/Semantic/Realize.v b/theories/Core/Semantic/Realize.v
index 5151b1bc..83f85b98 100644
--- a/theories/Core/Semantic/Realize.v
+++ b/theories/Core/Semantic/Realize.v
@@ -22,7 +22,7 @@ Lemma realize_per_univ_elem_gen : forall i a a' R,
     {{ Dom a ≈ a' ∈ per_top_typ }}
     /\ (forall {c c'}, {{ Dom c ≈ c' ∈ per_bot }} -> {{ Dom ⇑ a c ≈ ⇑ a' c' ∈ R }})
     /\ (forall {b b'}, {{ Dom b ≈ b' ∈ R }} -> {{ Dom ⇓ a b ≈ ⇓ a' b' ∈ per_top }}).
-Proof with (solve [(((eexists; split) || idtac; econstructor) || idtac); mauto]).
+Proof with (solve [try (try (eexists; split); econstructor); mauto]).
   intros * H; simpl in H.
   induction H using per_univ_elem_ind; repeat split; intros.
   - subst; intro s...