From 7c31f0675af9f300440b25a528103d9cf762393d Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Sun, 9 Jun 2024 04:27:10 -0400
Subject: [PATCH 1/3] Add optimized system

---
 .../Core/Soundness/LogicalRelation/Lemmas.v   |   4 +-
 theories/Core/Syntactic/Corollaries.v         |   8 +-
 theories/Core/Syntactic/Presup.v              |  29 +--
 theories/Core/Syntactic/System.v              |   2 +-
 theories/Core/Syntactic/System/Tactics.v      |  16 ++
 theories/Core/Syntactic/SystemOpt.v           | 234 ++++++++++++++++++
 theories/_CoqProject                          |   2 +
 7 files changed, 261 insertions(+), 34 deletions(-)
 create mode 100644 theories/Core/Syntactic/System/Tactics.v
 create mode 100644 theories/Core/Syntactic/SystemOpt.v

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index a9308400..8f5c25df 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1,6 +1,6 @@
 From Coq Require Import Morphisms Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation PER Presup CtxEq Readback Syntactic.Corollaries System.Lemmas.
+From Mcltt.Core Require Import Evaluation PER Presup CtxEq Readback Syntactic.Corollaries SystemOpt.
 
 From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions.
 From Mcltt.Core.Soundness Require Export Weakening.Lemmas.
