Refactoring structure (#69)

* Move modules into subdirectories

* Export some missed signature-related code

* Move context equality lemmas into a single file

theories/Core/Semantic/Evaluation.v

@@ -1 +1 @@
-From Mcltt Require Export EvaluationDefinitions EvaluationLemmas.
+From Mcltt Require Export Evaluation.Definitions Evaluation.Lemmas.

theories/Core/Semantic/EvaluationLemmas.v → theories/Core/Semantic/Evaluation/Lemmas.v

@@ -1,5 +1,5 @@
 From Coq Require Import Lia PeanoNat Relations.
-From Mcltt Require Import Base LibTactics EvaluationDefinitions.
+From Mcltt Require Import Base LibTactics Evaluation.Definitions.
 Import Domain_Notations.
 
 Section functional_eval.

theories/Core/Semantic/PER.v

@@ -1 +1 @@
-From Mcltt Require Export PERDefinitions PERLemmas.
+From Mcltt Require Export PER.Definitions PER.Lemmas.

theories/Core/Semantic/PERLemmas.v → theories/Core/Semantic/PER/Lemmas.v

@@ -1,5 +1,5 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
-From Mcltt Require Import Axioms Base Evaluation LibTactics PERDefinitions Readback.
+From Mcltt Require Import Axioms Base Evaluation LibTactics PER.Definitions Readback.
 Import Domain_Notations.
 
 Lemma per_bot_sym : forall m n,

theories/Core/Semantic/Readback.v

@@ -1 +1 @@
-From Mcltt Require Export ReadbackDefinitions ReadbackLemmas.
+From Mcltt Require Export Readback.Definitions Readback.Lemmas.

theories/Core/Semantic/ReadbackLemmas.v → theories/Core/Semantic/Readback/Lemmas.v

@@ -1,5 +1,5 @@
 From Coq Require Import Lia PeanoNat Relations.
-From Mcltt Require Import Base EvaluationLemmas LibTactics ReadbackDefinitions.
+From Mcltt Require Import Base Evaluation LibTactics Readback.Definitions.
 Import Domain_Notations.
 
 Section functional_read.

theories/Core/Syntactic/CtxEq.v

@@ -0,0 +1,144 @@
+From Mcltt Require Import Base LibTactics.
+From Mcltt Require Export System.
+Import Syntax_Notations.
+
+Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ≈ Γ }}.
+Proof with solve [mauto].
+  induction 1...
+Qed.
+
+#[export]
+Hint Resolve ctx_eq_refl : mcltt.
+
+Lemma ctx_eq_sym : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ ≈ Γ }}.
+Proof with solve [mauto].
+  induction 1...
+Qed.
+
+#[export]
+Hint Resolve ctx_eq_sym : mcltt.
+
+Module ctxeq_judg.
+  #[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
+  | _ => idtac
+  end.
+
+  #[local]
+  Lemma ctxeq_exp_helper : forall {Γ M A}, {{ Γ ⊢ M : A }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M : A }}
+  with
+  ctxeq_exp_eq_helper : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M ≈ M' : A }}
+  with
+  ctxeq_sub_helper : forall {Γ Γ' σ}, {{ Γ ⊢s σ : Γ' }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ : Γ' }}
+  with
+  ctxeq_sub_eq_helper : forall {Γ Γ' σ σ'}, {{ Γ ⊢s σ ≈ σ' : Γ' }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
+  Proof with solve [mauto].
+    (* ctxeq_exp_helper *)
+    - intros * HM * HΓΔ. gen Δ.
+      inversion_clear HM;
+        (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper);
+        clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper;
+        intros; destruct (presup_ctx_eq HΓΔ); mauto.
+      all: try (rename B into C); try (rename A0 into B).
+      2-4: assert {{ Δ ⊢ B : Type@i }} as HB by eauto.
+      2-4: assert {{ ⊢ Γ, B ≈ Δ, B }} by mauto; clear HB.
+      2-3: solve [mauto].
+
+      + assert {{ ⊢ Γ, ℕ ≈ Δ, ℕ }} by (econstructor; mauto).
+        assert {{ Δ, ℕ ⊢ B : Type@i }} by mauto.
+        econstructor...
+
+      + econstructor...
+
+      + assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
+
+    (* ctxeq_exp_eq_helper *)
+    - intros * HMM' * HΓΔ. gen Δ.
+      inversion_clear HMM';
+        (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper);
+        clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper;
+        intros; destruct (presup_ctx_eq HΓΔ); mauto.
+      all: try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
+      1-3: assert {{ ⊢ Γ, ℕ ≈ Δ, ℕ }} by (econstructor; mauto).
+      1-3: assert {{ Δ, ℕ ⊢ B : Type@i }} by eauto.
+      1-3: econstructor...
+      1-5: assert {{ Δ ⊢ B : Type@i }} by eauto.
+      1-5: assert {{ ⊢ Γ, B ≈ Δ, B }}...
+
+      + assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
+
+      + inversion_clear HΓΔ as [|? Δ0 ? ? C'].
+        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 *)
+    - intros * Hσ * HΓΔ. gen Δ.
+      inversion_clear Hσ;
+        (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper);
+        clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper;
+        intros; destruct (presup_ctx_eq HΓΔ); mauto.
+      inversion_clear HΓΔ.
+      econstructor...
+
+    (* ctxeq_sub_eq_helper *)
+    - intros * Hσσ' * HΓΔ. gen Δ.
+      inversion_clear Hσσ';
+        (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper);
+        clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper;
+        intros; destruct (presup_ctx_eq HΓΔ); mauto.
+      inversion_clear HΓΔ.
+      eapply wf_sub_eq_conv...
+
+      Unshelve.
+      all: constructor.
+  Qed.
+
+  Lemma ctxeq_exp : forall {Γ Δ M A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M : A }} -> {{ Δ ⊢ M : A }}.
+  Proof.
+    eauto using ctxeq_exp_helper.
+  Qed.
+
+  Lemma ctxeq_exp_eq : forall {Γ Δ M M' A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M ≈ M' : A }} -> {{ Δ ⊢ M ≈ M' : A }}.
+  Proof.
+    eauto using ctxeq_exp_eq_helper.
+  Qed.
+
+  Lemma ctxeq_sub : forall {Γ Δ σ Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ : Γ' }} -> {{ Δ ⊢s σ : Γ' }}.
+  Proof.
+    eauto using ctxeq_sub_helper.
+  Qed.
+
+  Lemma ctxeq_sub_eq : forall {Γ Δ σ σ' Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
+  Proof.
+    eauto using ctxeq_sub_eq_helper.
+  Qed.
+
+  #[export]
+  Hint Resolve ctxeq_exp ctxeq_exp_eq ctxeq_sub ctxeq_sub_eq : mcltt.
+End ctxeq_judg.
+
+Export ctxeq_judg.
+
+Lemma ctx_eq_trans : forall {Γ0 Γ1 Γ2}, {{ ⊢ Γ0 ≈ Γ1 }} -> {{ ⊢ Γ1 ≈ Γ2 }} -> {{ ⊢ Γ0 ≈ Γ2 }}.
+Proof with solve [mauto].
+  intros * HΓ01 HΓ12.
+  gen Γ2.
+  induction HΓ01 as [|Γ0 ? T0 i01 T1]; intros; mauto.
+  rename HΓ12 into HT1Γ12.
+  inversion_clear HT1Γ12 as [|? Γ2' ? i12 T2].
+  clear Γ2; rename Γ2' into Γ2.
+  set (i := max i01 i12).
+  assert {{ Γ0 ⊢ T0 : Type@i }} by mauto using lift_exp_max_left.
+  assert {{ Γ2 ⊢ T2 : Type@i }} by mauto using lift_exp_max_right.
+  assert {{ Γ0 ⊢ T0 ≈ T1 : Type@i }} by mauto using lift_exp_eq_max_left.
+  assert {{ Γ2 ⊢ T1 ≈ T2 : Type@i }} by mauto using lift_exp_eq_max_right.
+  econstructor...
+Qed.
+
+#[export]
+Hint Resolve ctx_eq_trans : mcltt.

theories/Core/Syntactic/Presup.v

@@ -1,4 +1,5 @@
-From Mcltt Require Import Base CtxEquiv LibTactics Relations System.
+From Mcltt Require Import Base CtxEq LibTactics.
+From Mcltt Require Export System.
 Import Syntax_Notations.
 
 #[local]

theories/Core/Syntactic/System.v

@@ -1 +1 @@
-From Mcltt Require Export SystemDefinitions SystemLemmas.
+From Mcltt Require Export System.Definitions System.Lemmas.

theories/Core/Syntactic/SystemLemmas.v → theories/Core/Syntactic/System/Lemmas.v

@@ -1,4 +1,4 @@
-From Mcltt Require Import Base LibTactics SystemDefinitions.
+From Mcltt Require Import Base LibTactics System.Definitions.
 Import Syntax_Notations.
 
 Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}.
@@ -158,14 +158,6 @@ Qed.
 #[export]
 Hint Resolve sub_eq_refl : mcltt.
 
-Lemma ctx_eq_sym : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ ≈ Γ }}.
-Proof with solve [mauto].
-  induction 1...
-Qed.
-
-#[export]
-Hint Resolve ctx_eq_sym : mcltt.
-
 Lemma exp_sub_typ : forall {Δ Γ A σ i}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ A[σ] : Type@i }}.
 Proof.
   mauto.

