From 81b0e141ca819c87c9af2ff9f2418200336d98e8 Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Sun, 21 Jan 2024 15:25:30 -0500
Subject: [PATCH] Refactor syntatic code style (#45)

---
 theories/Core/Base.v                   |  7 +++
 theories/Core/Syntactic/CtxEquiv.v     | 29 ++++-----
 theories/Core/Syntactic/Presup.v       | 30 ++++-----
 theories/Core/Syntactic/Relations.v    | 22 +++----
 theories/Core/Syntactic/Syntax.v       | 86 +++++++++++++++++++++-----
 theories/Core/Syntactic/System.v       |  8 +--
 theories/Core/Syntactic/SystemLemmas.v | 42 ++++++-------
 theories/Frontend/Elaborator.v         | 17 ++---
 theories/Frontend/Parser.vy            |  3 +-
 theories/Frontend/ParserExtraction.v   | 11 ++--
 theories/LibTactics.v                  |  4 +-
 theories/_CoqProject                   |  1 +
 12 files changed, 142 insertions(+), 118 deletions(-)
 create mode 100644 theories/Core/Base.v

diff --git a/theories/Core/Base.v b/theories/Core/Base.v
new file mode 100644
index 00000000..b0de8da4
--- /dev/null
+++ b/theories/Core/Base.v
@@ -0,0 +1,7 @@
+#[global] Declare Scope exp_scope.
+#[global] Delimit Scope exp_scope with exp.
+
+#[global] Bind Scope exp_scope with Sortclass.
+
+#[global] Declare Custom Entry judg.
+Notation "{{ x }}" := x (at level 0, x custom judg at level 99, format "'{{'  x  '}}'").
diff --git a/theories/Core/Syntactic/CtxEquiv.v b/theories/Core/Syntactic/CtxEquiv.v
index 6d99fcf6..8320dfdc 100644
--- a/theories/Core/Syntactic/CtxEquiv.v
+++ b/theories/Core/Syntactic/CtxEquiv.v
@@ -1,27 +1,22 @@
-Require Import Unicode.Utf8_core.
-
-Require Import LibTactics.
-Require Import Syntactic.Syntax.
-Require Import Syntactic.System.
-Require Import Syntactic.SystemLemmas.
+From Mcltt Require Import Base LibTactics Syntax System SystemLemmas.
 
 #[local]
 Ltac gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper H :=
   match type of H with
-  | {{ ?Γ ⊢ ?M : ?A }} => pose proof ctxeq_exp_helper _ _ _ H
-  | {{ ?Γ ⊢ ?M ≈ ?N : ?A }} => pose proof ctxeq_exp_eq_helper _ _ _ _ H
-  | {{ ?Γ ⊢s ?σ : ?Δ }} => pose proof ctxeq_sub_helper _ _ _ H
-  | {{ ?Γ ⊢s ?σ ≈ ?τ : ?Δ }} => pose proof ctxeq_sub_eq_helper _ _ _ _ H
+  | {{ ~?Γ ⊢ ~?M : ~?A }} => pose proof ctxeq_exp_helper _ _ _ H
+  | {{ ~?Γ ⊢ ~?M ≈ ~?N : ~?A }} => pose proof ctxeq_exp_eq_helper _ _ _ _ H
+  | {{ ~?Γ ⊢s ~?σ : ~?Δ }} => pose proof ctxeq_sub_helper _ _ _ H
+  | {{ ~?Γ ⊢s ~?σ ≈ ~?τ : ~?Δ }} => pose proof ctxeq_sub_eq_helper _ _ _ _ H
   | _ => idtac
   end.
 
-Lemma ctxeq_exp_helper : forall {Γ M A}, {{ Γ ⊢ M : A }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M : A }}
+Lemma ctxeq_exp_helper : forall {Γ M A}, {{ Γ ⊢ M : A }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M : A }}
 with
-ctxeq_exp_eq_helper : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M ≈ M' : A }}
+ctxeq_exp_eq_helper : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M ≈ M' : A }}
 with
-ctxeq_sub_helper : forall {Γ Γ' σ}, {{ Γ ⊢s σ : Γ' }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ : Γ' }}
+ctxeq_sub_helper : forall {Γ Γ' σ}, {{ Γ ⊢s σ : Γ' }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ : Γ' }}
 with
