From a1abe3ebe41ea3b2fd0959728e082e83f3910fff Mon Sep 17 00:00:00 2001 From: Jason Hu Date: Tue, 16 Jul 2024 12:39:16 -0400 Subject: [PATCH] finish completeness proof (#133) * finish completeness proof * fix one lemma --- .../Core/Completeness/FundamentalTheorem.v | 121 ++++++------------ theories/Core/Syntactic/System/Definitions.v | 9 +- 2 files changed, 50 insertions(+), 80 deletions(-) diff --git a/theories/Core/Completeness/FundamentalTheorem.v b/theories/Core/Completeness/FundamentalTheorem.v index e8c9e133..16b08798 100644 --- a/theories/Core/Completeness/FundamentalTheorem.v +++ b/theories/Core/Completeness/FundamentalTheorem.v @@ -6,97 +6,60 @@ From Mcltt.Core Require Import Completeness.SubstitutionCases Completeness.TermStructureCases Completeness.UniverseCases - Completeness.VariableCases. + Completeness.VariableCases + Completeness.SubtypingCases. From Mcltt.Core Require Export Completeness.LogicalRelation SystemOpt. Import Domain_Notations. Section completeness_fundamental. - Let ctx_prop Γ (_ : {{ ⊢ Γ }}) : Prop := {{ ⊨ Γ }}. - Let ctx_eq_prop Γ Γ' (_ : {{ ⊢ Γ ≈ Γ' }}) : Prop := {{ ⊨ Γ ≈ Γ' }}. - Let exp_prop Γ M A (_ : {{ Γ ⊢ M : A }}) : Prop := {{ Γ ⊨ M : A }}. - Let exp_eq_prop Γ A M M' (_ : {{ Γ ⊢ M ≈ M' : A }}) : Prop := {{ Γ ⊨ M ≈ M' : A }}. - Let sub_prop Γ σ Δ (_ : {{ Γ ⊢s σ : Δ }}) : Prop := {{ Γ ⊨s σ : Δ }}. - Let sub_eq_prop Γ Δ σ σ' (_ : {{ Γ ⊢s σ ≈ σ' : Δ }}) : Prop := {{ Γ ⊨s σ ≈ σ' : Δ }}. - #[local] - Ltac unfold_prop := - unfold ctx_prop, ctx_eq_prop, exp_prop, exp_eq_prop, sub_prop, sub_eq_prop in *; - clear ctx_prop ctx_eq_prop exp_prop exp_eq_prop sub_prop sub_eq_prop. + Theorem completeness_fundamental : + (forall Γ, {{ ⊢ Γ }} -> {{ ⊨ Γ }}) /\ + (forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}) /\ + (forall Γ M A, {{ Γ ⊢ M : A }} -> {{ Γ ⊨ M : A }}) /\ + (forall Γ A M M', {{ Γ ⊢ M ≈ M' : A }} -> {{ Γ ⊨ M ≈ M' : A }}) /\ + (forall Γ σ Δ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊨s σ : Δ }}) /\ + (forall Γ Δ σ σ', {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ Γ ⊨s σ ≈ σ' : Δ }}) /\ + (forall Γ A A', {{ Γ ⊢ A ⊆ A' }} -> {{ Γ ⊨ A ⊆ A' }}). + Proof. + apply syntactic_wf_mut_ind; + mauto 3. + intros. + apply valid_exp_var; + mauto. + Qed. #[local] - Ltac solve_completeness_fundamental := - unfold_prop; mauto; solve [apply valid_ctx_empty | apply valid_exp_var; mauto]. + Ltac solve_it := pose proof completeness_fundamental; firstorder. + + + Theorem completeness_fundamental_ctx : forall Γ, {{ ⊢ Γ }} -> {{ ⊨ Γ }}. + Proof. solve_it. Qed. + + Theorem completeness_fundamental_ctx_sub : forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}. + Proof. solve_it. Qed. - Theorem completeness_fundamental_ctx : forall Γ (HΓ : {{ ⊢ Γ }}), ctx_prop Γ HΓ. - (* Proof with solve_completeness_fundamental using. *) - (* induction 1 using wf_ctx_mut_ind *) - (* with *) - (* (P0 := ctx_eq_prop) *) - (* (P1 := exp_prop) *) - (* (P2 := exp_eq_prop) *) - (* (P3 := sub_prop) *) - (* (P4 := sub_eq_prop)... *) - (* Qed. *) - Admitted. + Theorem completeness_fundamental_exp : forall Γ M A, {{ Γ ⊢ M : A }} -> {{ Γ ⊨ M : A }}. + Proof. solve_it. Qed. - Theorem completeness_fundamental_ctx_eq : forall Γ Γ' (HΓΓ' : {{ ⊢ Γ ≈ Γ' }}), ctx_eq_prop Γ Γ' HΓΓ'. - (* Proof with solve_completeness_fundamental using. *) - (* induction 1 using wf_ctx_eq_mut_ind *) - (* with *) - (* (P := ctx_prop) *) - (* (P1 := exp_prop) *) - (* (P2 := exp_eq_prop) *) - (* (P3 := sub_prop) *) - (* (P4 := sub_eq_prop)... *) - (* Qed. *) - Admitted. + Theorem completeness_fundamental_exp_eq : forall Γ A M M', {{ Γ ⊢ M ≈ M' : A }} -> {{ Γ ⊨ M ≈ M' : A }}. + Proof. solve_it. Qed. - Theorem completeness_fundamental_exp : forall Γ M A (HM : {{ Γ ⊢ M : A }}), exp_prop Γ M A HM. - (* Proof with solve_completeness_fundamental using. *) - (* induction 1 using wf_exp_mut_ind *) - (* with *) - (* (P := ctx_prop) *) - (* (P0 := ctx_eq_prop) *) - (* (P2 := exp_eq_prop) *) - (* (P3 := sub_prop) *) - (* (P4 := sub_eq_prop)... *) - (* Qed. *) - Admitted. + Theorem completeness_fundamental_sub : forall Γ σ Δ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊨s σ : Δ }}. + Proof. solve_it. Qed. - Theorem completeness_fundamental_exp_eq : forall Γ M M' A (HMM' : {{ Γ ⊢ M ≈ M' : A }}), exp_eq_prop Γ A M M' HMM'. - (* Proof with solve_completeness_fundamental using. *) - (* induction 1 using wf_exp_eq_mut_ind *) - (* with *) - (* (P := ctx_prop) *) - (* (P0 := ctx_eq_prop) *) - (* (P1 := exp_prop) *) - (* (P3 := sub_prop) *) - (* (P4 := sub_eq_prop)... *) - (* Qed. *) - Admitted. + Theorem completeness_fundamental_sub_eq : forall Γ Δ σ σ', {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ Γ ⊨s σ ≈ σ' : Δ }}. + Proof. solve_it. Qed. - Theorem completeness_fundamental_sub : forall Γ σ Δ (Hσ : {{ Γ ⊢s σ : Δ }}), sub_prop Γ σ Δ Hσ. - (* Proof with solve_completeness_fundamental using. *) - (* induction 1 using wf_sub_mut_ind *) - (* with *) - (* (P := ctx_prop) *) - (* (P0 := ctx_eq_prop) *) - (* (P1 := exp_prop) *) - (* (P2 := exp_eq_prop) *) - (* (P4 := sub_eq_prop)... *) - (* Qed. *) - Admitted. + Theorem completeness_fundamental_subtyp : forall Γ A A', {{ Γ ⊢ A ⊆ A' }} -> {{ Γ ⊨ A ⊆ A' }}. + Proof. solve_it. Qed. - Theorem completeness_fundamental_sub_eq : forall Γ σ σ' Δ (Hσσ' : {{ Γ ⊢s σ ≈ σ' : Δ }}), sub_eq_prop Γ Δ σ σ' Hσσ'. - (* Proof with solve_completeness_fundamental using. *) - (* induction 1 using wf_sub_eq_mut_ind *) - (* with *) - (* (P := ctx_prop) *) - (* (P0 := ctx_eq_prop) *) - (* (P1 := exp_prop) *) - (* (P2 := exp_eq_prop) *) - (* (P3 := sub_prop)... *) - (* Qed. *) - Admitted. + Theorem completeness_fundamental_ctx_eq : forall Γ Γ', {{ ⊢ Γ ≈ Γ' }} -> {{ ⊨ Γ ≈ Γ' }}. + Proof. + induction 1. + - apply valid_ctx_empty. + - apply completeness_fundamental_exp_eq in H2. + mauto. + Qed. End completeness_fundamental. diff --git a/theories/Core/Syntactic/System/Definitions.v b/theories/Core/Syntactic/System/Definitions.v index d878848b..06e436d7 100644 --- a/theories/Core/Syntactic/System/Definitions.v +++ b/theories/Core/Syntactic/System/Definitions.v @@ -324,7 +324,14 @@ with wf_exp_eq_mut_ind := Induction for wf_exp_eq Sort Prop with wf_sub_mut_ind := Induction for wf_sub Sort Prop with wf_sub_eq_mut_ind := Induction for wf_sub_eq Sort Prop with wf_subtyping_mut_ind := Induction for wf_subtyping Sort Prop. - +Combined Scheme syntactic_wf_mut_ind from + wf_ctx_mut_ind, + wf_ctx_sub_mut_ind, + wf_exp_mut_ind, + wf_exp_eq_mut_ind, + wf_sub_mut_ind, + wf_sub_eq_mut_ind, + wf_subtyping_mut_ind. Inductive wf_ctx_eq : ctx -> ctx -> Prop := | wf_ctx_eq_empty : {{ ⊢ ⋅ ≈ ⋅ }}