theories/_CoqProject

@@ -6,22 +6,21 @@
 ./Core/Base.v
 ./Core/Semantic/Domain.v
 ./Core/Semantic/Evaluation.v
-./Core/Semantic/EvaluationDefinitions.v
-./Core/Semantic/EvaluationLemmas.v
+./Core/Semantic/Evaluation/Definitions.v
+./Core/Semantic/Evaluation/Lemmas.v
 ./Core/Semantic/PER.v
-./Core/Semantic/PERDefinitions.v
-./Core/Semantic/PERLemmas.v
+./Core/Semantic/PER/Definitions.v
+./Core/Semantic/PER/Lemmas.v
 ./Core/Semantic/Readback.v
-./Core/Semantic/ReadbackDefinitions.v
-./Core/Semantic/ReadbackLemmas.v
+./Core/Semantic/Readback/Definitions.v
+./Core/Semantic/Readback/Lemmas.v
 ./Core/Semantic/Realizability.v
-./Core/Syntactic/CtxEquiv.v
+./Core/Syntactic/CtxEq.v
 ./Core/Syntactic/Presup.v
-./Core/Syntactic/Relations.v
 ./Core/Syntactic/Syntax.v
 ./Core/Syntactic/System.v
-./Core/Syntactic/SystemDefinitions.v
-./Core/Syntactic/SystemLemmas.v
+./Core/Syntactic/System/Definitions.v
+./Core/Syntactic/System/Lemmas.v
 ./Frontend/Elaborator.v
 ./Frontend/Parser.v
 ./Frontend/ParserExtraction.v