Reorganize imports

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  '}}'").

theories/Core/Semantic/Domain.v

@@ -1,4 +1,4 @@
-Require Import Syntactic.Syntax.
+From Mcltt Require Import Syntax.
 
 Reserved Notation "'env'".
 

theories/Core/Semantic/Evaluate.v

@@ -1,6 +1,7 @@
-Require Import Syntactic.Syntax.
-Require Import Syntactic.System.
-Require Import Semantic.Domain.
+From Mcltt Require Import Base.
+From Mcltt Require Import Domain.
+From Mcltt Require Import Syntax.
+From Mcltt Require Import System.
 
 Reserved Notation "'⟦' M '⟧' p '↘' r" (in custom judg at level 80, M custom exp at level 99, p custom domain at level 99, r custom domain at level 99).
 Reserved Notation "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" (in custom judg at level 80, m custom domain at level 99, A custom exp at level 99, MZ custom exp at level 99, MS custom exp at level 99, p custom domain at level 99, r custom domain at level 99).
@@ -9,7 +10,7 @@ Reserved Notation "'⟦' σ '⟧s' p '↘' p'" (in custom judg at level 80, σ c
 
 Generalizable All Variables.
 
-Inductive eval_exp : exp -> env -> domain -> Type :=
+Inductive eval_exp : exp -> env -> domain -> Prop :=
 | eval_exp_typ :
   `( {{ ⟦ Type@i ⟧ p ↘ 𝕌@i }} )
 | eval_exp_nat :
@@ -38,7 +39,7 @@ Inductive eval_exp : exp -> env -> domain -> Type :=
      {{ ⟦ M ⟧ p' ↘ m }} ->
      {{ ⟦ M[σ] ⟧ p ↘ m }} )
 where "'⟦' e '⟧' p '↘' r" := (eval_exp e p r) (in custom judg)
-with eval_natrec : exp -> exp -> exp -> domain -> env -> domain -> Type :=
+with eval_natrec : exp -> exp -> exp -> domain -> env -> domain -> Prop :=
 | eval_natrec_zero :
   `( {{ ⟦ MZ ⟧ p ↘ mz }} ->
      {{ rec zero ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ mz }} )
@@ -51,15 +52,15 @@ with eval_natrec : exp -> exp -> exp -> domain -> env -> domain -> Type :=
      {{ ⟦ A ⟧ p ↦ ⇑ 𝕟 m ↘ a }} ->
      {{ rec ⇑ 𝕟 m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ⇑ a (rec m under p return A | zero -> mz | succ -> MS end) }} )
 where "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" := (eval_natrec A MZ MS m p r) (in custom judg)
-with eval_app : domain -> domain -> domain -> Type :=
+with eval_app : domain -> domain -> domain -> Prop :=
 | eval_app_fn :
   `( {{ ⟦ M ⟧ p ↦ n ↘ m }} ->
      {{ $| λ p M & n |↘ m }} )
 | eval_app_neut :
   `( {{ ⟦ B ⟧ p ↦ n ↘ b }} ->
      {{ $| ⇑ (Π a p B) m & n |↘ ⇑ b (m (⇓ a N)) }} )
 where "'$|' m '&' n '|↘' r" := (eval_app m n r) (in custom judg)
-with eval_sub : sub -> env -> env -> Type :=
+with eval_sub : sub -> env -> env -> Prop :=
 | eval_sub_id :
   `( {{ ⟦ Id ⟧s p ↘ p }} )
 | eval_sub_weaken :

theories/Core/Semantic/Readback.v

@@ -1,15 +1,16 @@
-Require Import Syntactic.Syntax.
-Require Import Syntactic.System.
-Require Import Semantic.Domain.
-Require Import Semantic.Evaluate.
+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.
 
 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).
 Reserved Notation "'Rtyp' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).
 
 Generalizable All Variables.
 
-Inductive read_nf : nat -> domain_nf -> nf -> Type :=
+Inductive read_nf : nat -> domain_nf -> nf -> Prop :=
 | read_nf_type :
   `( {{ Rtyp a in s ↘ A }} ->
      {{ Rnf ⇓ 𝕌@i a in s ↘ A }} )
@@ -35,7 +36,7 @@ Inductive read_nf : nat -> domain_nf -> nf -> Type :=
   `( {{ Rne m in s ↘ M }} ->
      {{ Rnf ⇓ (⇑ a b) (⇑ c m) in s ↘ ⇑ M }} )
 where "'Rnf' m 'in' s ↘ M" := (read_nf s m M) (in custom judg) : exp_scope
-with read_ne : nat -> domain_ne -> ne -> Type :=
+with read_ne : nat -> domain_ne -> ne -> Prop :=
 | read_ne_var :
   `( {{ Rne !x in s ↘ #(s - x - 1) }} )
 | read_ne_app :
@@ -61,7 +62,7 @@ with read_ne : nat -> domain_ne -> ne -> Type :=
 
      {{ Rne rec m under p return B | zero -> mz | succ -> MS end in s ↘ rec M return B' | zero -> MZ | succ -> MS' end }} )
 where "'Rne' m 'in' s ↘ M" := (read_ne s m M) (in custom judg) : exp_scope
-with read_typ : nat -> domain -> nf -> Type :=
+with read_typ : nat -> domain -> nf -> Prop :=
 | read_typ_univ :
   `( {{ Rtyp 𝕌@i in s ↘ Type@i }} )
 | read_typ_nat :

theories/Core/Syntactic/CtxEquiv.v

@@ -1,9 +1,8 @@
-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.
+From Mcltt Require Import LibTactics.
+From Mcltt Require Import Syntax.
+From Mcltt Require Import System.
+From Mcltt Require Import SystemLemmas.
 
 #[local]
 Ltac gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper H :=
@@ -15,13 +14,13 @@ Ltac gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper c
   | _ => 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 +36,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 +48,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 *)

theories/Core/Syntactic/Presup.v

@@ -1,12 +1,10 @@
-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.
+From Mcltt Require Import CtxEquiv.
+From Mcltt Require Import LibTactics.
+From Mcltt Require Import Relations.
+From Mcltt Require Import Syntax.
+From Mcltt Require Import System.
+From Mcltt Require Import SystemLemmas.
 
 Ltac gen_presup_ctx H :=
   match type of H with
@@ -44,9 +42,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,15 +177,15 @@ 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.
       assert {{ Γ ⊢ C[Wk][σ ,, N] ≈ C[σ] : Type@i' }} by 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.

theories/Core/Syntactic/Relations.v

@@ -1,12 +1,11 @@
-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.
+From Mcltt Require Import CtxEquiv.
+From Mcltt Require Import LibTactics.
+From Mcltt Require Import Syntax.
+From Mcltt Require Import System.
+From Mcltt Require Import SystemLemmas.
 
 Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ≈ Γ }}.
 Proof with mauto.
@@ -36,12 +35,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.

theories/Core/Syntactic/Syntax.v

@@ -1,5 +1,7 @@
-Require Import String.
-Require Import List.
+From Coq Require Import List.
+From Coq Require Import String.
+
+From Mcltt Require Import Base.
 
 (* CST term *)
 Module Cst.
@@ -63,15 +65,11 @@ 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.

theories/Core/Syntactic/System.v

@@ -1,11 +1,9 @@
-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.
+From Mcltt Require Import LibTactics.
+From Mcltt Require Import 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).