From 6a2d1a19789ae52ffbf43c6cd915dda220c4484a Mon Sep 17 00:00:00 2001 From: HuStmpHrrr Date: Thu, 27 Jun 2024 16:36:25 -0400 Subject: [PATCH] finish completeness proof using only co-variant subtyping --- theories/Algorithmic/Subtyping/Definitions.v | 2 +- theories/Algorithmic/Subtyping/Lemmas.v | 68 ++++++++++--------- .../Core/Completeness/Consequences/Rules.v | 23 +++++++ theories/LibTactics.v | 4 +- theories/_CoqProject | 1 + 5 files changed, 64 insertions(+), 34 deletions(-) create mode 100644 theories/Core/Completeness/Consequences/Rules.v diff --git a/theories/Algorithmic/Subtyping/Definitions.v b/theories/Algorithmic/Subtyping/Definitions.v index bf97797d..22b53a5a 100644 --- a/theories/Algorithmic/Subtyping/Definitions.v +++ b/theories/Algorithmic/Subtyping/Definitions.v @@ -21,7 +21,7 @@ Inductive alg_subtyping_nf : nf -> nf -> Prop := i <= j -> {{ ⊢anf Type@i ⊆ Type@j }} | asnf_pi : forall A B A' B', - {{ ⊢anf A' ⊆ A }} -> + A = A' -> {{ ⊢anf B ⊆ B' }} -> {{ ⊢anf Π A B ⊆ Π A' B' }} where "⊢anf M ⊆ N" := (alg_subtyping_nf M N) (in custom judg) : type_scope. diff --git a/theories/Algorithmic/Subtyping/Lemmas.v b/theories/Algorithmic/Subtyping/Lemmas.v index df8ff1fa..446f6c74 100644 --- a/theories/Algorithmic/Subtyping/Lemmas.v +++ b/theories/Algorithmic/Subtyping/Lemmas.v @@ -1,5 +1,6 @@ From Mcltt Require Import Base LibTactics. -From Mcltt.Core Require Import System Evaluation Readback NbE CoreTypeInversions Presup CtxSub. +From Mcltt.Core Require Import System Evaluation Readback NbE CoreTypeInversions Presup CtxSub SystemOpt. +From Mcltt.Core.Completeness Require Import Consequences.Rules. From Mcltt Require Import Completeness Soundness. From Mcltt.Algorithmic Require Import Subtyping.Definitions. Import Syntax_Notations. @@ -32,8 +33,8 @@ Proof. fail_if_dup end. apply_subtyping. - deepexec IHalg_subtyping_nf1 ltac:(fun H => pose proof H). - eapply wf_subtyp_pi with (i := i); mauto. + deepexec IHalg_subtyping_nf ltac:(fun H => pose proof H). + mauto 3. Qed. Lemma alg_subtyping_nf_trans : forall M1 M0 M2, @@ -74,31 +75,36 @@ Qed. Hint Resolve alg_subtyping_trans : mcltt. -(* Lemma alg_subtyping_complete : forall Γ M N, *) -(* {{ Γ ⊢ M ⊆ N }} -> *) -(* {{ Γ ⊢a M ⊆ N }}. *) -(* Proof. *) -(* induction 1; mauto. *) -(* - apply completeness in H. *) -(* destruct H as [W [? ?]]. *) -(* econstructor; mauto. *) -(* - assert {{ Γ ⊢ Type@i : Type@(S i) }} by mauto. *) -(* assert {{ Γ ⊢ Type@j : Type@(S j) }} by mauto. *) -(* apply soundness in H1. *) -(* apply soundness in H2. *) -(* destruct_all. *) -(* econstructor; try eassumption. *) -(* progressive_inversion. *) -(* mauto. *) -(* - assert {{ Γ ⊢ Π A B : Type@i }} as HΠ1 by mauto. *) -(* assert {{ Γ ⊢ Π A' B' : Type@i }} as HΠ2 by mauto. *) -(* apply soundness in HΠ1. *) -(* apply soundness in HΠ2. *) -(* destruct_all. *) -(* econstructor; try eassumption. *) -(* progressive_inversion. *) -(* simpl in *. *) -(* functional_initial_env_rewrite_clear. *) -(* simplify_evals. *) -(* functional_read_rewrite_clear. *) -(* eapply asnf_pi; trivial. *) +Lemma alg_subtyping_complete : forall Γ M N, + {{ Γ ⊢ M ⊆ N }} -> + {{ Γ ⊢a M ⊆ N }}. +Proof. + induction 1; mauto. + - apply completeness in H. + destruct H as [W [? ?]]. + econstructor; mauto. + - assert {{ Γ ⊢ Type@i : Type@(S i) }} by mauto. + assert {{ Γ ⊢ Type@j : Type@(S j) }} by mauto. + on_all_hyp: fun H => apply soundness in H. + destruct_all. + econstructor; try eassumption. + progressive_inversion. + mauto. + - assert {{ Γ ⊢ Π A B : Type@i }} as HΠ1 by mauto. + assert {{ Γ ⊢ Π A' B' : Type@i }} as HΠ2 by mauto. + assert {{ ⊢ Γ , A ≈ Γ , A' }} by mauto. + eapply ctxeq_nbe_eq in H5; [ |eassumption]. + match goal with + | H : _ |- _ => apply completeness in H + end. + apply soundness in HΠ1. + apply soundness in HΠ2. + destruct_all. + econstructor; try eassumption. + progressive_inversion. + simpl in *. + functional_initial_env_rewrite_clear. + simplify_evals. + functional_read_rewrite_clear. + eapply asnf_pi; trivial. +Qed. diff --git a/theories/Core/Completeness/Consequences/Rules.v b/theories/Core/Completeness/Consequences/Rules.v new file mode 100644 index 00000000..e30e0fc8 --- /dev/null +++ b/theories/Core/Completeness/Consequences/Rules.v @@ -0,0 +1,23 @@ +From Coq Require Import RelationClasses. +From Mcltt Require Import Base LibTactics. +From Mcltt.Core Require Import Completeness Completeness.FundamentalTheorem Completeness.LogicalRelation Semantic.Realizability PER. +From Mcltt.Core Require Export SystemOpt. +Import Domain_Notations. + +Lemma ctxeq_nbe_eq : forall Γ Γ' M A, + {{ Γ ⊢ M : A }} -> + {{ ⊢ Γ ≈ Γ' }} -> + exists w, nbe Γ M A w /\ nbe Γ' M A w. +Proof. + intros ? ? ? ? [envR [Henv [i ?]]]%completeness_fundamental_exp [envR' Henv']%completeness_fundamental_ctx_eq. + handle_per_ctx_env_irrel. + destruct (per_ctx_then_per_env_initial_env Henv') as [p [p' [? [? ?]]]]. + deepexec H ltac:(fun H => destruct H as [R [? ?]]). + progressive_inversion. + deepexec @per_elem_then_per_top ltac:(fun H => destruct H as [w [? ?]]). + exists w. + split; econstructor; eauto. + erewrite per_ctx_respects_length; try eassumption. + eexists. symmetry. + eassumption. +Qed. diff --git a/theories/LibTactics.v b/theories/LibTactics.v index 27b1aaf3..65bcd431 100644 --- a/theories/LibTactics.v +++ b/theories/LibTactics.v @@ -267,7 +267,7 @@ Ltac deepexec lem tac := lazymatch type of T with | Prop => match goal with | H : _ |- _ => unify x H - | _ => idtac + | _ => tac lem end | _ => idtac end; @@ -294,7 +294,7 @@ Ltac cutexec lem C tac := (lazymatch type of T with | Prop => match goal with | H : _ |- _ => unify x H - | _ => idtac + | _ => tac lem end | _ => idtac end; diff --git a/theories/_CoqProject b/theories/_CoqProject index 0c194eb3..ea5d4a00 100644 --- a/theories/_CoqProject +++ b/theories/_CoqProject @@ -6,6 +6,7 @@ ./Algorithmic/Subtyping/Lemmas.v ./Core/Axioms.v ./Core/Base.v +./Core/Completeness/Consequences/Rules.v ./Core/Completeness/Consequences/Types.v ./Core/Completeness/Consequences/Inversions.v ./Core/Completeness/ContextCases.v