From df75a3107c40633ab532ad2a9f1e666c7792fbd9 Mon Sep 17 00:00:00 2001 From: "Junyoung/\"Clare\" Jang" Date: Thu, 9 May 2024 00:00:17 -0400 Subject: [PATCH] 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 | 2 +- .../Definitions.v} | 0 .../Lemmas.v} | 2 +- theories/Core/Semantic/PER.v | 2 +- .../{PERDefinitions.v => PER/Definitions.v} | 0 .../Semantic/{PERLemmas.v => PER/Lemmas.v} | 2 +- theories/Core/Semantic/Readback.v | 2 +- .../Definitions.v} | 0 .../{ReadbackLemmas.v => Readback/Lemmas.v} | 2 +- theories/Core/Syntactic/CtxEq.v | 144 ++++++++++++++++++ theories/Core/Syntactic/CtxEquiv.v | 103 ------------- theories/Core/Syntactic/Presup.v | 3 +- theories/Core/Syntactic/Relations.v | 42 ----- theories/Core/Syntactic/System.v | 2 +- .../Definitions.v} | 0 .../{SystemLemmas.v => System/Lemmas.v} | 10 +- theories/_CoqProject | 19 ++- 17 files changed, 163 insertions(+), 172 deletions(-) rename theories/Core/Semantic/{EvaluationDefinitions.v => Evaluation/Definitions.v} (100%) rename theories/Core/Semantic/{EvaluationLemmas.v => Evaluation/Lemmas.v} (98%) rename theories/Core/Semantic/{PERDefinitions.v => PER/Definitions.v} (100%) rename theories/Core/Semantic/{PERLemmas.v => PER/Lemmas.v} (99%) rename theories/Core/Semantic/{ReadbackDefinitions.v => Readback/Definitions.v} (100%) rename theories/Core/Semantic/{ReadbackLemmas.v => Readback/Lemmas.v} (97%) create mode 100644 theories/Core/Syntactic/CtxEq.v delete mode 100644 theories/Core/Syntactic/CtxEquiv.v delete mode 100644 theories/Core/Syntactic/Relations.v rename theories/Core/Syntactic/{SystemDefinitions.v => System/Definitions.v} (100%) rename theories/Core/Syntactic/{SystemLemmas.v => System/Lemmas.v} (99%) diff --git a/theories/Core/Semantic/Evaluation.v b/theories/Core/Semantic/Evaluation.v index bbe67f65..b14afbf7 100644 --- a/theories/Core/Semantic/Evaluation.v +++ b/theories/Core/Semantic/Evaluation.v @@ -1 +1 @@ -From Mcltt Require Export EvaluationDefinitions EvaluationLemmas. +From Mcltt Require Export Evaluation.Definitions Evaluation.Lemmas. diff --git a/theories/Core/Semantic/EvaluationDefinitions.v b/theories/Core/Semantic/Evaluation/Definitions.v similarity index 100% rename from theories/Core/Semantic/EvaluationDefinitions.v rename to theories/Core/Semantic/Evaluation/Definitions.v diff --git a/theories/Core/Semantic/EvaluationLemmas.v b/theories/Core/Semantic/Evaluation/Lemmas.v similarity index 98% rename from theories/Core/Semantic/EvaluationLemmas.v rename to theories/Core/Semantic/Evaluation/Lemmas.v index 00ee3b27..f194bead 100644 --- a/theories/Core/Semantic/EvaluationLemmas.v +++ b/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. diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v index e749f9a8..3547a029 100644 --- a/theories/Core/Semantic/PER.v +++ b/theories/Core/Semantic/PER.v @@ -1 +1 @@ -From Mcltt Require Export PERDefinitions PERLemmas. +From Mcltt Require Export PER.Definitions PER.Lemmas. diff --git a/theories/Core/Semantic/PERDefinitions.v b/theories/Core/Semantic/PER/Definitions.v similarity index 100% rename from theories/Core/Semantic/PERDefinitions.v rename to theories/Core/Semantic/PER/Definitions.v diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PER/Lemmas.v similarity index 99% rename from theories/Core/Semantic/PERLemmas.v rename to theories/Core/Semantic/PER/Lemmas.v index 57778502..858203b4 100644 --- a/theories/Core/Semantic/PERLemmas.v +++ b/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, diff --git a/theories/Core/Semantic/Readback.v b/theories/Core/Semantic/Readback.v index 9a282331..21f4329a 100644 --- a/theories/Core/Semantic/Readback.v +++ b/theories/Core/Semantic/Readback.v @@ -1 +1 @@ -From Mcltt Require Export ReadbackDefinitions ReadbackLemmas. +From Mcltt Require Export Readback.Definitions Readback.Lemmas. diff --git a/theories/Core/Semantic/ReadbackDefinitions.v b/theories/Core/Semantic/Readback/Definitions.v similarity index 100% rename from theories/Core/Semantic/ReadbackDefinitions.v rename to theories/Core/Semantic/Readback/Definitions.v diff --git a/theories/Core/Semantic/ReadbackLemmas.v b/theories/Core/Semantic/Readback/Lemmas.v similarity index 97% rename from theories/Core/Semantic/ReadbackLemmas.v rename to theories/Core/Semantic/Readback/Lemmas.v index 30001af9..2b303fd4 100644 --- a/theories/Core/Semantic/ReadbackLemmas.v +++ b/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. diff --git a/theories/Core/Syntactic/CtxEq.v b/theories/Core/Syntactic/CtxEq.v new file mode 100644 index 00000000..34517e9a --- /dev/null +++ b/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. diff --git a/theories/Core/Syntactic/CtxEquiv.v b/theories/Core/Syntactic/CtxEquiv.v deleted file mode 100644 index b58996a6..00000000 --- a/theories/Core/Syntactic/CtxEquiv.v +++ /dev/null @@ -1,103 +0,0 @@ -From Mcltt Require Import Base LibTactics System. -Import Syntax_Notations. - -#[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. - -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. diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v index fcb1f2b3..94b86e53 100644 --- a/theories/Core/Syntactic/Presup.v +++ b/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] diff --git a/theories/Core/Syntactic/Relations.v b/theories/Core/Syntactic/Relations.v deleted file mode 100644 index 23f9fda5..00000000 --- a/theories/Core/Syntactic/Relations.v +++ /dev/null @@ -1,42 +0,0 @@ -From Coq Require Import Setoid. -From Mcltt Require Import Base CtxEquiv LibTactics 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_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. - -Add Relation (ctx) (wf_ctx_eq) - symmetry proved by @ctx_eq_sym - transitivity proved by @ctx_eq_trans - as ctx_eq. - -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) (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/System.v b/theories/Core/Syntactic/System.v index 0e9ab2b1..16ba6364 100644 --- a/theories/Core/Syntactic/System.v +++ b/theories/Core/Syntactic/System.v @@ -1 +1 @@ -From Mcltt Require Export SystemDefinitions SystemLemmas. +From Mcltt Require Export System.Definitions System.Lemmas. diff --git a/theories/Core/Syntactic/SystemDefinitions.v b/theories/Core/Syntactic/System/Definitions.v similarity index 100% rename from theories/Core/Syntactic/SystemDefinitions.v rename to theories/Core/Syntactic/System/Definitions.v diff --git a/theories/Core/Syntactic/SystemLemmas.v b/theories/Core/Syntactic/System/Lemmas.v similarity index 99% rename from theories/Core/Syntactic/SystemLemmas.v rename to theories/Core/Syntactic/System/Lemmas.v index ff657031..e16fa52b 100644 --- a/theories/Core/Syntactic/SystemLemmas.v +++ b/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. diff --git a/theories/_CoqProject b/theories/_CoqProject index c714ab5f..a78ff45f 100644 --- a/theories/_CoqProject +++ b/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