From 1e6f531df8f4cf8020a45e9ed770ff13741cd441 Mon Sep 17 00:00:00 2001 From: Jason Hu Date: Mon, 29 Jul 2024 19:57:07 -0400 Subject: [PATCH] working on realizability (#140) * working on realizability * add a few more cases * reorganize * keep moving * improve autorewrite a bit * more rewrite tricks * keep working on more lemmas * need a few more morphisms * readjusted the order of the arguments * keep moving forward * keep moving forward * keep moving forward * finish proof * prettify * finish the lemmas * use this definition instead * comment out lemma * flip instantiation * Update theories/Core/Syntactic/SystemOpt.v Co-authored-by: Junyoung/"Clare" Jang * move theorems --------- Co-authored-by: Junyoung/"Clare" Jang --- .../Core/Completeness/FundamentalTheorem.v | 4 +- theories/Core/Semantic/PER/Lemmas.v | 11 + theories/Core/Semantic/Realizability.v | 8 + .../Soundness/LogicalRelation/Definitions.v | 58 +-- .../Core/Soundness/LogicalRelation/Lemmas.v | 67 +++- theories/Core/Soundness/Realizability.v | 357 ++++++++++++++++++ .../Core/Soundness/Weakening/Definition.v | 3 +- theories/Core/Soundness/Weakening/Lemmas.v | 52 ++- theories/Core/Syntactic/Corollaries.v | 101 ++++- theories/Core/Syntactic/CtxEq.v | 4 +- theories/Core/Syntactic/CtxSub.v | 9 +- theories/Core/Syntactic/Syntax.v | 6 +- theories/Core/Syntactic/System/Definitions.v | 57 ++- theories/Core/Syntactic/System/Lemmas.v | 11 - theories/Core/Syntactic/SystemOpt.v | 16 + theories/LibTactics.v | 29 ++ theories/_CoqProject | 1 + 17 files changed, 717 insertions(+), 77 deletions(-) create mode 100644 theories/Core/Soundness/Realizability.v diff --git a/theories/Core/Completeness/FundamentalTheorem.v b/theories/Core/Completeness/FundamentalTheorem.v index 16b08798..37d49f20 100644 --- a/theories/Core/Completeness/FundamentalTheorem.v +++ b/theories/Core/Completeness/FundamentalTheorem.v @@ -16,9 +16,9 @@ Section completeness_fundamental. Theorem completeness_fundamental : (forall Γ, {{ ⊢ Γ }} -> {{ ⊨ Γ }}) /\ (forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}) /\ - (forall Γ M A, {{ Γ ⊢ M : A }} -> {{ Γ ⊨ M : A }}) /\ + (forall Γ A M, {{ Γ ⊢ M : A }} -> {{ Γ ⊨ M : A }}) /\ (forall Γ A M M', {{ Γ ⊢ M ≈ M' : A }} -> {{ Γ ⊨ M ≈ M' : A }}) /\ - (forall Γ σ Δ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊨s σ : Δ }}) /\ + (forall Γ Δ σ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊨s σ : Δ }}) /\ (forall Γ Δ σ σ', {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ Γ ⊨s σ ≈ σ' : Δ }}) /\ (forall Γ A A', {{ Γ ⊢ A ⊆ A' }} -> {{ Γ ⊨ A ⊆ A' }}). Proof. diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v index d4f22fc7..b372cb89 100644 --- a/theories/Core/Semantic/PER/Lemmas.v +++ b/theories/Core/Semantic/PER/Lemmas.v @@ -235,6 +235,17 @@ Proof. [setoid_rewrite <- HRR' | setoid_rewrite HRR']; eassumption. Qed. +Lemma domain_app_per : forall f f' a a', + {{ Dom f ≈ f' ∈ per_bot }} -> + {{ Dom a ≈ a' ∈ per_top }} -> + {{ Dom f a ≈ f' a' ∈ per_bot }}. +Proof. + intros. intros s. + destruct (H s) as [? []]. + destruct (H0 s) as [? []]. + mauto. +Qed. + Ltac rewrite_relation_equivalence_left := repeat match goal with | H : ?R1 <~> ?R2 |- _ => diff --git a/theories/Core/Semantic/Realizability.v b/theories/Core/Semantic/Realizability.v index 59dcc164..40d8c753 100644 --- a/theories/Core/Semantic/Realizability.v +++ b/theories/Core/Semantic/Realizability.v @@ -110,3 +110,11 @@ Proof. erewrite per_ctx_respects_length; mauto. eexists; eauto. Qed. + +Lemma var_per_elem : forall {A B i R} n, + {{ DF A ≈ B ∈ per_univ_elem i ↘ R }} -> + {{ Dom ⇑! A n ≈ ⇑! B n ∈ R }}. +Proof. + intros. + eapply per_bot_then_per_elem; mauto. +Qed. diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v index 9cc28eed..e632dea0 100644 --- a/theories/Core/Soundness/LogicalRelation/Definitions.v +++ b/theories/Core/Soundness/LogicalRelation/Definitions.v @@ -16,10 +16,10 @@ Notation "'glu_typ_pred_equivalence'" := (@predicate_equivalence glu_typ_pred_ar (* This type annotation is to distinguish this notation from others *) Notation "Γ ⊢ A ® R" := ((R Γ A : Prop) : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, A custom exp, R constr). -Notation "'glu_exp_pred_args'" := (Tcons ctx (Tcons exp (Tcons typ (Tcons domain Tnil)))). +Notation "'glu_exp_pred_args'" := (Tcons ctx (Tcons typ (Tcons exp (Tcons domain Tnil)))). Notation "'glu_exp_pred'" := (predicate glu_exp_pred_args). Notation "'glu_exp_pred_equivalence'" := (@predicate_equivalence glu_exp_pred_args) (only parsing). -Notation "Γ ⊢ M : A ® m ∈ R" := (R Γ M A m : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp, m custom domain, R constr). +Notation "Γ ⊢ M : A ® m ∈ R" := (R Γ A M m : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp, m custom domain, R constr). Notation "'glu_sub_pred_args'" := (Tcons ctx (Tcons sub (Tcons env Tnil))). Notation "'glu_sub_pred'" := (predicate glu_sub_pred_args). @@ -48,7 +48,7 @@ Hint Constructors glu_nat : mcltt. Definition nat_glu_typ_pred i : glu_typ_pred := fun Γ M => {{ Γ ⊢ M ≈ ℕ : Type@i }}. Arguments nat_glu_typ_pred i Γ M/. -Definition nat_glu_exp_pred i : glu_exp_pred := fun Γ m M a => {{ Γ ⊢ M ® nat_glu_typ_pred i }} /\ glu_nat Γ m a. +Definition nat_glu_exp_pred i : glu_exp_pred := fun Γ M m a => {{ Γ ⊢ M ® nat_glu_typ_pred i }} /\ glu_nat Γ m a. Arguments nat_glu_exp_pred i Γ m M a/. Definition neut_glu_typ_pred i C : glu_typ_pred := @@ -73,6 +73,7 @@ Inductive pi_glu_typ_pred i (OP : forall c (equiv_c : {{ Dom c ≈ c ∈ IR }}), glu_typ_pred) : glu_typ_pred := | mk_pi_glu_typ_pred : `{ {{ Γ ⊢ M ≈ Π IT OT : Type@i }} -> + {{ Γ ⊢ IT : Type@i }} -> {{ Γ , IT ⊢ OT : Type@i }} -> (forall Δ σ, {{ Δ ⊢w σ : Γ }} -> {{ Δ ⊢ IT[σ] ® IP }}) -> (forall Δ σ m a, @@ -92,6 +93,7 @@ Inductive pi_glu_exp_pred i `{ {{ Γ ⊢ m : M }} -> {{ Dom a ≈ a ∈ elem_rel }} -> {{ Γ ⊢ M ≈ Π IT OT : Type@i }} -> + {{ Γ ⊢ IT : Type@i }} -> {{ Γ , IT ⊢ OT : Type@i }} -> (forall Δ σ, {{ Δ ⊢w σ : Γ }} -> {{ Δ ⊢ IT[σ] ® IP }}) -> (forall Δ σ m' b, @@ -113,7 +115,7 @@ Section Gluing. (glu_univ_typ_rec : forall {j}, j < i -> domain -> glu_typ_pred). Definition univ_glu_exp_pred' {j} (lt_j_i : j < i) : glu_exp_pred := - fun Γ m M A => + fun Γ M m A => {{ Γ ⊢ m : M }} /\ {{ Γ ⊢ M ≈ Type@j : Type@i }} /\ {{ Γ ⊢ m ® glu_univ_typ_rec lt_j_i A }}. @@ -172,7 +174,7 @@ Definition glu_univ_typ (i : nat) (A : domain) : glu_typ_pred := Arguments glu_univ_typ i A Γ M/. Definition univ_glu_exp_pred j i : glu_exp_pred := - fun Γ m M A => + fun Γ M m A => {{ Γ ⊢ m : M }} /\ {{ Γ ⊢ M ≈ Type@j : Type@i }} /\ {{ Γ ⊢ m ® glu_univ_typ j A }}. Arguments univ_glu_exp_pred j i Γ t T a/. @@ -250,28 +252,38 @@ Section GluingInduction. Qed. End GluingInduction. -Inductive glu_neut i A Γ m M c : Prop := -| mk_glu_neut : - {{ Γ ⊢ m : M }} -> - {{ Γ ⊢ M ® glu_univ_typ i A }} -> +Inductive glu_elem_bot i A Γ T t c : Prop := +| glu_elem_bot_make : forall P El, + {{ Γ ⊢ t : T }} -> + {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} -> + {{ Γ ⊢ T ® P }} -> {{ Dom c ≈ c ∈ per_bot }} -> - (forall Δ σ a, {{ Δ ⊢w σ : Γ }} -> {{ Rne c in length Δ ↘ a }} -> {{ Δ ⊢ m[σ] ≈ a : M[σ] }}) -> - {{ Γ ⊢ m : M ® c ∈ glu_neut i A }}. + (forall Δ σ w, {{ Δ ⊢w σ : Γ }} -> {{ Rne c in length Δ ↘ w }} -> {{ Δ ⊢ t [ σ ] ≈ w : T [ σ ] }}) -> + {{ Γ ⊢ t : T ® c ∈ glu_elem_bot i A }}. +#[export] + Hint Constructors glu_elem_bot : mcltt. -Inductive glu_norm i A Γ m M a : Prop := -| mk_glu_norm : - {{ Γ ⊢ m : M }} -> - {{ Γ ⊢ M ® glu_univ_typ i A }} -> - {{ Dom ⇓ A a ≈ ⇓ A a ∈ per_top }} -> - (forall Δ σ b, {{ Δ ⊢w σ : Γ }} -> {{ Rnf ⇓ A a in length Δ ↘ b }} -> {{ Δ ⊢ m [ σ ] ≈ b : M [ σ ] }}) -> - {{ Γ ⊢ m : M ® a ∈ glu_norm i A }}. -Inductive glu_typ i A Γ M : Prop := -| mk_glu_typ : forall P El, - {{ Γ ⊢ M : Type@i }} -> +Inductive glu_elem_top i A Γ T t a : Prop := +| glu_elem_top_make : forall P El, + {{ Γ ⊢ t : T }} -> {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} -> - (forall Δ σ a, {{ Δ ⊢w σ : Γ }} -> {{ Rtyp A in length Δ ↘ a }} -> {{ Δ ⊢ M[σ] ≈ a : Type@i }}) -> - {{ Γ ⊢ M ® glu_typ i A }}. + {{ Γ ⊢ T ® P }} -> + {{ Dom ⇓ A a ≈ ⇓ A a ∈ per_top }} -> + (forall Δ σ w, {{ Δ ⊢w σ : Γ }} -> {{ Rnf ⇓ A a in length Δ ↘ w }} -> {{ Δ ⊢ t [ σ ] ≈ w : T [ σ ] }}) -> + {{ Γ ⊢ t : T ® a ∈ glu_elem_top i A }}. +#[export] + Hint Constructors glu_elem_top : mcltt. + + +Inductive glu_typ_top i A Γ T : Prop := +| glu_typ_top_make : + {{ Γ ⊢ T : Type@i }} -> + {{ Dom A ≈ A ∈ per_top_typ }} -> + (forall Δ σ W, {{ Δ ⊢w σ : Γ }} -> {{ Rtyp A in length Δ ↘ W }} -> {{ Δ ⊢ T [ σ ] ≈ W : Type@i }}) -> + {{ Γ ⊢ T ® glu_typ_top i A }}. +#[export] + Hint Constructors glu_typ_top : mcltt. Ltac invert_glu_rel1 := match goal with diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v index bb5c5a2b..5347b0c0 100644 --- a/theories/Core/Soundness/LogicalRelation/Lemmas.v +++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v @@ -15,7 +15,7 @@ Lemma pi_glu_exp_pred_pi_glu_typ_pred : forall i IR IP IEl (OP : forall c (equiv Proof. inversion_clear 1; econstructor; eauto. intros. - edestruct H5 as [? []]; eauto. + edestruct H6 as [? []]; eauto. Qed. Lemma glu_nat_per_nat : forall Γ m a, @@ -113,6 +113,16 @@ Proof. assert {{ Δ ⊢ T[σ] ≈ V : Type@i }}; mauto. Qed. + +Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ : (P Γ) + with signature wf_exp_eq Γ {{{Type@i}}} ==> iff as glu_univ_elem_typ_morphism_iff1. +Proof. + intros. split; intros; + eapply glu_univ_elem_typ_resp_equiv; + mauto 2. +Qed. + + Lemma glu_univ_elem_trm_resp_typ_equiv : forall i P El A, {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} -> forall Γ t T a T', @@ -128,6 +138,14 @@ Proof. assert {{ Δ ⊢ M[σ] ≈ V : Type@i }}; mauto. Qed. +Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ : (El Γ) + with signature wf_exp_eq Γ {{{Type@i}}} ==> eq ==> eq ==> iff as glu_univ_elem_elem_morphism_iff1. +Proof. + split; intros; + eapply glu_univ_elem_trm_resp_typ_equiv; + mauto 2. +Qed. + Lemma glu_univ_elem_typ_resp_ctx_equiv : forall i P El A, {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} -> forall Γ T Δ, @@ -141,6 +159,15 @@ Proof. econstructor; mauto. Qed. +Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) : P + with signature wf_ctx_eq ==> eq ==> iff as glu_univ_elem_typ_morphism_iff2. +Proof. + intros. split; intros; + eapply glu_univ_elem_typ_resp_ctx_equiv; + mauto 2. +Qed. + + Lemma glu_nat_resp_wk' : forall Γ m a, glu_nat Γ m a -> forall Δ σ, @@ -242,7 +269,7 @@ Proof. match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H). intros. destruct_rel_mod_eval. - edestruct H11 as [? []]; eauto. + edestruct H12 as [? []]; eauto. Qed. Lemma glu_univ_elem_trm_univ_lvl : forall i P El A, @@ -274,7 +301,7 @@ Proof. intros. destruct_rel_mod_eval. assert {{ Δ ⊢ m' : IT [σ]}} by eauto using glu_univ_elem_trm_escape. - edestruct H12 as [? []]; eauto. + edestruct H13 as [? []]; eauto. eexists; split; eauto. enough {{ Δ ⊢ m[σ] m' ≈ t'[σ] m' : OT[σ,,m'] }} by eauto. assert {{ Γ ⊢ m ≈ t' : Π IT OT }} as Hty by mauto. @@ -289,6 +316,16 @@ Proof. mauto 4. Qed. + +Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ T : (El Γ T) + with signature wf_exp_eq Γ T ==> eq ==> iff as glu_univ_elem_elem_morphism_iff2. +Proof. + split; intros; + eapply glu_univ_elem_trm_resp_equiv; + mauto 2. +Qed. + + Lemma glu_univ_elem_core_univ' : forall j i typ_rel el_rel, j < i -> (typ_rel <∙> univ_glu_typ_pred j i) -> @@ -482,7 +519,7 @@ Proof. do 4 eexists. repeat split. 1: eassumption. - 1: instantiate (1 := fun c equiv_c Γ M A m => forall (b : domain) Pb Elb, + 1: instantiate (1 := fun c equiv_c Γ A M m => forall (b : domain) Pb Elb, {{ ⟦ B ⟧ p ↦ c ↘ b }} -> {{ DG b ∈ glu_univ_elem i ↘ Pb ↘ Elb }} -> {{ Γ ⊢ M : A ® m ∈ Elb }}). @@ -496,7 +533,7 @@ Proof. assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv0_c ↘ OEl c equiv0_c }} by mauto 3. apply -> simple_glu_univ_elem_morphism_iff; [| reflexivity | |]; [eauto | |]. + intros ? ? ? ?. - split; [intros; handle_functional_glu_univ_elem |]; intuition. + split; intros; handle_functional_glu_univ_elem; intuition. + intros ? ?. split; [intros; handle_functional_glu_univ_elem |]; intuition. - rename a0 into c. @@ -596,7 +633,7 @@ Proof. do 2 eexists. glu_univ_elem_econstructor; try (eassumption + reflexivity). + saturate_refl; eassumption. - + instantiate (1 := fun (c : domain) (equiv_c : in_rel c c) Γ M A m => + + instantiate (1 := fun (c : domain) (equiv_c : in_rel c c) Γ A M m => forall b P El, {{ ⟦ B' ⟧ p' ↦ c ↘ b }} -> glu_univ_elem i P El b -> @@ -620,6 +657,22 @@ Proof. glu_univ_elem_econstructor; try reflexivity; mauto. Qed. +Ltac saturate_glu_info1 := + match goal with + | H : glu_univ_elem _ ?P _ _, + H1 : ?P _ _ |- _ => + pose proof (glu_univ_elem_univ_lvl _ _ _ _ H _ _ H1); + fail_if_dup + | H : glu_univ_elem _ _ ?El _, + H1 : ?El _ _ _ _ |- _ => + pose proof (glu_univ_elem_trm_escape _ _ _ _ H _ _ _ _ H1); + fail_if_dup + end. + +Ltac saturate_glu_info := + clear_dups; + repeat saturate_glu_info1. + (* TODO: strengthen the result (implication from P to P' / El to El') *) Lemma glu_univ_elem_cumu_ge : forall {i j a P El}, i <= j -> @@ -635,7 +688,7 @@ Proof. destruct_conjs. do 2 eexists. glu_univ_elem_econstructor; try reflexivity; mauto. - instantiate (1 := fun c equiv_c Γ M A m => forall b Pb Elb, + instantiate (1 := fun c equiv_c Γ A M m => forall b Pb Elb, {{ ⟦ B ⟧ p ↦ c ↘ b }} -> glu_univ_elem j Pb Elb b -> {{ Γ ⊢ M : A ® m ∈ Elb }}). diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v new file mode 100644 index 00000000..125c4bea --- /dev/null +++ b/theories/Core/Soundness/Realizability.v @@ -0,0 +1,357 @@ +From Coq Require Import Nat. + +From Mcltt Require Import Base LibTactics. +From Mcltt.Core.Syntactic Require Import CtxSub SystemOpt Corollaries CoreInversions. +From Mcltt.Core Require Import PER. +From Mcltt.Core.Semantic Require Import Realizability Readback. +From Mcltt.Core.Soundness Require Export LogicalRelation Weakening. +Import Domain_Notations. + +Open Scope list_scope. + +Lemma wf_ctx_sub_ctx_lookup : forall n T Γ, + {{ #n : T ∈ Γ }} -> + forall Δ, + {{ ⊢ Δ ⊆ Γ}} -> + exists Δ1 T0 Δ2 T', + Δ = Δ1 ++ T0 :: Δ2 /\ + n = length Δ1 /\ + T' = iter (S n) (fun T => {{{T [ Wk ]}}}) T0 /\ + {{ #n : T' ∈ Δ }} /\ + {{ Δ ⊢ T' ⊆ T }}. +Proof. + induction 1; intros; progressive_inversion. + - exists nil. + repeat eexists; mauto 4. + - edestruct IHctx_lookup as [Δ1 [? [? [? [? [? [? []]]]]]]]; eauto. + exists (A0 :: Δ1). subst. + repeat eexists; mauto 4. +Qed. + + +Lemma var_arith : forall Γ1 Γ2 (T : typ), + length (Γ1 ++ T :: Γ2) - length Γ2 - 1 = length Γ1. +Proof. + intros. + rewrite List.app_length. simpl. + lia. +Qed. + +Lemma var_weaken_gen : forall Δ σ Γ, + {{ Δ ⊢w σ : Γ }} -> + forall Γ1 Γ2 T, + Γ = Γ1 ++ T :: Γ2 -> + {{Δ ⊢ (# (length Γ1)) [σ] ≈ # (length Δ - length Γ2 - 1) : ~(iter (S (length Γ1)) (fun T => {{{T [ Wk ]}}}) T) [ σ ] }}. +Proof. + induction 1; intros; subst; gen_presups. + - pose proof (app_ctx_vlookup _ _ _ _ HΔ eq_refl). + gen_presup H0. + clear_dups. + apply wf_sub_id_inversion in Hτ. + pose proof (wf_ctx_sub_length _ _ Hτ). + transitivity {{{#(length Γ1) [Id]}}}; [mauto 3 |]. + rewrite H1, var_arith, H. + bulky_rewrite. mauto 3. + - pose proof (app_ctx_vlookup _ _ _ _ HΔ0 eq_refl). + pose proof (app_ctx_lookup Γ1 T0 Γ2 _ eq_refl). + gen_presup H2. + clear_dups. + assert {{ Δ', T ⊢s Wk : ~ (Γ1 ++ {{{ Γ2, T0 }}}) }} by mauto. + transitivity {{{#(length Γ1) [Wk ∘ τ]}}}; [mauto 3 |]. + rewrite H1. + etransitivity; [eapply wf_exp_eq_sub_compose; mauto 3 |]. + pose proof (wf_ctx_sub_length _ _ H0). + + rewrite <- exp_eq_sub_compose_typ; mauto 2. + deepexec wf_ctx_sub_ctx_lookup ltac:(fun H => destruct H as [? [? [? [? [-> [? [-> []]]]]]]]). + repeat rewrite List.app_length in *. + rewrite H6 in *. + assert (length x1 = length Γ2) by (simpl in *; lia). + rewrite <- H9. + + etransitivity. + + eapply wf_exp_eq_sub_cong; [ |mauto 3]. + eapply wf_exp_eq_subtyp. + * eapply wf_exp_eq_var_weaken; [mauto 3|]; eauto. + * mauto 4. + + eapply wf_exp_eq_subtyp. + * eapply IHweakening with (Γ1 := T :: _). + reflexivity. + * eapply wf_subtyping_subst; [ |mauto 3]. + simpl. eapply wf_subtyping_subst; mauto 3. +Qed. + +Lemma var_glu_elem_bot : forall A i P El Γ T, + {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} -> + {{ Γ ⊢ T ® P }} -> + {{ Γ, T ⊢ #0 : T[Wk] ® ! (length Γ) ∈ glu_elem_bot i A }}. +Proof. + intros. saturate_glu_info. + econstructor; mauto 4. + - admit. + - intros. progressive_inversion. + exact (var_weaken_gen _ _ _ H2 nil _ _ eq_refl). +Admitted. + +#[local] + Hint Rewrite -> wf_sub_eq_extend_compose using mauto 4 : mcltt. + +Theorem realize_glu_univ_elem_gen : forall A i P El, + {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} -> + (forall Γ T R, {{ DF A ≈ A ∈ per_univ_elem i ↘ R }} -> + {{ Γ ⊢ T ® P }} -> + {{ Γ ⊢ T ® glu_typ_top i A }}) /\ + (forall Γ t T c, {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} -> + {{ Γ ⊢ t : T ® c ∈ glu_elem_bot i A }} -> + {{ Γ ⊢ t : T ® ⇑ A c ∈ El }}) /\ + (forall Γ t T a R, {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} -> + {{ Γ ⊢ t : T ® a ∈ El }} -> + {{ DF A ≈ A ∈ per_univ_elem i ↘ R }} -> + {{ Dom a ≈ a ∈ R }} -> + {{ Γ ⊢ t : T ® a ∈ glu_elem_top i A }}). +Proof. + simpl. induction 1 using glu_univ_elem_ind. + all:split; [| split]; intros; + apply_equiv_left; + gen_presups; + try match_by_head1 per_univ_elem ltac:(fun H => pose proof (per_univ_then_per_top_typ H)); + match_by_head glu_elem_bot ltac:(fun H => destruct H as []); + destruct_all. + - econstructor; eauto; intros. + progressive_inversion. + transitivity {{{Type@j [ σ ]}}}; mauto 4. + - handle_functional_glu_univ_elem. + match_by_head glu_univ_elem invert_glu_univ_elem. + clear_dups. + apply_equiv_left. + repeat split; eauto. + repeat eexists. + + glu_univ_elem_econstructor; eauto; reflexivity. + + simpl. repeat split. + * rewrite <- H5. trivial. + * intros. + saturate_weakening_escape. + rewrite <- wf_exp_eq_typ_sub; try eassumption. + rewrite <- H5. + firstorder. + - deepexec glu_univ_elem_per_univ ltac:(fun H => pose proof H). + firstorder. + specialize (H _ _ _ H10) as [? []]. + econstructor; eauto. + + apply_equiv_left. trivial. + + mauto 2. + + intros. + saturate_weakening_escape. + deepexec H ltac:(fun H => destruct H). + progressive_invert H16. + deepexec H20 ltac:(fun H => pose proof H). + functional_read_rewrite_clear. + bulky_rewrite. + + - econstructor; eauto; intros. + progressive_inversion. + transitivity {{{ℕ [ σ ]}}}; mauto 3. + - handle_functional_glu_univ_elem. + match_by_head glu_univ_elem invert_glu_univ_elem. + apply_equiv_left. + repeat split; eauto. + econstructor; trivial. + + intros. + saturate_weakening_escape. + assert {{ Δ ⊢ T [σ] ≈ ℕ[σ] : Type @ i }} by mauto 3. + rewrite <- wf_exp_eq_nat_sub; try eassumption. + rewrite <- H10. firstorder. + - econstructor; eauto. + + rewrite H2. mauto 3. + + apply_equiv_left. trivial. + + mauto 2. + + intros. + saturate_weakening_escape. + bulky_rewrite. + mauto using glu_nat_readback. + + - match_by_head pi_glu_typ_pred progressive_invert. + handle_per_univ_elem_irrel. + invert_per_univ_elem H6. + econstructor; eauto; intros. + + gen_presups. trivial. + + saturate_weakening_escape. + assert {{ Γ ⊢w Id : Γ }} by mauto 4. + pose proof (H13 _ _ H16). + specialize (H13 _ _ H19). + assert {{ Γ ⊢ IT[Id] ≈ IT : Type@i}} by mauto 3. + bulky_rewrite_in H13. + progressive_invert H17. + destruct (H9 _ _ _ H0 H13) as []. + bulky_rewrite. + simpl. apply wf_exp_eq_pi_cong'; [firstorder |]. + pose proof (var_per_elem (length Δ) H0). + destruct_rel_mod_eval. + simplify_evals. + destruct (H2 _ ltac:(eassumption) _ ltac:(eassumption)) as [? []]. + specialize (H10 _ _ _ _ ltac:(trivial) (var_glu_elem_bot _ _ _ _ _ _ ltac:(eassumption) ltac:(eassumption))). + autorewrite with mcltt in H10. + specialize (H14 {{{Δ, IT[σ]}}} {{{σ ∘ Wk}}} _ _ ltac:(mauto) ltac:(eassumption) ltac:(eassumption)). + specialize (H8 _ _ _ ltac:(eassumption) ltac:(eassumption)) as []. + etransitivity; [| eapply H30]; mauto 3. + - handle_functional_glu_univ_elem. + apply_equiv_left. + invert_glu_rel1. + econstructor; try eapply per_bot_then_per_elem; eauto. + + intros. + saturate_weakening_escape. + saturate_glu_info. + match_by_head1 per_univ_elem invert_per_univ_elem. + destruct_rel_mod_eval. + simplify_evals. + eexists; repeat split; mauto 3. + eapply H2; eauto. + assert {{ Δ ⊢ t [σ] : M[σ] }} by mauto 3. + bulky_rewrite_in H24. + unshelve (econstructor; eauto). + + trivial. + + eassert {{ Δ ⊢ ~ (a_sub t σ) m' : ~_ }} by (eapply wf_app'; eassumption). + autorewrite with mcltt in H26. + trivial. + + mauto using domain_app_per. + + intros. + saturate_weakening_escape. + progressive_invert H27. + destruct (H15 _ _ _ _ _ ltac:(eassumption) ltac:(eassumption) ltac:(eassumption) equiv_b). + handle_functional_glu_univ_elem. + autorewrite with mcltt. + + etransitivity. + * rewrite sub_decompose_q_typ; mauto 4. + * simpl. + rewrite <- sub_eq_q_sigma_id_extend; mauto 4. + rewrite <- exp_eq_sub_compose_typ; mauto 3; + [eapply wf_exp_eq_app_cong' |]. + -- specialize (H12 _ {{{σ ∘ σ0}}} _ ltac:(mauto 3) ltac:(eassumption)). + rewrite wf_exp_eq_sub_compose with (M := t) in H12; mauto 3. + bulky_rewrite_in H12. + -- rewrite <- exp_eq_sub_compose_typ; mauto 3. + -- econstructor; mauto 3. + autorewrite with mcltt. + rewrite <- exp_eq_sub_compose_typ; mauto 3. + + - handle_functional_glu_univ_elem. + handle_per_univ_elem_irrel. + pose proof H8. + invert_per_univ_elem H8. + econstructor; mauto 3. + + invert_glu_rel1. trivial. + + eapply glu_univ_elem_trm_typ; eauto. + + intros. + saturate_weakening_escape. + invert_glu_rel1. clear_dups. + progressive_invert H20. + + assert {{ Γ ⊢w Id : Γ }} by mauto 4. + pose proof (H10 _ _ H24). + specialize (H10 _ _ H19). + assert {{ Γ ⊢ IT[Id] ≈ IT : Type@i}} by mauto 3. + bulky_rewrite_in H25. + destruct (H11 _ _ _ ltac:(eassumption) ltac:(eassumption)) as []. + specialize (H29 _ _ _ H19 H9). + rewrite H5 in *. + autorewrite with mcltt. + eassert {{ Δ ⊢ m[σ] : ~_ }} by (mauto 2). + autorewrite with mcltt in H30. + rewrite @wf_exp_eq_pi_eta' with (M := {{{m[σ]}}}); [| trivial]. + cbn [nf_to_exp]. + eapply wf_exp_eq_fn_cong'; eauto. + + pose proof (var_per_elem (length Δ) H0). + destruct_rel_mod_eval. + simplify_evals. + destruct (H2 _ ltac:(eassumption) _ ltac:(eassumption)) as [? []]. + specialize (H12 _ _ _ _ ltac:(trivial) (var_glu_elem_bot _ _ _ _ _ _ H H10)). + autorewrite with mcltt in H12. + specialize (H14 {{{Δ, IT[σ]}}} {{{σ ∘ Wk}}} _ _ ltac:(mauto) ltac:(eassumption) ltac:(eassumption)) as [? []]. + apply_equiv_left. + destruct_rel_mod_app. + simplify_evals. + deepexec H1 ltac:(fun H => pose proof H). + specialize (H33 _ _ _ _ _ ltac:(eassumption) ltac:(eassumption) ltac:(eassumption) ltac:(eassumption)) as []. + specialize (H40 _ {{{Id}}} _ ltac:(mauto 3) ltac:(eassumption)). + do 2 (rewrite wf_exp_eq_sub_id in H40; mauto 4). + etransitivity; [|eassumption]. + simpl. + assert {{ Δ, IT[σ] ⊢ # 0 : IT[σ ∘ Wk] }} by (rewrite <- exp_eq_sub_compose_typ; mauto 3). + rewrite <- sub_eq_q_sigma_id_extend; mauto 4. + rewrite <- exp_eq_sub_compose_typ; mauto 2. + 2:eapply sub_q; mauto 4. + 2:gen_presup H41; econstructor; mauto 3. + eapply wf_exp_eq_app_cong'; [| mauto 3]. + symmetry. + rewrite <- wf_exp_eq_pi_sub; mauto 4. + + - econstructor; eauto. + intros. + progressive_inversion. + firstorder. + - handle_functional_glu_univ_elem. + apply_equiv_left. + econstructor; eauto. + - handle_functional_glu_univ_elem. + invert_glu_rel1. + econstructor; eauto. + + invert_glu_rel1. + specialize (H7 (length Γ)) as [? []]. + specialize (H3 (length Γ)) as [? []]. + assert {{ Γ ⊢w Id : Γ }} by mauto. + clear_dups. progressive_inversion. + deepexec H6 ltac:(fun H => pose proof H). + autorewrite with mcltt in H; + gen_presups; mauto 3. + + intros s. destruct (H1 s) as [? []]. + mauto. + + intros. + progressive_inversion. + specialize (H10 (length Δ)) as [? []]. + firstorder. + +Qed. + +Corollary realize_glu_typ_top : forall A i P El, + {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} -> + forall Γ T, + {{ Γ ⊢ T ® P }} -> + {{ Γ ⊢ T ® glu_typ_top i A }}. +Proof. + intros. + pose proof H. + eapply glu_univ_elem_per_univ in H. + simpl in *. destruct_all. + eapply realize_glu_univ_elem_gen; eauto. +Qed. + +Theorem realize_glu_elem_bot : forall A i P El, + {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} -> + forall Γ t T c, + {{ Γ ⊢ t : T ® c ∈ glu_elem_bot i A }} -> + {{ Γ ⊢ t : T ® ⇑ A c ∈ El }}. +Proof. + intros. + eapply realize_glu_univ_elem_gen; eauto. +Qed. + +Theorem realize_glu_elem_top : forall A i P El, + {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} -> + forall Γ t T a, + {{ Γ ⊢ t : T ® a ∈ El }} -> + {{ Γ ⊢ t : T ® a ∈ glu_elem_top i A }}. +Proof. + intros. + pose proof H. + eapply glu_univ_elem_per_univ in H. + simpl in *. destruct_all. + eapply realize_glu_univ_elem_gen; eauto. + eapply glu_univ_elem_per_elem; eauto. +Qed. + +#[export] + Hint Resolve realize_glu_typ_top realize_glu_elem_top : mcltt. diff --git a/theories/Core/Soundness/Weakening/Definition.v b/theories/Core/Soundness/Weakening/Definition.v index 43fd1dc0..2acabf81 100644 --- a/theories/Core/Soundness/Weakening/Definition.v +++ b/theories/Core/Soundness/Weakening/Definition.v @@ -10,7 +10,8 @@ Inductive weakening : ctx -> sub -> ctx -> Prop := `( {{ Γ ⊢s σ ≈ Id : Δ }} -> {{ Γ ⊢w σ : Δ }} ) | wk_p : - `( {{ Γ ⊢w τ : Δ , T }} -> + `( {{ Γ ⊢w τ : Δ', T }} -> + {{ ⊢ Δ' ⊆ Δ }} -> {{ Γ ⊢s σ ≈ Wk ∘ τ : Δ }} -> {{ Γ ⊢w σ : Δ }} ) where "Γ ⊢w σ : Δ" := (weakening Γ σ Δ) (in custom judg) : type_scope. diff --git a/theories/Core/Soundness/Weakening/Lemmas.v b/theories/Core/Soundness/Weakening/Lemmas.v index 7b2864e8..bcdaa1e1 100644 --- a/theories/Core/Soundness/Weakening/Lemmas.v +++ b/theories/Core/Soundness/Weakening/Lemmas.v @@ -1,7 +1,7 @@ From Coq Require Import Program.Equality. From Mcltt Require Import Base LibTactics. -From Mcltt.Core Require Import Syntactic.Corollaries Weakening.Definition. +From Mcltt.Core Require Import Syntactic.Corollaries Syntactic.CtxSub Weakening.Definition. Import Syntax_Notations. Lemma weakening_escape : forall Γ σ Δ, @@ -18,6 +18,17 @@ Qed. #[export] Hint Resolve weakening_escape : mcltt. + +Ltac saturate_weakening_escape1 := + match goal with + | H : {{ ~_ ⊢w ~_ : ~_ }} |- _ => + pose proof (weakening_escape _ _ _ H); + fail_if_dup + end. + +Ltac saturate_weakening_escape := + repeat saturate_weakening_escape1. + Lemma weakening_resp_equiv : forall Γ σ σ' Δ, {{ Γ ⊢w σ : Δ }} -> {{ Γ ⊢s σ ≈ σ' : Δ }} -> @@ -35,24 +46,26 @@ Proof. induction 1; mauto. Qed. +Lemma ctxsub_weakening : forall Γ σ Δ, + {{ Γ ⊢w σ : Δ }} -> + forall Δ', + {{ ⊢ Δ ⊆ Δ' }} -> + {{ Γ ⊢w σ : Δ' }}. +Proof. + induction 1; mauto. +Qed. + Lemma weakening_conv : forall Γ σ Δ, {{ Γ ⊢w σ : Δ }} -> forall Δ', {{ ⊢ Δ ≈ Δ' }} -> {{ Γ ⊢w σ : Δ' }}. Proof. - induction 1; intros; mauto. - eapply wk_p. - - eapply IHweakening. - apply weakening_escape in H. - gen_presup H. - progressive_invert HΔ. - econstructor; [ | | eapply ctxeq_exp | ..]; mauto. - - mauto. + intros; mauto using ctxsub_weakening. Qed. #[export] -Hint Resolve weakening_conv : mcltt. +Hint Resolve ctxsub_weakening weakening_conv : mcltt. Lemma weakening_compose : forall Γ' σ' Γ'', {{ Γ' ⊢w σ' : Γ'' }} -> @@ -60,16 +73,15 @@ Lemma weakening_compose : forall Γ' σ' Γ'', {{ Γ ⊢w σ : Γ' }} -> {{ Γ ⊢w σ' ∘ σ : Γ'' }}. Proof with mautosolve. -(* induction 1; intros. *) -(* - gen_presup H. *) -(* assert {{ ⊢ Γ ⊆ Δ }} by mauto. *) -(* eapply weakening_resp_equiv; [mauto 2 |]. *) -(* transitivity {{{ Id ∘ σ0 }}}... *) -(* - eapply wk_p; [eauto |]. *) -(* transitivity {{{ Wk ∘ τ ∘ σ0 }}}; mauto 4. *) -(* eapply wf_sub_eq_compose_assoc; revgoals... *) -(* Qed. *) -Admitted. + induction 1; intros. + - gen_presup H. + assert {{ ⊢ Γ ⊆ Δ }} by mauto. + eapply weakening_resp_equiv; [mauto 2 |]. + transitivity {{{ Id ∘ σ0 }}}... + - eapply wk_p; eauto. + transitivity {{{ Wk ∘ τ ∘ σ0 }}}; mauto 4. + eapply wf_sub_eq_compose_assoc; revgoals... +Qed. #[export] Hint Resolve weakening_compose : mcltt. diff --git a/theories/Core/Syntactic/Corollaries.v b/theories/Core/Syntactic/Corollaries.v index 3fe37412..ac11d9f5 100644 --- a/theories/Core/Syntactic/Corollaries.v +++ b/theories/Core/Syntactic/Corollaries.v @@ -1,4 +1,4 @@ -From Coq Require Import Setoid. +From Coq Require Import Setoid Nat. From Mcltt Require Import Base LibTactics CtxSub. From Mcltt.Core Require Export SystemOpt CoreInversions. Import Syntax_Notations. @@ -26,10 +26,105 @@ Qed. #[export] Hint Resolve invert_sub_id : mcltt. -Add Parametric Morphism i Γ Δ t (H : {{ Δ ⊢ t : Type@i }}) : (a_sub t) - with signature wf_sub_eq Γ Δ ==> wf_exp_eq Γ {{{ Type@i }}} as sub_typ_cong1. +Add Parametric Morphism i Γ Δ : a_sub + with signature wf_exp_eq Δ {{{ Type@i }}} ==> wf_sub_eq Γ Δ ==> wf_exp_eq Γ {{{ Type@i }}} as sub_typ_cong. Proof. intros. gen_presups. mauto 4. Qed. + +Add Parametric Morphism Γ1 Γ2 Γ3 : a_compose + with signature wf_sub_eq Γ2 Γ3 ==> wf_sub_eq Γ1 Γ2 ==> wf_sub_eq Γ1 Γ3 as sub_compose_cong. +Proof. mauto. Qed. + +Lemma wf_ctx_sub_length : forall Γ Δ, + {{ ⊢ Γ ⊆ Δ }} -> + length Γ = length Δ. +Proof. induction 1; simpl; auto. Qed. + +Open Scope list_scope. + +Lemma app_ctx_lookup : forall Δ T Γ n, + length Δ = n -> + {{ #n : ~(iter (S n) (fun T => {{{T [ Wk ]}}}) T) ∈ ~(Δ ++ T :: Γ) }}. +Proof. + induction Δ; intros; simpl in *; subst; mauto. +Qed. + +Lemma ctx_lookup_functional : forall n T Γ, + {{ #n : T ∈ Γ }} -> + forall T', + {{ #n : T' ∈ Γ }} -> + T = T'. +Proof. + induction 1; intros; progressive_inversion; eauto. + erewrite IHctx_lookup; eauto. +Qed. + +Lemma app_ctx_vlookup : forall Δ T Γ n, + {{ ⊢ ~(Δ ++ T :: Γ) }} -> + length Δ = n -> + {{ ~(Δ ++ T :: Γ) ⊢ #n : ~(iter (S n) (fun T => {{{T [ Wk ]}}}) T) }}. +Proof. + intros. econstructor; auto using app_ctx_lookup. +Qed. + +Lemma sub_q_eq : forall Δ A i Γ σ σ', + {{ Δ ⊢ A : Type@i }} -> + {{ Γ ⊢s σ ≈ σ' : Δ }} -> + {{ Γ, A[σ] ⊢s q σ ≈ q σ' : Δ, A }}. +Proof. + intros. gen_presup H0. + econstructor; mauto 3. + - econstructor; mauto 4. + - rewrite <- exp_eq_sub_compose_typ; mauto 4. +Qed. +#[export] + Hint Resolve sub_q_eq : mcltt. + +Lemma wf_subtyping_subst_eq : forall Δ A B, + {{ Δ ⊢ A ⊆ B }} -> + forall Γ σ σ', + {{ Γ ⊢s σ ≈ σ' : Δ }} -> + {{ Γ ⊢ A [σ] ⊆ B[σ'] }}. +Proof. + induction 1; intros * Hσσ'; gen_presup Hσσ'. + - econstructor. mauto 4. + - etransitivity; mauto 4. + - autorewrite with mcltt. + mauto 2. + - autorewrite with mcltt. + eapply wf_subtyp_pi'; mauto. +Qed. + + +Lemma wf_subtyping_subst : forall Δ A B, + {{ Δ ⊢ A ⊆ B }} -> + forall Γ σ, + {{ Γ ⊢s σ : Δ }} -> + {{ Γ ⊢ A [σ] ⊆ B[σ] }}. +Proof. + intros; mauto 2 using wf_subtyping_subst_eq. +Qed. +#[export] + Hint Resolve wf_subtyping_subst_eq wf_subtyping_subst : mcltt. + +Lemma sub_decompose_q_typ : forall Γ S T i σ Δ Δ' τ t, + {{Γ, S ⊢ T : Type@i}} -> + {{Δ ⊢s σ : Γ}} -> + {{Δ' ⊢s τ : Δ}} -> + {{Δ' ⊢ t : S [ σ ] [ τ ]}} -> + {{Δ' ⊢ T [ σ ∘ τ ,, t ] ≈ T [ q σ ] [ τ ,, t ] : Type@i}}. +Proof. + intros. gen_presups. + simpl. autorewrite with mcltt. + rewrite wf_sub_eq_extend_compose; mauto 3; + [| mauto + | rewrite <- exp_eq_sub_compose_typ; mauto 4]. + eapply exp_eq_sub_cong_typ2'; [mauto 2 | mauto |]. + eapply wf_sub_eq_extend_cong; eauto. + - rewrite wf_sub_eq_compose_assoc; mauto 3; mauto 4. + rewrite wf_sub_eq_p_extend; eauto; mauto 4. + - rewrite <- exp_eq_sub_compose_typ; mauto 4. +Qed. diff --git a/theories/Core/Syntactic/CtxEq.v b/theories/Core/Syntactic/CtxEq.v index 26de2d49..0105b184 100644 --- a/theories/Core/Syntactic/CtxEq.v +++ b/theories/Core/Syntactic/CtxEq.v @@ -41,8 +41,8 @@ Lemma ctx_eq_trans : forall {Γ0 Γ1 Γ2}, {{ ⊢ Γ0 ≈ Γ1 }} -> {{ ⊢ Γ1 Proof with mautosolve. intros * HΓ01. gen Γ2. - induction HΓ01 as [|Γ0 ? T0 i01 T1]; mauto. - inversion_clear 1 as [|? Γ2' ? i12 T2]. + induction HΓ01 as [|Γ0 ? i01 T0 T1]; mauto. + inversion_clear 1 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. diff --git a/theories/Core/Syntactic/CtxSub.v b/theories/Core/Syntactic/CtxSub.v index f8b19157..f2250e75 100644 --- a/theories/Core/Syntactic/CtxSub.v +++ b/theories/Core/Syntactic/CtxSub.v @@ -49,7 +49,7 @@ Module ctxsub_judg. 2-3: inversion_clear HΓΔ; econstructor; mautosolve 4. - (* ctxsub_exp_eq_helper variable case *) - inversion_clear HΓΔ as [|Δ0 ? C']. + inversion_clear HΓΔ as [|Δ0 ? ? C']. assert (exists D, {{ #x : D ∈ Δ0 }} /\ {{ Δ0 ⊢ D ⊆ B }}) as [D [i0 ?]] by mauto. destruct_conjs. assert {{ ⊢ Δ0, C' }} by mauto. @@ -105,3 +105,10 @@ Qed. #[export] Instance wf_ctx_sub_trans_ins : Transitive wf_ctx_sub. Proof. eauto using wf_ctx_sub_trans. Qed. + + +Add Parametric Morphism : wf_exp + with signature wf_ctx_sub --> eq ==> eq ==> Basics.impl as ctxsub_exp_morphism. +Proof. + cbv. intros. mauto 3. +Qed. diff --git a/theories/Core/Syntactic/Syntax.v b/theories/Core/Syntactic/Syntax.v index d831551e..d2f031e1 100644 --- a/theories/Core/Syntactic/Syntax.v +++ b/theories/Core/Syntactic/Syntax.v @@ -108,6 +108,10 @@ Proof. apply PeanoNat.Nat.eq_dec. Defined. +Definition q σ := a_extend (a_compose σ a_weaken) (a_var 0). +Arguments q σ/. + + #[global] Declare Custom Entry exp. #[global] Declare Custom Entry nf. @@ -137,7 +141,7 @@ Module Syntax_Notations. Infix "∘" := a_compose (in custom exp at level 40) : mcltt_scope. Infix ",," := a_extend (in custom exp at level 50) : mcltt_scope. - Notation "'q' σ" := ({{{ σ ∘ Wk ,, # 0 }}}) (in custom exp at level 30) : mcltt_scope. + Notation "'q' σ" := (q σ) (in custom exp at level 30) : mcltt_scope. Notation "⋅" := nil (in custom exp at level 0) : mcltt_scope. Notation "x , y" := (cons y x) (in custom exp at level 50) : mcltt_scope. diff --git a/theories/Core/Syntactic/System/Definitions.v b/theories/Core/Syntactic/System/Definitions.v index 06e436d7..6b2546fb 100644 --- a/theories/Core/Syntactic/System/Definitions.v +++ b/theories/Core/Syntactic/System/Definitions.v @@ -39,7 +39,7 @@ with wf_ctx_sub : ctx -> ctx -> Prop := {{ ⊢ Γ , A ⊆ Δ , A' }} ) where "⊢ Γ ⊆ Γ'" := (wf_ctx_sub Γ Γ') (in custom judg) : type_scope -with wf_exp : ctx -> exp -> typ -> Prop := +with wf_exp : ctx -> typ -> exp -> Prop := | wf_typ : `( {{ ⊢ Γ }} -> {{ Γ ⊢ Type@i : Type@(S i) }} ) @@ -84,9 +84,9 @@ with wf_exp : ctx -> exp -> typ -> Prop := `( {{ Γ ⊢ M : A }} -> {{ Γ ⊢ A ⊆ A' }} -> {{ Γ ⊢ M : A' }} ) -where "Γ ⊢ M : A" := (wf_exp Γ M A) (in custom judg) : type_scope +where "Γ ⊢ M : A" := (wf_exp Γ A M) (in custom judg) : type_scope -with wf_sub : ctx -> sub -> ctx -> Prop := +with wf_sub : ctx -> ctx -> sub -> Prop := | wf_sub_id : `( {{ ⊢ Γ }} -> {{ Γ ⊢s Id : Γ }} ) @@ -106,7 +106,7 @@ with wf_sub : ctx -> sub -> ctx -> Prop := `( {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Δ ⊆ Δ' }} -> {{ Γ ⊢s σ : Δ' }} ) -where "Γ ⊢s σ : Δ" := (wf_sub Γ σ Δ) (in custom judg) : type_scope +where "Γ ⊢s σ : Δ" := (wf_sub Γ Δ σ) (in custom judg) : type_scope with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop := | wf_exp_eq_typ_sub : @@ -372,7 +372,7 @@ Qed. Add Parametric Morphism i Γ : (wf_exp Γ) - with signature eq ==> wf_exp_eq Γ {{{ Type@i }}} ==> iff as wf_exp_morph. + with signature wf_exp_eq Γ {{{ Type@i }}} ==> eq ==> iff as wf_exp_morph. Proof. intros; split; mauto. Qed. @@ -383,10 +383,55 @@ Proof. intros; split; mauto. Qed. +Add Parametric Morphism Γ T : (wf_exp_eq Γ T) + with signature (wf_exp_eq Γ T) ==> eq ==> iff as wf_exp_eq_morph1. +Proof. + intros; split; mauto. +Qed. + +Add Parametric Morphism Γ T : (wf_exp_eq Γ T) + with signature eq ==> (wf_exp_eq Γ T) ==> iff as wf_exp_eq_morph2. +Proof. + intros; split; mauto. +Qed. + #[export] -Hint Rewrite -> wf_exp_eq_typ_sub wf_exp_eq_nat_sub using eassumption : mcltt. +Hint Rewrite -> wf_exp_eq_typ_sub wf_exp_eq_nat_sub using mauto 3 : mcltt. #[export] Hint Rewrite -> wf_sub_eq_id_compose_right wf_sub_eq_id_compose_left wf_sub_eq_compose_assoc (* prefer right association *) wf_sub_eq_p_extend using mauto 4 : mcltt. + + +#[export] + Hint Rewrite -> wf_exp_eq_sub_id wf_exp_eq_pi_sub using mauto 4 : mcltt. + +#[export] + Instance wf_exp_eq_per_elem Γ T : PERElem _ (wf_exp Γ T) (wf_exp_eq Γ T). +Proof. + intros a Ha. mauto. +Qed. + + +#[export] + Instance wf_sub_eq_per_elem Γ Δ : PERElem _ (wf_sub Γ Δ) (wf_sub_eq Γ Δ). +Proof. + intros a Ha. mauto. +Qed. + + +Add Parametric Morphism Γ j : (wf_subtyping Γ) + with signature eq ==> (wf_exp_eq Γ {{{Type@j}}}) ==> iff as wf_subtyping_resp_exp_eq_morphism1. +Proof. + split; intros; + etransitivity; mauto 3. +Qed. + + +Add Parametric Morphism Γ i : (wf_subtyping Γ) + with signature (wf_exp_eq Γ {{{Type@i}}}) ==> eq ==> iff as wf_subtyping_resp_exp_eq_morphism2. +Proof. + split; intros; + etransitivity; mauto 3. +Qed. diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v index daff4d4e..574cfe2a 100644 --- a/theories/Core/Syntactic/System/Lemmas.v +++ b/theories/Core/Syntactic/System/Lemmas.v @@ -764,17 +764,6 @@ Qed. #[export] Hint Resolve sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : mcltt. -(* Lemma typ_subsumption_wf_ctx : forall {Γ A A'}, *) -(* {{ Γ ⊢ A ⊆ A' }} -> *) -(* {{ ⊢ Γ }}. *) -(* Proof. *) -(* intros * H. *) -(* dependent induction H; mauto. *) -(* Qed. *) - -(* #[export] *) -(* Hint Resolve typ_subsumption_wf_ctx : mcltt. *) - Fact wf_subtyping_refl : forall {Γ A i}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢ A ⊆ A }}. diff --git a/theories/Core/Syntactic/SystemOpt.v b/theories/Core/Syntactic/SystemOpt.v index 2a4a720b..a9d0ba98 100644 --- a/theories/Core/Syntactic/SystemOpt.v +++ b/theories/Core/Syntactic/SystemOpt.v @@ -285,3 +285,19 @@ Qed. Hint Resolve wf_subtyp_pi' : mcltt. #[export] Remove Hints wf_subtyp_pi : mcltt. + + +Lemma wf_exp_eq_nat_sub_gen : forall Γ σ Δ i, + {{ Γ ⊢s σ : Δ }} -> + {{ Γ ⊢ ℕ[σ] ≈ ℕ : Type@i }}. +Proof. + intros. + assert (0 <= i) by lia. + mauto. +Qed. + +#[export] + Hint Resolve wf_exp_eq_nat_sub_gen : mcltt. + +#[export] +Hint Rewrite -> wf_exp_eq_nat_sub_gen using eassumption : mcltt. diff --git a/theories/LibTactics.v b/theories/LibTactics.v index 9a69c5e8..3180d4d3 100644 --- a/theories/LibTactics.v +++ b/theories/LibTactics.v @@ -421,3 +421,32 @@ Instance subrelation_relation_equivalence {A} : subrelation relation_equivalence Proof. intro; intuition. Qed. + +(* The following facility converts search of Proper from type class instances to the local context *) + +Class PERElem (A : Type) (P : A -> Prop) (R : A -> A -> Prop) := + per_elem : forall a, P a -> R a a. + +#[export] + Instance PERProper (A : Type) (P : A -> Prop) (R : A -> A -> Prop) `(Ins : PERElem A P R) a (H : P a) : + Proper R a. +Proof. + cbv. auto using per_elem. +Qed. + + +Ltac bulky_rewrite1 := + match goal with + | H : _ |- _ => rewrite H + | _ => progress (autorewrite with mcltt) + end. + +Ltac bulky_rewrite := repeat (bulky_rewrite1; mauto 2). + +Ltac bulky_rewrite_in1 HT := + match goal with + | H : _ |- _ => tryif unify H HT then fail else rewrite H in HT + | _ => progress (autorewrite with mcltt in HT) + end. + +Ltac bulky_rewrite_in HT := repeat (bulky_rewrite_in1 HT; mauto 2). diff --git a/theories/_CoqProject b/theories/_CoqProject index fefc4416..2ffabbb0 100644 --- a/theories/_CoqProject +++ b/theories/_CoqProject @@ -59,6 +59,7 @@ ./Core/Soundness/Weakening.v ./Core/Soundness/Weakening/Definition.v ./Core/Soundness/Weakening/Lemmas.v +./Core/Soundness/Realizability.v ./Frontend/Elaborator.v ./Frontend/Parser.v ./Frontend/ParserExtraction.v