-ctxeq_sub_eq_helper : forall {Γ Γ' σ σ'}, {{ Γ ⊢s σ ≈ σ' : Γ' }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
+ctxeq_sub_eq_helper : forall {Γ Γ' σ σ'}, {{ Γ ⊢s σ ≈ σ' : Γ' }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
 Proof with solve [mauto].
   (* ctxeq_exp_helper *)
   - intros * HM * HΓΔ. gen Δ.
@@ -37,7 +32,7 @@ Proof with solve [mauto].
 
     + econstructor...
 
-    + assert (∃ B i, {{ #x : B ∈ Δ }} ∧ {{ Γ ⊢ A ≈ B : Type@i }} ∧ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
+    + assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
 
   (* ctxeq_exp_eq_helper *)
   - intros * HMM' * HΓΔ. gen Δ.
@@ -49,10 +44,10 @@ Proof with solve [mauto].
     1-5: assert {{ Δ ⊢ B : Type@i }} by eauto.
     1-5: assert {{ ⊢ Γ, B ≈ Δ, B }}...
 
-    + assert (∃ B i, {{ #x : B ∈ Δ }} ∧ {{ Γ ⊢ A ≈ B : Type@i }} ∧ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
+    + assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
 
     + inversion_clear HΓΔ as [|? Δ0 ? ? C'].
-      assert (∃ D i', {{ #x : D ∈ Δ0 }} ∧ {{ Γ0 ⊢ B ≈ D : Type@i' }} ∧ {{ Δ0 ⊢ B ≈ D : Type@i' }}) as [D [i0 [? [? ?]]]] by mauto.
+      assert (exists D i', {{ #x : D ∈ Δ0 }} /\ {{ Γ0 ⊢ B ≈ D : Type@i' }} /\ {{ Δ0 ⊢ B ≈ D : Type@i' }}) as [D [i0 [? [? ?]]]] by mauto.
       assert {{ Δ0, C' ⊢ B[Wk] ≈ D[Wk] : Type @ i0 }}...
 
   (* ctxeq_sub_helper *)
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index a16b8433..2dc93fd4 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -1,20 +1,12 @@
-Require Import Unicode.Utf8_core.
-Require Import Setoid.
-
-Require Import LibTactics.
-Require Import Syntactic.Syntax.
-Require Import Syntactic.System.
-Require Import Syntactic.SystemLemmas.
-Require Import Syntactic.CtxEquiv.
-Require Import Syntactic.Relations.
+From Mcltt Require Import Base CtxEquiv LibTactics Relations Syntax System SystemLemmas.
 
 Ltac gen_presup_ctx H :=
   match type of H with
-  | {{ ⊢ ?Γ ≈ ?Δ }} =>
+  | {{ ⊢ ~?Γ ≈ ~?Δ }} =>
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_ctx_eq H as [HΓ HΔ]
-  | {{ ?Γ ⊢s ?σ : ?Δ }} =>
+  | {{ ~?Γ ⊢s ~?σ : ~?Δ }} =>
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_sub_ctx H as [HΓ HΔ]
@@ -23,19 +15,19 @@ Ltac gen_presup_ctx H :=
 
 Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H :=
   match type of H with
-  | {{ ?Γ ⊢ ?M : ?A }} =>
+  | {{ ~?Γ ⊢ ~?M : ~?A }} =>
       let HΓ := fresh "HΓ" in
       let i := fresh "i" in
       let HAi := fresh "HAi" in
       pose proof presup_exp _ _ _ H as [HΓ [i HAi]]
-  | {{ ?Γ ⊢ ?M ≈ ?N : ?A }} =>
+  | {{ ~?Γ ⊢ ~?M ≈ ~?N : ~?A }} =>
       let HΓ := fresh "HΓ" in
       let i := fresh "i" in
       let HM := fresh "HM" in
       let HN := fresh "HN" in
       let HAi := fresh "HAi" in
       pose proof presup_exp_eq _ _ _ _ H as [HΓ [HM [HN [i HAi]]]]
-  | {{ ?Γ ⊢s ?σ ≈ ?τ : ?Δ }} =>
+  | {{ ~?Γ ⊢s ~?σ ≈ ~?τ : ~?Δ }} =>
       let HΓ := fresh "HΓ" in
       let Hσ := fresh "Hσ" in
       let Hτ := fresh "Hτ" in
@@ -44,9 +36,9 @@ Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H :=
   | _ => gen_presup_ctx H
   end.
 
-Lemma presup_exp : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ A : Type@i }}
-with presup_exp_eq : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢ M : A }} ∧ {{ Γ ⊢ M' : A }} ∧ ∃ i, {{ Γ ⊢ A : Type@i }}
-with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢s σ : Δ }} ∧ {{ Γ ⊢s σ' : Δ }} ∧ {{ ⊢ Δ }}.
+Lemma presup_exp : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}
+with presup_exp_eq : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢ M : A }} /\ {{ Γ ⊢ M' : A }} /\ exists i, {{ Γ ⊢ A : Type@i }}
+with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢s σ : Δ }} /\ {{ Γ ⊢s σ' : Δ }} /\ {{ ⊢ Δ }}.
 Proof with solve [mauto].
   (* presup_exp *)
   - intros * HM.
@@ -179,7 +171,7 @@ Proof with solve [mauto].
       assert {{ Γ ⊢ B[Wk][σ ,, N'] ≈ B[σ] : Type@i }} by mauto.
       enough {{ Γ ⊢ #0[σ ,, N'] : B[Wk][σ ,, N'] }}...
 
-    + assert (∃ i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto.
+    + assert (exists i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto.
       assert {{ Γ ⊢s Wk∘(σ ,, N) ≈ σ : Δ }} by mauto.
       assert {{ Γ ⊢ C[Wk∘(σ ,, N)] ≈ C[σ] : Type@i' }} by mauto.
       assert {{ Δ, B ⊢s Wk : Δ }} by mauto.
@@ -187,7 +179,7 @@ Proof with solve [mauto].
       assert {{ Δ, B ⊢ #(S x) : C[Wk] }} by mauto.
       enough {{ Γ ⊢ #(S x)[σ ,, N] : C[Wk][σ ,, N] }}...
 
-    + assert (∃ i, {{ Δ ⊢ C : Type@i }}) as []...
+    + assert (exists i, {{ Δ ⊢ C : Type@i }}) as []...
 
   - intros * Hσσ'.
     inversion_clear Hσσ'; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq); clear presup_exp presup_exp_eq presup_sub_eq; repeat split; mauto.
diff --git a/theories/Core/Syntactic/Relations.v b/theories/Core/Syntactic/Relations.v
index f17875ab..eb79285e 100644
--- a/theories/Core/Syntactic/Relations.v
+++ b/theories/Core/Syntactic/Relations.v
@@ -1,12 +1,6 @@
-Require Import Unicode.Utf8_core.
-Require Import Setoid.
-Require Import Coq.Program.Equality.
+From Coq Require Import Setoid.
 
-Require Import LibTactics.
-Require Import Syntactic.Syntax.
-Require Import Syntactic.System.
-Require Import Syntactic.SystemLemmas.
-Require Import Syntactic.CtxEquiv.
+From Mcltt Require Import Base CtxEquiv LibTactics Syntax System SystemLemmas.
 
 Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ≈ Γ }}.
 Proof with mauto.
@@ -36,12 +30,12 @@ Add Relation (ctx) (wf_ctx_eq)
     transitivity proved by @ctx_eq_trans
     as ctx_eq.
 
-Add Parametric Relation (Γ : ctx) (T : typ) : (exp) (λ t t', {{ Γ ⊢ t ≈ t' : T }})
-    symmetry proved by (λ t t', wf_exp_eq_sym Γ t t' T)
-    transitivity proved by (λ t t' t'', wf_exp_eq_trans Γ t t' T t'')
+Add Parametric Relation (Γ : ctx) (T : typ) : (exp) (fun t t' => {{ Γ ⊢ t ≈ t' : T }})
+    symmetry proved by (fun t t' => wf_exp_eq_sym Γ t t' T)
+    transitivity proved by (fun t t' t'' => wf_exp_eq_trans Γ t t' T t'')
     as exp_eq.                                                
 
-Add Parametric Relation (Γ Δ : ctx) : (sub) (λ σ τ, {{ Γ ⊢s σ ≈ τ : Δ }})
-    symmetry proved by (λ σ τ, wf_sub_eq_sym Γ σ τ Δ)
-    transitivity proved by (λ σ τ ρ, wf_sub_eq_trans Γ σ τ Δ ρ)
+Add Parametric Relation (Γ Δ : ctx) : (sub) (fun σ τ => {{ Γ ⊢s σ ≈ τ : Δ }})
+    symmetry proved by (fun σ τ => wf_sub_eq_sym Γ σ τ Δ)
+    transitivity proved by (fun σ τ ρ => wf_sub_eq_trans Γ σ τ Δ ρ)
     as sub_eq.
diff --git a/theories/Core/Syntactic/Syntax.v b/theories/Core/Syntactic/Syntax.v
index bfcb0cfe..59e37cab 100644
--- a/theories/Core/Syntactic/Syntax.v
+++ b/theories/Core/Syntactic/Syntax.v
@@ -1,5 +1,6 @@
-Require Import String.
-Require Import List.
+From Coq Require Import List String.
+
+From Mcltt Require Import Base.
 
 (* CST term *)
 Module Cst.
@@ -37,6 +38,9 @@ with sub : Set :=
 | a_compose : sub -> sub -> sub
 | a_extend : sub -> exp -> sub.
 
+Notation ctx := (list exp).
+Notation typ := exp.
+
 Fixpoint nat_to_exp n : exp :=
   match n with
   | 0 => a_zero
@@ -60,39 +64,87 @@ Definition exp_to_num e :=
   | None => None
   end.
 
-#[global] Declare Custom Entry exp.
-#[global] Declare Scope exp_scope.
-#[global] Delimit Scope exp_scope with exp.
 #[global] Bind Scope exp_scope with exp.
 #[global] Bind Scope exp_scope with sub.
-#[global] Bind Scope exp_scope with Sortclass.
 Open Scope exp_scope.
-Open Scope nat_scope.
+
+#[global] Declare Custom Entry exp.
 
 Notation "{{{ x }}}" := x (at level 0, x custom exp at level 99, format "'{{{'  x  '}}}'") : exp_scope.
 Notation "( x )" := x (in custom exp at level 0, x custom exp at level 60) : exp_scope.
 Notation "~ x" := x (in custom exp at level 0, x constr at level 0) : exp_scope.
-Notation "x" := x (in custom exp at level 0, x constr at level 0) : exp_scope.
+Notation "x" := x (in custom exp at level 0, x global) : exp_scope.
 Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, s custom exp at level 60) : exp_scope.
-Notation "'λ' T e" := (a_fn T e) (in custom exp at level 0, T custom exp at level 0, e custom exp at level 60) : exp_scope.
+Notation "'λ' A e" := (a_fn A e) (in custom exp at level 0, A custom exp at level 0, e custom exp at level 60) : exp_scope.
 Notation "f x .. y" := (a_app .. (a_app f x) .. y) (in custom exp at level 40, f custom exp, x custom exp at next level, y custom exp at next level) : exp_scope.
 Notation "'ℕ'" := a_nat (in custom exp) : exp_scope.
 Notation "'Type' @ n" := (a_typ n) (in custom exp at level 0, n constr at level 0) : exp_scope.
-Notation "'Π' T S" := (a_pi T S) (in custom exp at level 0, T custom exp at level 0, S custom exp at level 60) : exp_scope.
-Number Notation exp num_to_exp exp_to_num : exp_scope.
+Notation "'Π' A B" := (a_pi A B) (in custom exp at level 0, A custom exp at level 0, B custom exp at level 60) : exp_scope.
 Notation "'zero'" := a_zero (in custom exp at level 0) : exp_scope.
 Notation "'succ' e" := (a_succ e) (in custom exp at level 0, e custom exp at level 0) : exp_scope.
-Notation "'rec' e 'return' m | 'zero' -> ez | 'succ' -> es 'end'" := (a_natrec m ez es e) (in custom exp at level 0, m custom exp at level 60, ez custom exp at level 60, es custom exp at level 60, e custom exp at level 60) : exp_scope.
+Notation "'rec' e 'return' A | 'zero' -> ez | 'succ' -> es 'end'" := (a_natrec A ez es e) (in custom exp at level 0, A custom exp at level 60, ez custom exp at level 60, es custom exp at level 60, e custom exp at level 60) : exp_scope.
 Notation "'#' n" := (a_var n) (in custom exp at level 0, n constr at level 0) : exp_scope.
 Notation "'Id'" := a_id (in custom exp at level 0) : exp_scope.
 Notation "'Wk'" := a_weaken (in custom exp at level 0) : exp_scope.
 
-Notation "⋅" := nil (in custom exp at level 0) : exp_scope.
-Notation "x , y" := (cons y x) (in custom exp at level 50) : exp_scope.
-
 Infix "∘" := a_compose (in custom exp at level 40) : exp_scope.
 Infix ",," := a_extend (in custom exp at level 50) : exp_scope.
 Notation "'q' σ" := ({{{ σ ∘ Wk ,, # 0 }}}) (in custom exp at level 30) : exp_scope.
 
-Notation ctx := (list exp).
-Notation typ := exp.
+Notation "⋅" := nil (in custom exp at level 0) : exp_scope.
+Notation "x , y" := (cons y x) (in custom exp at level 50) : exp_scope.
+
+Inductive nf : Set :=
+| nf_typ : nat -> nf
+| nf_nat : nf
+| nf_zero : nf
+| nf_succ : nf -> nf
+| nf_pi : nf -> nf -> nf
+| nf_fn : nf -> nf -> nf
+| nf_neut : ne -> nf
+with ne : Set :=
+| ne_natrec : nf -> nf -> nf -> ne -> ne
+| ne_app : ne -> nf -> ne
+| ne_var : nat -> ne
+.
+
+#[global] Declare Custom Entry nf.
+
+#[global] Bind Scope exp_scope with nf.
+#[global] Bind Scope exp_scope with ne.
+
+Notation "n{{{ x }}}" := x (at level 0, x custom nf at level 99, format "'n{{{'  x  '}}}'") : exp_scope.
+Notation "( x )" := x (in custom nf at level 0, x custom nf at level 60) : exp_scope.
+Notation "~ x" := x (in custom nf at level 0, x constr at level 0) : exp_scope.
+Notation "x" := x (in custom nf at level 0, x global) : exp_scope.
+Notation "'λ' A e" := (nf_fn A e) (in custom nf at level 0, A custom nf at level 0, e custom nf at level 60) : exp_scope.
+Notation "f x .. y" := (ne_app .. (ne_app f x) .. y) (in custom nf at level 40, f custom nf, x custom nf at next level, y custom nf at next level) : exp_scope.
+Notation "'ℕ'" := nf_nat (in custom nf) : exp_scope.
+Notation "'Type' @ n" := (nf_typ n) (in custom nf at level 0, n constr at level 0) : exp_scope.
+Notation "'Π' A B" := (nf_pi A B) (in custom nf at level 0, A custom nf at level 0, B custom nf at level 60) : exp_scope.
+Notation "'zero'" := nf_zero (in custom nf at level 0) : exp_scope.
+Notation "'succ' M" := (nf_succ M) (in custom nf at level 0, M custom nf at level 0) : exp_scope.
+Notation "'rec' M 'return' A | 'zero' -> MZ | 'succ' -> MS 'end'" := (ne_natrec A MZ MS M) (in custom nf at level 0, A custom nf at level 60, MZ custom nf at level 60, MS custom nf at level 60, M custom nf at level 60) : exp_scope.
+Notation "'#' n" := (ne_var n) (in custom nf at level 0, n constr at level 0) : exp_scope.
+Notation "'⇑' M" := (nf_neut M) (in custom nf at level 0, M custom nf at level 0) : exp_scope.
+
+Fixpoint nf_to_exp (M : nf) : exp :=
+  match M with
+  | nf_typ i => a_typ i
+  | nf_nat => a_nat
+  | nf_zero => a_zero
+  | nf_succ M => a_succ (nf_to_exp M)
+  | nf_pi A B => a_pi (nf_to_exp A) (nf_to_exp B)
+  | nf_fn A M => a_fn (nf_to_exp A) (nf_to_exp M)
+  | nf_neut M => ne_to_exp M
+  end
+with ne_to_exp (M : ne) : exp :=
+  match M with
+  | ne_natrec A MZ MS M => a_natrec (nf_to_exp A) (nf_to_exp MZ) (nf_to_exp MS) (ne_to_exp M)
+  | ne_app M N => a_app (ne_to_exp M) (nf_to_exp N)
+  | ne_var x => a_var x
+  end
+.
+
+Coercion nf_to_exp : nf >-> exp.
+Coercion ne_to_exp : ne >-> exp.
diff --git a/theories/Core/Syntactic/System.v b/theories/Core/Syntactic/System.v
index be179c97..66182660 100644
--- a/theories/Core/Syntactic/System.v
+++ b/theories/Core/Syntactic/System.v
@@ -1,11 +1,7 @@
-Require Import List.
-Require Import Unicode.Utf8_core.
+From Coq Require Import List.
 
-Require Import LibTactics.
-Require Import Syntactic.Syntax.
+From Mcltt Require Import Base LibTactics Syntax.
 
-#[global] Declare Custom Entry judg.
-Notation "{{ x }}" := x (at level 0, x custom judg at level 99, format "'{{'  x  '}}'").
 Reserved Notation "⊢ Γ" (in custom judg at level 80, Γ custom exp).
 Reserved Notation "⊢ Γ ≈ Γ'" (in custom judg at level 80, Γ custom exp, Γ' custom exp).
 Reserved Notation "Γ ⊢ M ≈ M' : A" (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp, A custom exp).
diff --git a/theories/Core/Syntactic/SystemLemmas.v b/theories/Core/Syntactic/SystemLemmas.v
index 2b2c1fe0..2d8245d5 100644
--- a/theories/Core/Syntactic/SystemLemmas.v
+++ b/theories/Core/Syntactic/SystemLemmas.v
@@ -1,10 +1,6 @@
-Require Import Unicode.Utf8_core.
+From Mcltt Require Import Base LibTactics System Syntax.
 
-Require Import LibTactics.
-Require Import Syntactic.Syntax.
-Require Import Syntactic.System.
-
-Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ A : Type@i }}.
+Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}.
 Proof with solve [mauto].
   intros * HAΓ.
   inversion HAΓ; subst...
@@ -19,7 +15,7 @@ Proof with solve [eauto].
   eapply proj1, ctx_decomp...
 Qed.
 
-Lemma ctx_decomp_right : forall {Γ A}, {{ ⊢ Γ , A }} -> ∃ i, {{ Γ ⊢ A : Type@i }}.
+Lemma ctx_decomp_right : forall {Γ A}, {{ ⊢ Γ , A }} -> exists i, {{ Γ ⊢ A : Type@i }}.
 Proof with solve [eauto].
   intros * HAΓ.
   eapply proj2, ctx_decomp...
@@ -70,7 +66,7 @@ Proof with solve [mauto].
   assert (m <= max n m) by lia...
 Qed.
 
-Lemma presup_ctx_eq : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }} ∧ {{ ⊢ Δ }}.
+Lemma presup_ctx_eq : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
 Proof with solve [mauto].
   intros * HΓΔ.
   induction HΓΔ as [|* ? []]...
@@ -91,7 +87,7 @@ Qed.
 #[export]
 Hint Resolve presup_ctx_eq presup_ctx_eq_left presup_ctx_eq_right : mcltt.
 
-Lemma presup_sub_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} ∧ {{ ⊢ Δ }}.
+Lemma presup_sub_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
 Proof with solve [mauto].
   intros * Hσ.
   induction Hσ; repeat destruct_one_pair...
@@ -487,7 +483,7 @@ Qed.
 #[export]
 Hint Resolve exp_eq_sub_sub_compose_cong : mcltt.
 
-Lemma ctx_lookup_wf : forall {Γ A x}, {{ ⊢ Γ }} -> {{ #x : A ∈ Γ }} -> ∃ i, {{ Γ ⊢ A : Type@i }}.
+Lemma ctx_lookup_wf : forall {Γ A x}, {{ ⊢ Γ }} -> {{ #x : A ∈ Γ }} -> exists i, {{ Γ ⊢ A : Type@i }}.
 Proof with solve [mauto].
   intros * HΓ Hx.
   induction Hx; inversion_clear HΓ; [|assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by eauto]...
@@ -496,7 +492,7 @@ Qed.
 #[export]
 Hint Resolve ctx_lookup_wf : mcltt.
 
-Lemma ctxeq_ctx_lookup : forall {Γ Δ A x}, {{ ⊢ Γ ≈ Δ }} -> {{ #x : A ∈ Γ }} -> ∃ B i, {{ #x : B ∈ Δ }} ∧ {{ Γ ⊢ A ≈ B : Type@i }} ∧ {{ Δ ⊢ A ≈ B : Type@i }}.
+Lemma ctxeq_ctx_lookup : forall {Γ Δ A x}, {{ ⊢ Γ ≈ Δ }} -> {{ #x : A ∈ Γ }} -> exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}.
 Proof with solve [mauto].
   intros * HΓΔ Hx; gen Δ.
   induction Hx as [|* ? IHHx]; intros; inversion_clear HΓΔ as [|? ? ? ? ? HΓΔ'];
@@ -506,7 +502,7 @@ Qed.
 #[export]
 Hint Resolve ctxeq_ctx_lookup : mcltt.
 
-Lemma sub_id_extend : ∀ {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s Id,,M : Γ, A }}.
+Lemma sub_id_extend : forall {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s Id,,M : Γ, A }}.
 Proof with solve [mauto].
   intros.
   econstructor...
@@ -515,7 +511,7 @@ Qed.
 #[export]
 Hint Resolve sub_id_extend : mcltt.
 
-Lemma sub_eq_p_id_extend : ∀ {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s Wk∘(Id ,, M) ≈ Id : Γ }}.
+Lemma sub_eq_p_id_extend : forall {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s Wk∘(Id ,, M) ≈ Id : Γ }}.
 Proof with solve [mauto].
   intros.
   econstructor...
@@ -572,12 +568,12 @@ Qed.
 #[export]
 Hint Resolve exp_eq_var_1_sub_q_sigma_nat : mcltt.
 
-Lemma sub_id_extend_zero : ∀ {Γ}, {{ ⊢ Γ }} -> {{ Γ ⊢s Id,,zero : Γ, ℕ }}.
+Lemma sub_id_extend_zero : forall {Γ}, {{ ⊢ Γ }} -> {{ Γ ⊢s Id,,zero : Γ, ℕ }}.
 Proof.
   mauto.
 Qed.
 
-Lemma sub_weak_compose_weak_extend_succ_var_1 : ∀ {Γ A i}, {{ Γ, ℕ ⊢ A : Type@i }} -> {{ Γ, ℕ, A ⊢s Wk∘Wk,,succ #1 : Γ, ℕ }}.
+Lemma sub_weak_compose_weak_extend_succ_var_1 : forall {Γ A i}, {{ Γ, ℕ ⊢ A : Type@i }} -> {{ Γ, ℕ, A ⊢s Wk∘Wk,,succ #1 : Γ, ℕ }}.
 Proof with solve [mauto].
   intros.
   assert {{ ⊢ Γ, ℕ }} by mauto.
@@ -585,7 +581,7 @@ Proof with solve [mauto].
   eapply sub_extend_nat...
 Qed.
 
-Lemma sub_eq_id_extend_nat_compose_sigma : ∀ {Γ M σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ M : ℕ }} -> {{ Γ ⊢s (Id,,M)∘σ ≈ σ,,M[σ] : Δ, ℕ }}.
+Lemma sub_eq_id_extend_nat_compose_sigma : forall {Γ M σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ M : ℕ }} -> {{ Γ ⊢s (Id,,M)∘σ ≈ σ,,M[σ] : Δ, ℕ }}.
 Proof with solve [mauto].
   intros.
   assert {{ Γ ⊢s (Id ,, M)∘σ ≈ Id∘σ ,, M[σ] : Δ, ℕ }} by (eapply sub_eq_extend_compose_nat; mauto).
@@ -594,7 +590,7 @@ Proof with solve [mauto].
   constructor.
 Qed.
 
-Lemma sub_eq_id_extend_compose_sigma : ∀ {Γ M A σ Δ i}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ A : Type@i }} -> {{ Δ ⊢ M : A }} -> {{ Γ ⊢s (Id,,M)∘σ ≈ σ,,M[σ] : Δ, A }}.
+Lemma sub_eq_id_extend_compose_sigma : forall {Γ M A σ Δ i}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ A : Type@i }} -> {{ Δ ⊢ M : A }} -> {{ Γ ⊢s (Id,,M)∘σ ≈ σ,,M[σ] : Δ, A }}.
 Proof with solve [mauto].
   intros.
   assert {{ Γ ⊢s (Id ,, M)∘σ ≈ Id∘σ ,, M[σ] : Δ, A }} by (eapply wf_sub_eq_extend_compose; mauto).
@@ -605,7 +601,7 @@ Qed.
 #[export]
 Hint Resolve sub_id_extend_zero sub_weak_compose_weak_extend_succ_var_1 sub_eq_id_extend_nat_compose_sigma sub_eq_id_extend_compose_sigma : mcltt.
 
-Lemma sub_eq_sigma_compose_weak_id_extend : ∀ {Γ M A i σ Δ}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s (σ∘Wk)∘(Id,,M) ≈ σ : Δ }}.
+Lemma sub_eq_sigma_compose_weak_id_extend : forall {Γ M A i σ Δ}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s (σ∘Wk)∘(Id,,M) ≈ σ : Δ }}.
 Proof with solve [mauto].
   intros.
   assert {{ Γ ⊢s Id,,M : Γ, A }} by mauto.
@@ -617,7 +613,7 @@ Qed.
 #[export]
 Hint Resolve sub_eq_sigma_compose_weak_id_extend : mcltt.
 
-Lemma sub_eq_q_sigma_id_extend : ∀ {Γ M A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : A[σ] }} -> {{ Γ ⊢s q σ∘(Id,,M) ≈ σ,,M : Δ, A }}.
+Lemma sub_eq_q_sigma_id_extend : forall {Γ M A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : A[σ] }} -> {{ Γ ⊢s q σ∘(Id,,M) ≈ σ,,M : Δ, A }}.
 Proof with solve [mauto].
   intros.
   assert {{ Γ ⊢s Id ,, M : Γ, A[σ] }} by mauto.
@@ -634,7 +630,7 @@ Qed.
 #[export]
 Hint Resolve sub_eq_q_sigma_id_extend : mcltt.
 
-Lemma sub_eq_p_q_sigma : ∀ {Γ A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, A[σ] ⊢s Wk∘q σ ≈ σ∘Wk : Δ }}.
+Lemma sub_eq_p_q_sigma : forall {Γ A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, A[σ] ⊢s Wk∘q σ ≈ σ∘Wk : Δ }}.
 Proof with solve [mauto].
   intros.
   assert {{ ⊢ Γ }} by mauto.
@@ -645,7 +641,7 @@ Qed.
 #[export]
 Hint Resolve sub_eq_p_q_sigma : mcltt.
 
-Lemma sub_eq_p_q_sigma_nat : ∀ {Γ σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ ⊢s Wk∘q σ ≈ σ∘Wk : Δ }}.
+Lemma sub_eq_p_q_sigma_nat : forall {Γ σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ ⊢s Wk∘q σ ≈ σ∘Wk : Δ }}.
 Proof with solve [mauto].
   intros.
   assert {{ ⊢ Γ }} by mauto.
@@ -655,7 +651,7 @@ Qed.
 #[export]
 Hint Resolve sub_eq_p_q_sigma_nat : mcltt.
 
-Lemma sub_eq_p_p_q_q_sigma_nat : ∀ {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ, A[q σ] ⊢s Wk∘(Wk∘q (q σ)) ≈ (σ∘Wk)∘Wk : Δ }}.
+Lemma sub_eq_p_p_q_q_sigma_nat : forall {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ, A[q σ] ⊢s Wk∘(Wk∘q (q σ)) ≈ (σ∘Wk)∘Wk : Δ }}.
 Proof with solve [mauto].
   intros.
   assert {{ ⊢ Γ }} by mauto.
@@ -670,7 +666,7 @@ Qed.
 #[export]
 Hint Resolve sub_eq_p_p_q_q_sigma_nat : mcltt.
 
-Lemma sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : ∀ {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ, A[q σ] ⊢s q σ∘(Wk∘Wk,,succ #1) ≈ (Wk∘Wk,,succ #1)∘q (q σ) : Δ, ℕ }}.
+Lemma sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : forall {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ, A[q σ] ⊢s q σ∘(Wk∘Wk,,succ #1) ≈ (Wk∘Wk,,succ #1)∘q (q σ) : Δ, ℕ }}.
 Proof with solve [mauto].
   intros.
   assert {{ ⊢ Δ }} by mauto.
diff --git a/theories/Frontend/Elaborator.v b/theories/Frontend/Elaborator.v
index 122f0901..31634b1d 100644
--- a/theories/Frontend/Elaborator.v
+++ b/theories/Frontend/Elaborator.v
@@ -1,11 +1,6 @@
-Require Export String.
-Require Export List.
-Require Export Coq.Structures.OrderedTypeEx.
-Require Export MSets.
-Require Export Arith.
-Require Export Lia.
+From Coq Require Import Lia List MSets PeanoNat String.
 
-Require Import Syntactic.Syntax.
+From Mcltt Require Import Syntax.
 
 Open Scope string_scope.
 
@@ -102,7 +97,7 @@ Inductive closed_at : exp -> nat -> Prop :=
 Hint Constructors closed_at: core.
 
 (*Lemma for the well_scoped proof, lookup succeeds if var is in context*)
-Lemma lookup_known (s : string) (ctx : list string) (H_in : List.In s ctx) : exists n : nat, (lookup s ctx = Some n /\ n < length ctx).
+Lemma lookup_known (s : string) (ctx : list string) (H_in : List.In s ctx) : exists n : nat, (lookup s ctx = Some n /\ n < List.length ctx).
 Proof.
   induction ctx as [| c ctx' IHctx]; simpl in *.
   - contradiction.
@@ -115,7 +110,7 @@ Proof.
 Qed.
 
 (*Lemma for the well_scoped proof, lookup result always less than context length*)
-Lemma lookup_bound s : forall ctx m, lookup s ctx = Some m -> m < (length ctx).
+Lemma lookup_bound s : forall ctx m, lookup s ctx = Some m -> m < (List.length ctx).
   induction ctx.
   - intros. discriminate H.
   - intros. destruct (string_dec a s).
@@ -138,7 +133,7 @@ Lemma lookup_bound s : forall ctx m, lookup s ctx = Some m -> m < (length ctx).
           rewrite (Nat.add_sub n1 1) in l.
           rewrite <- H1.
           rewrite Nat.add_1_r.
-          apply (Arith_prebase.lt_n_S_stt (n1) (length ctx)).
+          apply (Arith_prebase.lt_n_S_stt (n1) (List.length ctx)).
           apply l.
           reflexivity.
         --discriminate H.
@@ -163,7 +158,7 @@ Qed.
 (*Well scopedness lemma: If the set of free variables in a cst are contained in a context
   then elaboration succeeds with that context, and the result is a closed term*)
 Lemma well_scoped (cst : Cst.obj) : forall ctx,  cst_variables cst [<=] StrSProp.of_list ctx  ->
-exists a : exp, (elaborate cst ctx = Some a) /\ (closed_at a (length ctx)).
+exists a : exp, (elaborate cst ctx = Some a) /\ (closed_at a (List.length ctx)).
 Proof.
   induction cst; intros; simpl in *; eauto.
   - destruct (IHcst _ H) as [ast [-> ?]]; eauto.
diff --git a/theories/Frontend/Parser.vy b/theories/Frontend/Parser.vy
index 3544d5cb..86f9ac0c 100644
--- a/theories/Frontend/Parser.vy
+++ b/theories/Frontend/Parser.vy
@@ -1,7 +1,6 @@
 %{
 
-Require Import String.
-Require Import List.
+From Coq Require Import List String.
 
 From Mcltt Require Import Syntax.
 
diff --git a/theories/Frontend/ParserExtraction.v b/theories/Frontend/ParserExtraction.v
index 65a33a3b..1aafd5b6 100644
--- a/theories/Frontend/ParserExtraction.v
+++ b/theories/Frontend/ParserExtraction.v
@@ -1,11 +1,10 @@
-Require Extraction.
-Require Import Frontend.Parser.
+From Coq Require Extraction.
 
+From Coq Require Import ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlNativeString.
+
+From Mcltt Require Import Parser.
 Import MenhirLibParser.Inter.
-Extraction Language OCaml.
 
-Require Import ExtrOcamlBasic.
-Require Import ExtrOcamlNatInt.
-Require Import ExtrOcamlNativeString.
+Extraction Language OCaml.
 
 Extraction "parser.ml" Parser.prog.
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index a926da7c..edeab12e 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -1,6 +1,4 @@
-Require Export Coq.Program.Tactics.
-
-Require Export Lia.
+From Coq Require Export Program.Tactics Lia.
 
 Create HintDb mcltt discriminated.
 
diff --git a/theories/_CoqProject b/theories/_CoqProject
index ef06b8ec..0480f05f 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -2,6 +2,7 @@
 
 -arg -w -arg -notation-overridden
 
+./Core/Base.v
 ./Core/Syntactic/CtxEquiv.v
 ./Core/Syntactic/Presup.v
 ./Core/Syntactic/Relations.v