@@ -262,7 +262,7 @@ Proof.
     eapply H2; eauto.
     assert {{ Γ ⊢ m ≈ t' : Π IT OT }} as Hty by mauto.
     assert {{ Δ ⊢ IT [ σ ] : Type @ i4 }} by mauto 3.
-    eapply wf_exp_eq_sub_cong with (Γ := Δ) in Hty; [|mauto 4].
+    eapply wf_exp_eq_sub_cong with (Γ := Δ) in Hty; [| eapply sub_eq_refl; mauto 3].
     autorewrite with mcltt in Hty.
     eapply wf_exp_eq_app_cong with (N := m') (N' := m') in Hty; try pi_univ_level_tac; [|mauto 2].
     autorewrite with mcltt in Hty.
diff --git a/theories/Core/Syntactic/Corollaries.v b/theories/Core/Syntactic/Corollaries.v
index 57227c51..586232d9 100644
--- a/theories/Core/Syntactic/Corollaries.v
+++ b/theories/Core/Syntactic/Corollaries.v
@@ -1,6 +1,6 @@
 From Coq Require Import Setoid.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import CtxEq Presup.
+From Mcltt.Core Require Import SystemOpt.
 Import Syntax_Notations.
 
 Corollary invert_id : forall Γ Δ,
@@ -20,7 +20,7 @@ Corollary sub_id_typ : forall Γ M A,
 Proof.
   intros.
   gen_presups.
-  mauto 6.
+  econstructor; mauto 4.
 Qed.
 
 #[export]
@@ -40,5 +40,7 @@ Hint Resolve invert_sub_id : mcltt.
 Add Parametric Morphism i Γ Δ t (H : {{ Δ ⊢ t : Type@i }}) : (a_sub t)
     with signature wf_sub_eq Γ Δ ==> wf_exp_eq Γ {{{ Type@i }}} as sub_typ_cong1.
 Proof.
-  intros. gen_presups. mauto 4.
+  intros.
+  gen_presups.
+  mauto 4.
 Qed.
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 1f744e05..e9a0bf5c 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -257,33 +257,6 @@ Qed.
 #[export]
 Hint Resolve presup_exp presup_exp_eq presup_sub_eq : mcltt.
 
-#[local]
-Ltac invert_wf_ctx1 H :=
-  match type of H with
-  | {{ ⊢ ~_ , ~_ }} =>
-      let H' := fresh "H" in
-      pose proof H as H';
-      progressive_invert H'
-  end.
-
-Ltac invert_wf_ctx :=
-  (on_all_hyp: fun H => invert_wf_ctx1 H);
-  clear_dups.
-
 Ltac gen_presup H := gen_presup_IH @presup_exp @presup_exp_eq @presup_sub_eq H.
 
-Ltac gen_presups := (on_all_hyp: fun H => gen_presup H); invert_wf_ctx;  clear_dups.
-
-Lemma wf_ctx_eq_extend' : forall (Γ Δ : ctx) (A : typ) (i : nat) (A' : typ),
-    {{ ⊢ Γ ≈ Δ }} ->
-    {{ Γ ⊢ A ≈ A' : Type@i }} ->
-    {{ ⊢ Γ , A ≈ Δ , A' }}.
-Proof.
-  intros. gen_presups.
-  econstructor; mauto.
-Qed.
-
-#[export]
-Hint Resolve wf_ctx_eq_extend' : mcltt.
-#[export]
-Remove Hints wf_ctx_eq_extend : mcltt.
+Ltac gen_presups := (on_all_hyp: fun H => gen_presup H); invert_wf_ctx; clear_dups.
diff --git a/theories/Core/Syntactic/System.v b/theories/Core/Syntactic/System.v
index 16ba6364..09df7bf6 100644
--- a/theories/Core/Syntactic/System.v
+++ b/theories/Core/Syntactic/System.v
@@ -1 +1 @@
-From Mcltt Require Export System.Definitions System.Lemmas.
+From Mcltt Require Export System.Definitions System.Lemmas System.Tactics.
diff --git a/theories/Core/Syntactic/System/Tactics.v b/theories/Core/Syntactic/System/Tactics.v
new file mode 100644
index 00000000..89aa7064
--- /dev/null
+++ b/theories/Core/Syntactic/System/Tactics.v
@@ -0,0 +1,16 @@
+From Mcltt Require Import Base LibTactics.
+From Mcltt Require Export System.Definitions.
+Import Syntax_Notations.
+
+#[local]
+Ltac invert_wf_ctx1 H :=
+  match type of H with
+  | {{ ⊢ ~_ , ~_ }} =>
+      let H' := fresh "H" in
+      pose proof H as H';
+      progressive_invert H'
+  end.
+
+Ltac invert_wf_ctx :=
+  (on_all_hyp: fun H => invert_wf_ctx1 H);
+  clear_dups.
diff --git a/theories/Core/Syntactic/SystemOpt.v b/theories/Core/Syntactic/SystemOpt.v
new file mode 100644
index 00000000..b417eed9
--- /dev/null
+++ b/theories/Core/Syntactic/SystemOpt.v
@@ -0,0 +1,234 @@
+From Coq Require Import Setoid.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Export CtxEq Presup System.
+Import Syntax_Notations.
+
+#[local]
+Ltac impl_opt_constructor :=
+  intros;
+  gen_presups;
+  mautosolve 4.
+
+Corollary wf_ctx_eq_extend' : forall {Γ Δ A A' i},
+    {{ ⊢ Γ ≈ Δ }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ ⊢ Γ , A ≈ Δ , A' }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_ctx_eq_extend' : mcltt.
+#[export]
+Remove Hints wf_ctx_eq_extend : mcltt.
+
+Corollary wf_natrec' : forall {Γ A MZ MS M},
+    {{ Γ ⊢ MZ : A[Id,,zero] }} ->
+    {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+    {{ Γ ⊢ M : ℕ }} ->
+    {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end : A[Id,,M] }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_natrec' : mcltt.
+#[export]
+Remove Hints wf_natrec : mcltt.
+
+Corollary wf_fn' : forall {Γ A M B},
+    {{ Γ , A ⊢ M : B }} ->
+    {{ Γ ⊢ λ A M : Π A B }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_fn' : mcltt.
+#[export]
+Remove Hints wf_fn : mcltt.
+
+Corollary wf_app' : forall {Γ M N A B i},
+    {{ Γ , A ⊢ B : Type@i }} ->
+    {{ Γ ⊢ M : Π A B }} ->
+    {{ Γ ⊢ N : A }} ->
+    {{ Γ ⊢ M N : B[Id,,N] }}.
+Proof.
+  intros.
+  gen_presups.
+  exvar nat ltac:(fun i => assert {{ Γ ⊢ A : Type@i }} by (eapply lift_exp_max_left; mauto 3)).
+  exvar nat ltac:(fun i => assert {{ Γ, A ⊢ B : Type@i }} by (eapply lift_exp_max_right; mauto 3)).
+  mautosolve 3.
+Qed.
+
+#[export]
+Hint Resolve wf_app' : mcltt.
+#[export]
+Remove Hints wf_app : mcltt.
+
+Corollary wf_exp_eq_natrec_cong' : forall {Γ A A' i MZ MZ' MS MS' M M'},
+    {{ Γ , ℕ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊢ MZ ≈ MZ' : A[Id,,zero] }} ->
+    {{ Γ , ℕ , A ⊢ MS ≈ MS' : A[Wk∘Wk,,succ(#1)] }} ->
+    {{ Γ ⊢ M ≈ M' : ℕ }} ->
+    {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end ≈ rec M' return A' | zero -> MZ' | succ -> MS' end : A[Id,,M] }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_natrec_cong' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_natrec_cong : mcltt.
+
+Corollary wf_exp_eq_natrec_sub' : forall {Γ σ Δ A MZ MS M},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ MZ : A[Id,,zero] }} ->
+    {{ Δ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+    {{ Δ ⊢ M : ℕ }} ->
+    {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end[σ] ≈ rec M[σ] return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M[σ]] }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_natrec_sub' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_natrec_sub : mcltt.
+
+Corollary wf_exp_eq_nat_beta_zero' : forall {Γ A MZ MS},
+    {{ Γ ⊢ MZ : A[Id,,zero] }} ->
+    {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+    {{ Γ ⊢ rec zero return A | zero -> MZ | succ -> MS end ≈ MZ : A[Id,,zero] }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_nat_beta_zero' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_nat_beta_zero : mcltt.
+
+Corollary wf_exp_eq_nat_beta_succ' : forall {Γ A MZ MS M},
+    {{ Γ ⊢ MZ : A[Id,,zero] }} ->
+    {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+    {{ Γ ⊢ M : ℕ }} ->
+    {{ Γ ⊢ rec (succ M) return A | zero -> MZ | succ -> MS end ≈ MS[Id,,M,,rec M return A | zero -> MZ | succ -> MS end] : A[Id,,succ M] }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_nat_beta_succ' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_nat_beta_succ : mcltt.
+
+Corollary wf_exp_eq_pi_cong' : forall {Γ A A' B B' i},
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ , A ⊢ B ≈ B' : Type@i }} ->
+    {{ Γ ⊢ Π A B ≈ Π A' B' : Type@i }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_pi_cong' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_pi_cong : mcltt.
+
+Corollary wf_exp_eq_fn_cong' : forall {Γ A A' i B M M'},
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ , A ⊢ M ≈ M' : B }} ->
+    {{ Γ ⊢ λ A M ≈ λ A' M' : Π A B }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_fn_cong' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_fn_cong : mcltt.
+
+Corollary wf_exp_eq_fn_sub' : forall {Γ σ Δ A M B},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ , A ⊢ M : B }} ->
+    {{ Γ ⊢ (λ A M)[σ] ≈ λ A[σ] M[q σ] : (Π A B)[σ] }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_fn_sub' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_fn_sub : mcltt.
+
+Corollary wf_exp_eq_app_cong' : forall {Γ A B i M M' N N'},
+    {{ Γ , A ⊢ B : Type@i }} ->
+    {{ Γ ⊢ M ≈ M' : Π A B }} ->
+    {{ Γ ⊢ N ≈ N' : A }} ->
+    {{ Γ ⊢ M N ≈ M' N' : B[Id,,N] }}.
+Proof.
+  intros.
+  gen_presups.
+  exvar nat ltac:(fun i => assert {{ Γ ⊢ A : Type@i }} by (eapply lift_exp_max_left; mauto 3)).
+  exvar nat ltac:(fun i => assert {{ Γ, A ⊢ B : Type@i }} by (eapply lift_exp_max_right; mauto 3)).
+  mautosolve 3.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_app_cong' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_app_cong : mcltt.
+
+Corollary wf_exp_eq_app_sub' : forall {Γ σ Δ A B i M N},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ , A ⊢ B : Type@i }} ->
+    {{ Δ ⊢ M : Π A B }} ->
+    {{ Δ ⊢ N : A }} ->
+    {{ Γ ⊢ (M N)[σ] ≈ M[σ] N[σ] : B[σ,,N[σ]] }}.
+Proof.
+  intros.
+  gen_presups.
+  exvar nat ltac:(fun i => assert {{ Δ ⊢ A : Type@i }} by (eapply lift_exp_max_left; mauto 3)).
+  exvar nat ltac:(fun i => assert {{ Δ, A ⊢ B : Type@i }} by (eapply lift_exp_max_right; mauto 3)).
+  mautosolve 3.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_app_sub' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_app_sub : mcltt.
+
+Corollary wf_exp_eq_pi_beta' : forall {Γ A B M N},
+    {{ Γ , A ⊢ M : B }} ->
+    {{ Γ ⊢ N : A }} ->
+    {{ Γ ⊢ (λ A M) N ≈ M[Id,,N] : B[Id,,N] }}.
+Proof.
+  intros.
+  gen_presups.
+  exvar nat ltac:(fun i => assert {{ Γ ⊢ A : Type@i }} by (eapply lift_exp_max_left; mauto 3)).
+  exvar nat ltac:(fun i => assert {{ Γ, A ⊢ B : Type@i }} by (eapply lift_exp_max_right; mauto 3)).
+  mautosolve 3.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_pi_beta' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_pi_beta : mcltt.
+
+Corollary wf_exp_eq_pi_eta' : forall {Γ A B i M},
+    {{ Γ , A ⊢ B : Type@i }} ->
+    {{ Γ ⊢ M : Π A B }} ->
+    {{ Γ ⊢ M ≈ λ A (M[Wk] #0) : Π A B }}.
+Proof.
+  intros.
+  gen_presups.
+  exvar nat ltac:(fun i => assert {{ Γ ⊢ A : Type@i }} by (eapply lift_exp_max_left; mauto 3)).
+  exvar nat ltac:(fun i => assert {{ Γ, A ⊢ B : Type@i }} by (eapply lift_exp_max_right; mauto 3)).
+  mautosolve 3.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_pi_eta' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_pi_eta : mcltt.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index 8e1ca02e..df44ad9d 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -39,6 +39,8 @@
 ./Core/Syntactic/System.v
 ./Core/Syntactic/System/Definitions.v
 ./Core/Syntactic/System/Lemmas.v
+./Core/Syntactic/System/Tactics.v
+./Core/Syntactic/SystemOpt.v
 ./Core/Soundness.v
 ./Core/Soundness/LogicalRelation.v
 ./Core/Soundness/LogicalRelation/Definitions.v

From 3aced9f08ecb3c29c1d99972b615863c23b96fb4 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Sun, 9 Jun 2024 04:38:44 -0400
Subject: [PATCH 2/3] Update imports

---
 theories/Core/Completeness.v                  |  4 ++--
 theories/Core/Completeness/ContextCases.v     |  4 ++--
 theories/Core/Completeness/FunctionCases.v    |  4 ++--
 .../Core/Completeness/FundamentalTheorem.v    |  5 ++---
 .../LogicalRelation/Definitions.v             |  2 +-
 .../Completeness/LogicalRelation/Tactics.v    |  3 +--
 theories/Core/Completeness/NatCases.v         | 19 ++++++++++---------
 .../Core/Completeness/SubstitutionCases.v     |  2 +-
 .../Core/Completeness/TermStructureCases.v    |  2 +-
 theories/Core/Completeness/VariableCases.v    |  4 ++--
 theories/Core/Semantic/NbE.v                  |  3 +--
 theories/Core/Semantic/PER/CoreTactics.v      |  2 +-
 theories/Core/Semantic/PER/Definitions.v      |  3 +--
 theories/Core/Semantic/PER/Lemmas.v           |  2 +-
 theories/Core/Semantic/Realizability.v        |  2 +-
 .../Soundness/LogicalRelation/Definitions.v   |  5 ++---
 .../Core/Soundness/LogicalRelation/Lemmas.v   |  4 ++--
 theories/Core/Soundness/Weakening/Lemmas.v    |  2 +-
 theories/Core/Syntactic/Corollaries.v         |  2 +-
 theories/Extraction/NbE.v                     |  2 +-
 theories/Extraction/TypeCheck.v               |  2 +-
 21 files changed, 37 insertions(+), 41 deletions(-)

diff --git a/theories/Core/Completeness.v b/theories/Core/Completeness.v
index ca522713..3c628b19 100644
--- a/theories/Core/Completeness.v
+++ b/theories/Core/Completeness.v
@@ -1,6 +1,6 @@
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Import Completeness.FundamentalTheorem Semantic.Realizability.
-From Mcltt.Core Require Export Completeness.LogicalRelation Semantic.NbE System.
+From Mcltt.Core Require Export Semantic.NbE SystemOpt.
 Import Domain_Notations.
 
 Theorem completeness : forall {Γ M M' A},
@@ -9,7 +9,7 @@ Theorem completeness : forall {Γ M M' A},
 Proof with mautosolve.
   intros * [env_relΓ]%completeness_fundamental_exp_eq.
   destruct_conjs.
-  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) as [p] by (apply per_ctx_then_per_env_initial_env; eauto).
+  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) as [p] by (eauto using per_ctx_then_per_env_initial_env).
   destruct_conjs.
   functional_initial_env_rewrite_clear.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
diff --git a/theories/Core/Completeness/ContextCases.v b/theories/Core/Completeness/ContextCases.v
index 6ebd799c..ff312fd7 100644
--- a/theories/Core/Completeness/ContextCases.v
+++ b/theories/Core/Completeness/ContextCases.v
@@ -1,6 +1,6 @@
-From Coq Require Import Morphisms_Relations RelationClasses.
+From Coq Require Import Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.UniverseCases System.
+From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.UniverseCases.
 Import Domain_Notations.
 
 Proposition valid_ctx_empty :
diff --git a/theories/Core/Completeness/FunctionCases.v b/theories/Core/Completeness/FunctionCases.v
index 95b88514..cc3e0e3d 100644
--- a/theories/Core/Completeness/FunctionCases.v
+++ b/theories/Core/Completeness/FunctionCases.v
@@ -1,6 +1,6 @@
-From Coq Require Import Morphisms_Relations Relation_Definitions RelationClasses.
+From Coq Require Import Morphisms_Relations Relation_Definitions.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.TermStructureCases Completeness.UniverseCases System.
+From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.TermStructureCases Completeness.UniverseCases.
 Import Domain_Notations.
 
 Lemma rel_exp_of_pi_inversion : forall {Γ M M' A B},
diff --git a/theories/Core/Completeness/FundamentalTheorem.v b/theories/Core/Completeness/FundamentalTheorem.v
index 4c262873..c43101c6 100644
--- a/theories/Core/Completeness/FundamentalTheorem.v
+++ b/theories/Core/Completeness/FundamentalTheorem.v
@@ -1,14 +1,13 @@
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Import
-  Completeness.LogicalRelation
   Completeness.ContextCases
   Completeness.FunctionCases
   Completeness.NatCases
   Completeness.SubstitutionCases
   Completeness.TermStructureCases
   Completeness.UniverseCases
-  Completeness.VariableCases
-  System.
+  Completeness.VariableCases.
+From Mcltt.Core Require Export Completeness.LogicalRelation SystemOpt.
 Import Domain_Notations.
 
 Section completeness_fundamental.
diff --git a/theories/Core/Completeness/LogicalRelation/Definitions.v b/theories/Core/Completeness/LogicalRelation/Definitions.v
index 5c7dbcce..709e551c 100644
--- a/theories/Core/Completeness/LogicalRelation/Definitions.v
+++ b/theories/Core/Completeness/LogicalRelation/Definitions.v
@@ -1,6 +1,6 @@
 From Coq Require Import Relations.
 From Mcltt Require Import Base.
-From Mcltt.Core Require Export Evaluation PER.
+From Mcltt.Core Require Export PER.
 Import Domain_Notations.
 
 Inductive rel_exp M p M' p' (R : relation domain) : Prop :=
diff --git a/theories/Core/Completeness/LogicalRelation/Tactics.v b/theories/Core/Completeness/LogicalRelation/Tactics.v
index 17667fb0..891c51df 100644
--- a/theories/Core/Completeness/LogicalRelation/Tactics.v
+++ b/theories/Core/Completeness/LogicalRelation/Tactics.v
@@ -1,6 +1,5 @@
-From Coq Require Import Morphisms_Relations RelationClasses.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation PER System.
+From Mcltt.Core Require Import PER.
 Import Domain_Notations.
 
 Ltac eexists_rel_exp :=
diff --git a/theories/Core/Completeness/NatCases.v b/theories/Core/Completeness/NatCases.v
index 6bbba227..b04a60ef 100644
--- a/theories/Core/Completeness/NatCases.v
+++ b/theories/Core/Completeness/NatCases.v
@@ -1,6 +1,6 @@
-From Coq Require Import Morphisms_Relations Relation_Definitions RelationClasses.
+From Coq Require Import Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.SubstitutionCases Completeness.TermStructureCases Completeness.UniverseCases Semantic.Realizability System.
+From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.SubstitutionCases Completeness.TermStructureCases Completeness.UniverseCases Semantic.Realizability.
 Import Domain_Notations.
 
 Lemma rel_exp_of_nat_inversion : forall {Γ M M'},
@@ -335,7 +335,7 @@ Lemma eval_natrec_rel : forall {Γ env_relΓ MZ MZ' MS MS' A A' i m m'},
     {{ Γ, ℕ, A ⊨ MS ≈ MS' : A[Wk∘Wk,,succ(#1)] }} ->
     {{ Dom m ≈ m' ∈ per_nat }} ->
     (forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}),
-      forall (elem_rel : relation domain),
+      forall elem_rel,
         rel_typ i A d{{{ p ↦ m }}} A d{{{ p' ↦ m' }}} elem_rel ->
         exists r r',
           {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} /\
@@ -423,7 +423,8 @@ Lemma rel_exp_natrec_cong_rel_typ: forall {Γ A A' i M M' env_relΓ},
     forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}) n n',
       {{ ⟦ M ⟧ p ↘ n }} ->
       {{ ⟦ M' ⟧ p' ↘ n' }} ->
-      exists elem_rel, rel_typ i A d{{{ p ↦ n }}} A d{{{ p' ↦ n' }}} elem_rel.
+      exists elem_rel,
+        rel_typ i A d{{{ p ↦ n }}} A d{{{ p' ↦ n' }}} elem_rel.
 Proof.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
@@ -495,8 +496,7 @@ Lemma eval_natrec_sub_rel : forall {Γ env_relΓ σ Δ env_relΔ MZ MZ' MS MS' A
     {{ Dom m ≈ m' ∈ per_nat }} ->
     (forall p p'
         (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }})
-        o o'
-        (elem_rel : relation domain),
+        o o' elem_rel,
         {{ ⟦ σ ⟧s p ↘ o }} ->
         {{ ⟦ σ ⟧s p' ↘ o' }} ->
         {{ Dom o ≈ o' ∈ env_relΔ }} ->
@@ -586,7 +586,8 @@ Lemma rel_exp_natrec_sub_rel_typ: forall {Γ σ Δ A i M env_relΓ},
     {{ Δ, ℕ ⊨ A : Type@i }} ->
     {{ Δ ⊨ M : ℕ }} ->
     forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}),
-    exists elem_rel, rel_typ i {{{ A[σ,,M[σ]] }}} p {{{ A[σ,,M[σ]] }}} p' elem_rel.
+    exists elem_rel,
+      rel_typ i {{{ A[σ,,M[σ]] }}} p {{{ A[σ,,M[σ]] }}} p' elem_rel.
 Proof.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
@@ -675,7 +676,7 @@ Lemma rel_exp_nat_beta_succ_rel_typ : forall {Γ env_relΓ A i M},
     {{ Γ, ℕ ⊨ A : Type@i }} ->
     {{ Γ ⊨ M : ℕ }} ->
     forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_relΓ }}),
-    exists elem_rel : relation domain,
+    exists elem_rel,
       rel_typ i {{{ A[Id,,succ M] }}} p {{{ A[Id,,succ M] }}} p' elem_rel.
 Proof.
   pose proof (@relation_equivalence_pointwise domain).
@@ -708,7 +709,7 @@ Proof.
   eexists_rel_exp.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  assert (exists elem_rel : relation domain,
+  assert (exists elem_rel,
              rel_typ i {{{ A[Id,,succ M] }}} p {{{ A[Id,,succ M] }}} p' elem_rel) as [elem_rel]
       by (eapply rel_exp_nat_beta_succ_rel_typ; mauto).
   eexists; split; [eassumption |].
diff --git a/theories/Core/Completeness/SubstitutionCases.v b/theories/Core/Completeness/SubstitutionCases.v
index f2ba1541..36b820c0 100644
--- a/theories/Core/Completeness/SubstitutionCases.v
+++ b/theories/Core/Completeness/SubstitutionCases.v
@@ -1,6 +1,6 @@
 From Coq Require Import Morphisms_Relations RelationClasses.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.ContextCases Completeness.LogicalRelation Completeness.UniverseCases System.
+From Mcltt.Core Require Import Completeness.ContextCases Completeness.LogicalRelation Completeness.UniverseCases.
 Import Domain_Notations.
 
 Lemma rel_sub_id : forall {Γ},
diff --git a/theories/Core/Completeness/TermStructureCases.v b/theories/Core/Completeness/TermStructureCases.v
index b2386a7a..2d894066 100644
--- a/theories/Core/Completeness/TermStructureCases.v
+++ b/theories/Core/Completeness/TermStructureCases.v
@@ -1,6 +1,6 @@
 From Coq Require Import Morphisms_Relations RelationClasses.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.UniverseCases System.
+From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.UniverseCases.
 Import Domain_Notations.
 
 Lemma rel_exp_sub_cong : forall {Δ M M' A σ σ' Γ},
diff --git a/theories/Core/Completeness/VariableCases.v b/theories/Core/Completeness/VariableCases.v
index ed171b54..f90964c6 100644
--- a/theories/Core/Completeness/VariableCases.v
+++ b/theories/Core/Completeness/VariableCases.v
@@ -1,6 +1,6 @@
-From Coq Require Import Morphisms_Relations RelationClasses.
+From Coq Require Import Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation System.
+From Mcltt.Core Require Import Completeness.LogicalRelation SystemOpt.
 Import Domain_Notations.
 
 Lemma valid_lookup : forall {Γ x A env_rel}
diff --git a/theories/Core/Semantic/NbE.v b/theories/Core/Semantic/NbE.v
index 4c1243b2..f6f38d57 100644
--- a/theories/Core/Semantic/NbE.v
+++ b/theories/Core/Semantic/NbE.v
@@ -1,6 +1,5 @@
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation Readback.
-From Mcltt.Core Require Export Domain.
+From Mcltt.Core Require Export Domain Evaluation Readback.
 Import Domain_Notations.
 
 Generalizable All Variables.
diff --git a/theories/Core/Semantic/PER/CoreTactics.v b/theories/Core/Semantic/PER/CoreTactics.v
index d282eda8..506b4a5a 100644
--- a/theories/Core/Semantic/PER/CoreTactics.v
+++ b/theories/Core/Semantic/PER/CoreTactics.v
@@ -1,7 +1,7 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation PER.Definitions Readback.
+From Mcltt.Core Require Import PER.Definitions.
 Import Domain_Notations.
 
 Ltac destruct_rel_by_assumption in_rel H :=
diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index bf9089cb..a26e915d 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -1,8 +1,7 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation Readback.
-From Mcltt Require Export Domain.
+From Mcltt.Core Require Export Domain Evaluation Readback.
 Import Domain_Notations.
 
 Notation "'Dom' a ≈ b ∈ R" := ((R a b : Prop) : Prop) (in custom judg at level 90, a custom domain, b custom domain, R constr).
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index ba11ac85..de7efe87 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -1,7 +1,7 @@
 From Coq Require Import Equivalence Lia Morphisms Morphisms_Prop Morphisms_Relations PeanoNat Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation PER.Definitions PER.CoreTactics Readback.
+From Mcltt.Core Require Import PER.Definitions PER.CoreTactics.
 Import Domain_Notations.
 
 Add Parametric Morphism A : PER
diff --git a/theories/Core/Semantic/Realizability.v b/theories/Core/Semantic/Realizability.v
index 5a6a0144..d5627898 100644
--- a/theories/Core/Semantic/Realizability.v
+++ b/theories/Core/Semantic/Realizability.v
@@ -1,7 +1,7 @@
 From Coq Require Import Lia Morphisms_Relations PeanoNat Relation_Definitions.
 From Equations Require Import Equations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Export Evaluation NbE PER Readback.
+From Mcltt.Core Require Export NbE PER.
 Import Domain_Notations.
 
 Lemma per_nat_then_per_top : forall {n m},
diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v
index 0e6626af..64481051 100644
--- a/theories/Core/Soundness/LogicalRelation/Definitions.v
+++ b/theories/Core/Soundness/LogicalRelation/Definitions.v
@@ -2,9 +2,8 @@ From Coq Require Import Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
 
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import System.Definitions Evaluation Readback PER.Definitions.
-From Mcltt Require Export Domain.
-From Mcltt.Core.Soundness Require Export Weakening.Definition.
+From Mcltt.Core Require Import System.Definitions.
+From Mcltt.Core Require Export Domain PER.Definitions Soundness.Weakening.Definition.
 
 Import Domain_Notations.
 Global Open Scope predicate_scope.
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 8f5c25df..59e99a6e 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1,7 +1,7 @@
 From Coq Require Import Morphisms Morphisms_Relations.
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation PER Presup CtxEq Readback Syntactic.Corollaries SystemOpt.
 
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import PER Syntactic.Corollaries.
 From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions.
 From Mcltt.Core.Soundness Require Export Weakening.Lemmas.
 Import Domain_Notations.
diff --git a/theories/Core/Soundness/Weakening/Lemmas.v b/theories/Core/Soundness/Weakening/Lemmas.v
index 477508fd..ad7ec46c 100644
--- a/theories/Core/Soundness/Weakening/Lemmas.v
+++ b/theories/Core/Soundness/Weakening/Lemmas.v
@@ -1,7 +1,7 @@
 From Coq Require Import Program.Equality.
 
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import CtxEq Presup Syntactic.Corollaries System Weakening.Definition.
+From Mcltt.Core Require Import Syntactic.Corollaries Weakening.Definition.
 Import Syntax_Notations.
 
 Lemma weakening_escape : forall Γ σ Δ,
diff --git a/theories/Core/Syntactic/Corollaries.v b/theories/Core/Syntactic/Corollaries.v
index 586232d9..06a3eb81 100644
--- a/theories/Core/Syntactic/Corollaries.v
+++ b/theories/Core/Syntactic/Corollaries.v
@@ -1,6 +1,6 @@
 From Coq Require Import Setoid.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import SystemOpt.
+From Mcltt.Core Require Export SystemOpt.
 Import Syntax_Notations.
 
 Corollary invert_id : forall Γ Δ,
diff --git a/theories/Extraction/NbE.v b/theories/Extraction/NbE.v
index 8aad8eff..b23d7645 100644
--- a/theories/Extraction/NbE.v
+++ b/theories/Extraction/NbE.v
@@ -1,5 +1,5 @@
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Readback Evaluation NbE.
+From Mcltt.Core Require Import NbE.
 From Mcltt.Extraction Require Import Evaluation Readback.
 From Equations Require Import Equations.
 Import Domain_Notations.
diff --git a/theories/Extraction/TypeCheck.v b/theories/Extraction/TypeCheck.v
index d0698684..bc923cae 100644
--- a/theories/Extraction/TypeCheck.v
+++ b/theories/Extraction/TypeCheck.v
@@ -1,5 +1,5 @@
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness NbE Presup Soundness System.
+From Mcltt.Core Require Import Completeness NbE Soundness SystemOpt.
 From Mcltt.Extraction Require Import NbE.
 From Equations Require Import Equations.
 Import Domain_Notations.

From 80ee4953391b3a92bf354df30c842afe63e6bbbc Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Sun, 9 Jun 2024 23:43:10 -0400
Subject: [PATCH 3/3] Remove more premises

---
 theories/Core/Syntactic/System/Lemmas.v |  8 ++++++++
 theories/Core/Syntactic/SystemOpt.v     | 24 ++++++++----------------
 2 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index aa776c4b..214389f6 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -145,6 +145,14 @@ Qed.
 #[export]
 Hint Resolve presup_exp_eq_ctx : mcltt.
 
+Lemma wf_pi_syntactic_inversion : forall {Γ A B C},
+    {{ Γ ⊢ Π A B : C }} ->
+    exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}.
+Proof.
+  intros * H.
+  dependent induction H; mauto 4.
+Qed.
+
 Lemma exp_eq_refl : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ Γ ⊢ M ≈ M : A }}.
 Proof.
   mauto.
diff --git a/theories/Core/Syntactic/SystemOpt.v b/theories/Core/Syntactic/SystemOpt.v
index b417eed9..976483fc 100644
--- a/theories/Core/Syntactic/SystemOpt.v
+++ b/theories/Core/Syntactic/SystemOpt.v
@@ -48,16 +48,14 @@ Hint Resolve wf_fn' : mcltt.
 #[export]
 Remove Hints wf_fn : mcltt.
 
-Corollary wf_app' : forall {Γ M N A B i},
-    {{ Γ , A ⊢ B : Type@i }} ->
+Corollary wf_app' : forall {Γ M N A B},
     {{ Γ ⊢ M : Π A B }} ->
     {{ Γ ⊢ N : A }} ->
     {{ Γ ⊢ M N : B[Id,,N] }}.
 Proof.
   intros.
   gen_presups.
-  exvar nat ltac:(fun i => assert {{ Γ ⊢ A : Type@i }} by (eapply lift_exp_max_left; mauto 3)).
-  exvar nat ltac:(fun i => assert {{ Γ, A ⊢ B : Type@i }} by (eapply lift_exp_max_right; mauto 3)).
+  assert (exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}) as [? []] by eauto using wf_pi_syntactic_inversion.
   mautosolve 3.
 Qed.
 
@@ -162,16 +160,14 @@ Hint Resolve wf_exp_eq_fn_sub' : mcltt.
 #[export]
 Remove Hints wf_exp_eq_fn_sub : mcltt.
 
-Corollary wf_exp_eq_app_cong' : forall {Γ A B i M M' N N'},
-    {{ Γ , A ⊢ B : Type@i }} ->
+Corollary wf_exp_eq_app_cong' : forall {Γ A B M M' N N'},
     {{ Γ ⊢ M ≈ M' : Π A B }} ->
     {{ Γ ⊢ N ≈ N' : A }} ->
     {{ Γ ⊢ M N ≈ M' N' : B[Id,,N] }}.
 Proof.
   intros.
   gen_presups.
-  exvar nat ltac:(fun i => assert {{ Γ ⊢ A : Type@i }} by (eapply lift_exp_max_left; mauto 3)).
-  exvar nat ltac:(fun i => assert {{ Γ, A ⊢ B : Type@i }} by (eapply lift_exp_max_right; mauto 3)).
+  assert (exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}) as [? []] by eauto using wf_pi_syntactic_inversion.
   mautosolve 3.
 Qed.
 
@@ -180,17 +176,15 @@ Hint Resolve wf_exp_eq_app_cong' : mcltt.
 #[export]
 Remove Hints wf_exp_eq_app_cong : mcltt.
 
-Corollary wf_exp_eq_app_sub' : forall {Γ σ Δ A B i M N},
+Corollary wf_exp_eq_app_sub' : forall {Γ σ Δ A B M N},
     {{ Γ ⊢s σ : Δ }} ->
-    {{ Δ , A ⊢ B : Type@i }} ->
     {{ Δ ⊢ M : Π A B }} ->
     {{ Δ ⊢ N : A }} ->
     {{ Γ ⊢ (M N)[σ] ≈ M[σ] N[σ] : B[σ,,N[σ]] }}.
 Proof.
   intros.
   gen_presups.
-  exvar nat ltac:(fun i => assert {{ Δ ⊢ A : Type@i }} by (eapply lift_exp_max_left; mauto 3)).
-  exvar nat ltac:(fun i => assert {{ Δ, A ⊢ B : Type@i }} by (eapply lift_exp_max_right; mauto 3)).
+  assert (exists i, {{ Δ ⊢ A : Type@i }} /\ {{ Δ, A ⊢ B : Type@i }}) as [? []] by eauto using wf_pi_syntactic_inversion.
   mautosolve 3.
 Qed.
 
@@ -216,15 +210,13 @@ Hint Resolve wf_exp_eq_pi_beta' : mcltt.
 #[export]
 Remove Hints wf_exp_eq_pi_beta : mcltt.
 
-Corollary wf_exp_eq_pi_eta' : forall {Γ A B i M},
-    {{ Γ , A ⊢ B : Type@i }} ->
+Corollary wf_exp_eq_pi_eta' : forall {Γ A B M},
     {{ Γ ⊢ M : Π A B }} ->
     {{ Γ ⊢ M ≈ λ A (M[Wk] #0) : Π A B }}.
 Proof.
   intros.
   gen_presups.
-  exvar nat ltac:(fun i => assert {{ Γ ⊢ A : Type@i }} by (eapply lift_exp_max_left; mauto 3)).
-  exvar nat ltac:(fun i => assert {{ Γ, A ⊢ B : Type@i }} by (eapply lift_exp_max_right; mauto 3)).
+  assert (exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}) as [? []] by eauto using wf_pi_syntactic_inversion.
   mautosolve 3.
 Qed.