From 07c74ccddf98c10bba5c2f1de672ffd7a7a2386f Mon Sep 17 00:00:00 2001 From: "Junyoung/\"Clare\" Jang" Date: Thu, 1 Aug 2024 13:27:00 -0400 Subject: [PATCH] Gluing Cumulativity (#150) * Update some others * Prove gluing cumulativity * Replace instances Co-authored-by: Jason Hu * Move extern hints to LibTactics --------- Co-authored-by: Jason Hu --- theories/Core/Semantic/PER/Lemmas.v | 2 +- theories/Core/Soundness/Cumulativity.v | 165 ++++++++++++++++++ .../Soundness/LogicalRelation/Definitions.v | 9 +- .../Core/Soundness/LogicalRelation/Lemmas.v | 69 ++------ theories/Core/Soundness/Realizability.v | 17 +- theories/Core/Syntactic/SystemOpt.v | 72 +++++--- theories/LibTactics.v | 18 +- theories/_CoqProject | 3 +- 8 files changed, 254 insertions(+), 101 deletions(-) create mode 100644 theories/Core/Soundness/Cumulativity.v diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v index b372cb89..5b8583d9 100644 --- a/theories/Core/Semantic/PER/Lemmas.v +++ b/theories/Core/Semantic/PER/Lemmas.v @@ -598,7 +598,7 @@ Proof. Qed. Ltac invert_per_univ_elem H := - (unshelve eapply (per_univ_elem_pi_clean_inversion _) in H; [| eassumption | |]; destruct H as [? []]) + (unshelve eapply (per_univ_elem_pi_clean_inversion _) in H; shelve_unifiable; [eassumption |]; destruct H as [? []]) + basic_invert_per_univ_elem H. Lemma per_univ_elem_cumu : forall i a0 a1 R, diff --git a/theories/Core/Soundness/Cumulativity.v b/theories/Core/Soundness/Cumulativity.v new file mode 100644 index 00000000..3e355f4f --- /dev/null +++ b/theories/Core/Soundness/Cumulativity.v @@ -0,0 +1,165 @@ +From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses. + +From Mcltt Require Import Base LibTactics. +From Mcltt.Core.Syntactic Require Import Corollaries. +From Mcltt.Core.Semantic Require Import Realizability. +From Mcltt.Core.Soundness Require Import Realizability. +From Mcltt.Core.Soundness Require Export LogicalRelation. +Import Domain_Notations. + +Section glu_univ_elem_cumulativity. + #[local] + Lemma glu_univ_elem_cumulativity_ge : forall {i j a P P' El El'}, + i <= j -> + {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> + {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} -> + (forall Γ A, {{ Γ ⊢ A ® P }} -> {{ Γ ⊢ A ® P' }}) /\ + (forall Γ A M m, {{ Γ ⊢ M : A ® m ∈ El }} -> {{ Γ ⊢ M : A ® m ∈ El' }}) /\ + (forall Γ A M m, {{ Γ ⊢ A ® P }} -> {{ Γ ⊢ M : A ® m ∈ El' }} -> {{ Γ ⊢ M : A ® m ∈ El }}). + Proof. + simpl. + intros * Hge Hglu Hglu'. gen El' P' j. + induction Hglu using glu_univ_elem_ind; repeat split; intros; + try assert {{ DF a ≈ a ∈ per_univ_elem j ↘ in_rel }} by mauto; + invert_glu_univ_elem Hglu'; + handle_functional_glu_univ_elem; + simpl in *; + try solve [repeat split; intros; destruct_conjs; mauto 3 | intuition; mauto 4]. + + - rename x into IP'. + rename x0 into IEl'. + rename x1 into OP'. + rename x2 into OEl'. + destruct_by_head pi_glu_typ_pred. + econstructor; intros; mauto 4. + + assert {{ Δ ⊢ IT[σ] ® IP }} by mauto. + assert (forall Γ A, {{ Γ ⊢ A ® IP }} -> {{ Γ ⊢ A ® IP' }}) by (eapply proj1; mauto). + mauto. + + rename a0 into c. + rename equiv_a into equiv_c. + match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H). + apply_relation_equivalence. + destruct_rel_mod_eval. + handle_per_univ_elem_irrel. + assert (forall Γ A, {{ Γ ⊢ A ® OP c equiv_c }} -> {{ Γ ⊢ A ® OP' c equiv_c }}) by (eapply proj1; mauto). + enough {{ Δ ⊢ OT[σ,,m] ® OP c equiv_c }} by mauto. + enough {{ Δ ⊢ m : IT[σ] ® c ∈ IEl }} by mauto. + eapply IHHglu; mauto. + - rename x into IP'. + rename x0 into IEl'. + rename x1 into OP'. + rename x2 into OEl'. + destruct_by_head pi_glu_exp_pred. + handle_per_univ_elem_irrel. + econstructor; intros; mauto 4. + + assert (forall Γ A, {{ Γ ⊢ A ® IP }} -> {{ Γ ⊢ A ® IP' }}) by (eapply proj1; mauto). + mauto. + + rename b into c. + rename equiv_b into equiv_c. + match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H). + handle_per_univ_elem_irrel. + destruct_rel_mod_eval. + destruct_rel_mod_app. + handle_per_univ_elem_irrel. + eexists; split; mauto. + assert (forall Γ A M m, {{ Γ ⊢ M : A ® m ∈ OEl c equiv_c }} -> {{ Γ ⊢ M : A ® m ∈ OEl' c equiv_c }}) by (eapply proj1, proj2; mauto). + enough {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® fa ∈ OEl c equiv_c }} by mauto. + assert {{ Δ ⊢ m' : IT[σ] ® c ∈ IEl }} by (eapply IHHglu; mauto). + assert (exists ac, {{ $| a0 & c |↘ ac }} /\ {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® ac ∈ OEl c equiv_c }}) by mauto. + destruct_conjs. + functional_eval_rewrite_clear. + mauto. + - rename x into IP'. + rename x0 into IEl'. + rename x1 into OP'. + rename x2 into OEl'. + destruct_by_head pi_glu_typ_pred. + destruct_by_head pi_glu_exp_pred. + handle_per_univ_elem_irrel. + econstructor; intros; mauto. + rename b into c. + rename equiv_b into equiv_c. + match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H). + handle_per_univ_elem_irrel. + destruct_rel_mod_eval. + destruct_rel_mod_app. + handle_per_univ_elem_irrel. + rename a1 into b. + eexists; split; mauto. + assert (forall Γ A M m, {{ Γ ⊢ A ® OP c equiv_c }} -> {{ Γ ⊢ M : A ® m ∈ OEl' c equiv_c }} -> {{ Γ ⊢ M : A ® m ∈ OEl c equiv_c }}) by (eapply proj2, proj2; eauto 3). + assert {{ Δ ⊢ OT[σ,,m'] ® OP c equiv_c }} by mauto. + enough {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® fa ∈ OEl' c equiv_c }} by mauto. + assert {{ Δ ⊢ m' : IT[σ] ® c ∈ IEl' }} by (eapply IHHglu; mauto). + assert {{ Δ ⊢ IT[σ] ≈ IT0[σ] : Type@j }} as HITeq. + { + assert {{ Δ ⊢ IT[σ] ® glu_typ_top i a }} as [] by mauto 3. + assert {{ Δ ⊢ IT0[σ] ® glu_typ_top j a }} as [] by mauto 3. + match_by_head per_top_typ ltac:(fun H => destruct (H (length Δ)) as [? []]). + clear_dups. + functional_read_rewrite_clear. + assert {{ Δ ⊢ IT[σ][Id] ≈ x1 : Type@i }} by mauto 4. + assert {{ Δ ⊢ IT[σ] ≈ x1 : Type@i }} by mauto 4. + assert {{ Δ ⊢ IT[σ] ≈ x1 : Type@j }} by mauto 4. + assert {{ Δ ⊢ IT0[σ][Id] ≈ x1 : Type@j }} by mauto 4. + enough {{ Δ ⊢ IT0[σ] ≈ x1 : Type@j }}; mautosolve 4. + } + assert {{ Δ ⊢ m' : IT0[σ] ® c ∈ IEl' }} by (rewrite <- HITeq; mauto). + assert (exists ac, {{ $| a0 & c |↘ ac }} /\ {{ Δ ⊢ m[σ] m' : OT0[σ,,m'] ® ac ∈ OEl' c equiv_c }}) by mauto. + destruct_conjs. + functional_eval_rewrite_clear. + enough {{ Δ ⊢ OT[σ,,m'] ≈ OT0[σ,,m'] : Type@j }} by (rewrite glu_univ_elem_elem_morphism_iff1; mauto). + assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv_c ↘ OEl c equiv_c }} by mauto. + assert {{ DG b ∈ glu_univ_elem j ↘ OP' c equiv_c ↘ OEl' c equiv_c }} by mauto. + assert {{ Δ ⊢ OT0[σ,,m'] ® OP' c equiv_c }} by (eapply glu_univ_elem_trm_typ; mauto). + assert {{ Δ ⊢ OT[σ,,m'] ® glu_typ_top i b }} as [] by mauto 3. + assert {{ Δ ⊢ OT0[σ,,m'] ® glu_typ_top j b }} as [] by mauto 3. + match_by_head per_top_typ ltac:(fun H => destruct (H (length Δ)) as [? []]). + clear_dups. + functional_read_rewrite_clear. + assert {{ Δ ⊢ OT[σ,,m'][Id] ≈ x1 : Type@i }} by mauto 4. + assert {{ Δ ⊢ OT[σ,,m'] ≈ x1 : Type@i }} by mauto 4. + assert {{ Δ ⊢ OT[σ,,m'] ≈ x1 : Type@j }} by mauto 4. + assert {{ Δ ⊢ OT0[σ,,m'][Id] ≈ x1 : Type@j }} by mauto 4. + enough {{ Δ ⊢ OT0[σ,,m'] ≈ x1 : Type@j }}; mautosolve 4. + - destruct_by_head neut_glu_exp_pred. + econstructor; mauto. + destruct_by_head neut_glu_typ_pred. + econstructor; mauto. + - destruct_by_head neut_glu_exp_pred. + econstructor; mauto. + Qed. +End glu_univ_elem_cumulativity. + +Corollary glu_univ_elem_typ_cumu_ge : forall {i j a P P' El El' Γ A}, + i <= j -> + {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> + {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} -> + {{ Γ ⊢ A ® P }} -> + {{ Γ ⊢ A ® P' }}. +Proof. + intros. + eapply glu_univ_elem_cumulativity_ge; mauto. +Qed. + +Corollary glu_univ_elem_exp_cumu_ge : forall {i j a P P' El El' Γ A M m}, + i <= j -> + {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> + {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} -> + {{ Γ ⊢ M : A ® m ∈ El }} -> + {{ Γ ⊢ M : A ® m ∈ El' }}. +Proof. + intros * ? ? ?. gen m M A Γ. + eapply glu_univ_elem_cumulativity_ge; mauto. +Qed. + +Corollary glu_univ_elem_exp_lower : forall {i j a P P' El El' Γ A M m}, + i <= j -> + {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> + {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} -> + {{ Γ ⊢ A ® P }} -> + {{ Γ ⊢ M : A ® m ∈ El' }} -> + {{ Γ ⊢ M : A ® m ∈ El }}. +Proof. + intros * ? ? ?. gen m M A Γ. + eapply glu_univ_elem_cumulativity_ge; mauto. +Qed. diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v index be77e16e..91e7cef4 100644 --- a/theories/Core/Soundness/LogicalRelation/Definitions.v +++ b/theories/Core/Soundness/LogicalRelation/Definitions.v @@ -14,7 +14,7 @@ Notation "'glu_typ_pred_args'" := (Tcons ctx (Tcons typ Tnil)). Notation "'glu_typ_pred'" := (predicate glu_typ_pred_args). Notation "'glu_typ_pred_equivalence'" := (@predicate_equivalence glu_typ_pred_args) (only parsing). (* 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 "Γ ⊢ A ® R" := ((R Γ A : (Prop : Type)) : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, A custom exp, R constr). Notation "'glu_exp_pred_args'" := (Tcons ctx (Tcons typ (Tcons exp (Tcons domain Tnil)))). Notation "'glu_exp_pred'" := (predicate glu_exp_pred_args). @@ -24,10 +24,10 @@ Notation "Γ ⊢ M : A ® m ∈ R" := (R Γ A M m : (Prop : (Type : Type))) (in Notation "'glu_sub_pred_args'" := (Tcons ctx (Tcons sub (Tcons env Tnil))). Notation "'glu_sub_pred'" := (predicate glu_sub_pred_args). Notation "'glu_sub_pred_equivalence'" := (@predicate_equivalence glu_sub_pred_args) (only parsing). -Notation "Γ ⊢s σ ® ρ ∈ R" := (R Γ σ ρ : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, σ custom exp, ρ custom domain, R constr). +Notation "Γ ⊢s σ ® ρ ∈ R" := ((R Γ σ ρ : Prop) : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, σ custom exp, ρ custom domain, R constr). -Notation "'DG' a ∈ R ↘ P ↘ El" := (R P El a : (Prop : (Type : Type))) (in custom judg at level 90, a custom domain, R constr, P constr, El constr). -Notation "'EG' A ∈ R ↘ Sb " := (R Sb A : (Prop : (Type : Type))) (in custom judg at level 90, A custom exp, R constr, Sb constr). +Notation "'DG' a ∈ R ↘ P ↘ El" := (R P El a : ((Prop : Type) : (Type : Type))) (in custom judg at level 90, a custom domain, R constr, P constr, El constr). +Notation "'EG' A ∈ R ↘ Sb " := (R Sb A : ((Prop : (Type : Type)) : (Type : Type))) (in custom judg at level 90, A custom exp, R constr, Sb constr). Inductive glu_nat : ctx -> exp -> domain -> Prop := | glu_nat_zero : @@ -109,6 +109,7 @@ Hint Constructors neut_glu_exp_pred pi_glu_typ_pred pi_glu_exp_pred : mcltt. Definition univ_glu_typ_pred j i : glu_typ_pred := fun Γ T => {{ Γ ⊢ T ≈ Type@j : Type@i }}. Arguments univ_glu_typ_pred j i Γ T/. +Transparent univ_glu_typ_pred. Section Gluing. Variable diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v index 1b7a333c..f1210025 100644 --- a/theories/Core/Soundness/LogicalRelation/Lemmas.v +++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v @@ -489,28 +489,28 @@ Ltac handle_functional_glu_univ_elem := apply_predicate_equivalence; clear_dups. -Lemma glu_univ_elem_pi_clean_inversion : forall {i a p B in_rel elem_rel typ_rel el_rel}, +Lemma glu_univ_elem_pi_clean_inversion : forall {i a p B in_rel typ_rel el_rel}, {{ DF a ≈ a ∈ per_univ_elem i ↘ in_rel }} -> - {{ DF Π a p B ≈ Π a p B ∈ per_univ_elem i ↘ elem_rel }} -> {{ DG Π a p B ∈ glu_univ_elem i ↘ typ_rel ↘ el_rel }} -> exists IP IEl (OP : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_typ_pred) - (OEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_exp_pred), + (OEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_exp_pred) elem_rel, {{ DG a ∈ glu_univ_elem i ↘ IP ↘ IEl }} /\ (forall c (equiv_c : {{ Dom c ≈ c ∈ in_rel }}) b, {{ ⟦ B ⟧ p ↦ c ↘ b }} -> {{ DG b ∈ glu_univ_elem i ↘ OP _ equiv_c ↘ OEl _ equiv_c }}) /\ + {{ DF Π a p B ≈ Π a p B ∈ per_univ_elem i ↘ elem_rel }} /\ (typ_rel <∙> pi_glu_typ_pred i in_rel IP IEl OP) /\ (el_rel <∙> pi_glu_exp_pred i in_rel IP IEl elem_rel OEl). Proof. intros *. simpl. - intros Hinper Hper Hglu. + intros Hinper Hglu. basic_invert_glu_univ_elem Hglu. handle_functional_glu_univ_elem. handle_per_univ_elem_irrel. - do 4 eexists. + do 5 eexists. repeat split. - 1: eassumption. + 1,3: eassumption. 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 }} -> @@ -563,9 +563,11 @@ Proof. intuition. Qed. +Arguments glu_univ_elem_pi_clean_inversion _ _ _ _ _ _ _ _ _ &. + Ltac invert_glu_univ_elem H := - (unshelve eapply (glu_univ_elem_pi_clean_inversion _ _) in H; [eassumption | eassumption | | |]; - destruct H as [? [? [? [? [? [? []]]]]]]) + (unshelve eapply (glu_univ_elem_pi_clean_inversion _) in H; shelve_unifiable; [eassumption |]; + destruct H as [? [? [? [? [? [? [? [? []]]]]]]]]) + basic_invert_glu_univ_elem H. Lemma glu_univ_elem_morphism_helper : forall i a a' P El, @@ -587,6 +589,7 @@ Proof. destruct_rel_mod_eval. handle_per_univ_elem_irrel. intuition. + - reflexivity. - apply neut_glu_typ_pred_morphism_glu_typ_pred_equivalence. eassumption. - apply neut_glu_exp_pred_morphism_glu_exp_pred_equivalence. @@ -665,39 +668,8 @@ 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 -> - {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> - exists P' El', {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }}. -Proof. - simpl. - intros * Hge Hglu. gen j. - induction Hglu using glu_univ_elem_ind; intros; - handle_functional_glu_univ_elem; try solve [do 2 eexists; glu_univ_elem_econstructor; try (reflexivity + lia); mauto]. - - edestruct IHHglu; [eassumption |]. - destruct_conjs. - do 2 eexists. - glu_univ_elem_econstructor; try reflexivity; mauto. - 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 }}). - instantiate (1 := fun c equiv_c Γ A => forall b Pb Elb, - {{ ⟦ B ⟧ p ↦ c ↘ b }} -> - glu_univ_elem j Pb Elb b -> - {{ Γ ⊢ A ® Pb }}). - intros. - assert (exists (P' : ctx -> typ -> Prop) (El' : ctx -> typ -> typ -> domain -> Prop), glu_univ_elem j P' El' b) as [] by mauto. - destruct_conjs. - rewrite simple_glu_univ_elem_morphism_iff; try (eassumption + reflexivity); - split; intros; handle_functional_glu_univ_elem; intuition. -Qed. - #[local] - Hint Rewrite -> sub_decompose_q using solve [mauto 4] : mcltt. - +Hint Rewrite -> sub_decompose_q using solve [mauto 4] : mcltt. Lemma glu_univ_elem_typ_monotone : forall i a P El, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> @@ -709,7 +681,7 @@ Proof. simpl. induction 1 using glu_univ_elem_ind; intros; saturate_weakening_escape; handle_functional_glu_univ_elem; - apply_equiv_left; + simpl in *; try solve [bulky_rewrite]. - simpl_glu_rel. econstructor; eauto; try solve [bulky_rewrite]; mauto 3. intros. @@ -719,12 +691,8 @@ Proof. destruct_rel_mod_eval. simplify_evals. deepexec H1 ltac:(fun H => pose proof H). - autorewrite with mcltt in H15. - autorewrite with mcltt in H17. - autorewrite with mcltt. - + eapply H11; mauto 2. - + econstructor; mauto 2. - bulky_rewrite. + autorewrite with mcltt in *. + mauto 3. - destruct_conjs. split; [mauto 3 |]. @@ -745,7 +713,7 @@ Proof. simpl. induction 1 using glu_univ_elem_ind; intros; saturate_weakening_escape; handle_functional_glu_univ_elem; - apply_equiv_left; + simpl in *; destruct_all. - repeat eexists; mauto 2; bulky_rewrite. eapply glu_univ_elem_typ_monotone; eauto. @@ -763,8 +731,7 @@ Proof. destruct_rel_mod_app. simplify_evals. deepexec H1 ltac:(fun H => pose proof H). - autorewrite with mcltt in H17. - autorewrite with mcltt in H19. + autorewrite with mcltt in *. repeat eexists; eauto. assert {{ Δ0 ⊢s σ0,, m' : Δ, ~ (a_sub IT σ) }}. { econstructor; mauto 2. @@ -781,7 +748,7 @@ Proof. } bulky_rewrite. - edestruct H13 with (b := b) as [? []]; + edestruct H10 with (b := b) as [? []]; simplify_evals; [| | eassumption]; mauto. diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v index 592940dd..2e8d30e7 100644 --- a/theories/Core/Soundness/Realizability.v +++ b/theories/Core/Soundness/Realizability.v @@ -1,9 +1,8 @@ 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.Syntactic Require Import CtxSub Corollaries. +From Mcltt.Core.Semantic Require Import Realizability. From Mcltt.Core.Soundness Require Export LogicalRelation Weakening. Import Domain_Notations. @@ -95,7 +94,7 @@ Proof. Qed. #[local] - Hint Rewrite -> wf_sub_eq_extend_compose using mauto 4 : mcltt. +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 }} -> @@ -162,7 +161,7 @@ Proof. saturate_weakening_escape. assert {{ Δ ⊢ T [σ] ≈ ℕ[σ] : Type @ i }} by mauto 3. rewrite <- wf_exp_eq_nat_sub; try eassumption. - rewrite <- H10. firstorder. + mauto 3. - econstructor; eauto. + rewrite H2. mauto 3. + apply_equiv_left. trivial. @@ -210,16 +209,16 @@ Proof. eexists; repeat split; mauto 3. eapply H2; eauto. assert {{ Δ ⊢ t [σ] : M[σ] }} by mauto 3. - bulky_rewrite_in H24. + bulky_rewrite_in H23. unshelve (econstructor; eauto). + trivial. + eassert {{ Δ ⊢ ~ (a_sub t σ) m' : ~_ }} by (eapply wf_app'; eassumption). - autorewrite with mcltt in H26. + autorewrite with mcltt in H25. trivial. + mauto using domain_app_per. + intros. saturate_weakening_escape. - progressive_invert H27. + progressive_invert H26. destruct (H15 _ _ _ _ _ ltac:(eassumption) ltac:(eassumption) ltac:(eassumption) equiv_b). handle_functional_glu_univ_elem. autorewrite with mcltt. @@ -347,4 +346,4 @@ Proof. Qed. #[export] - Hint Resolve realize_glu_typ_top realize_glu_elem_top : mcltt. +Hint Resolve realize_glu_typ_top realize_glu_elem_top : mcltt. diff --git a/theories/Core/Syntactic/SystemOpt.v b/theories/Core/Syntactic/SystemOpt.v index c93a52eb..5f49fc6d 100644 --- a/theories/Core/Syntactic/SystemOpt.v +++ b/theories/Core/Syntactic/SystemOpt.v @@ -22,6 +22,20 @@ Hint Resolve wf_ctx_eq_extend' : mcltt. #[export] Remove Hints wf_ctx_eq_extend : mcltt. +Corollary wf_nat' : forall {Γ i}, + {{ ⊢ Γ }} -> + {{ Γ ⊢ ℕ : Type@i }}. +Proof. + intros. + assert (0 <= i) by lia. + mauto. +Qed. + +#[export] +Hint Resolve wf_nat' : mcltt. +#[export] +Remove Hints wf_nat : mcltt. + Corollary wf_natrec' : forall {Γ A MZ MS M}, {{ Γ ⊢ MZ : A[Id,,zero] }} -> {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} -> @@ -78,6 +92,35 @@ Hint Resolve wf_app' : mcltt. #[export] Remove Hints wf_app : mcltt. +Lemma wf_exp_eq_typ_sub' : forall Γ σ Δ i j, + {{ Γ ⊢s σ : Δ }} -> + i < j -> + {{ Γ ⊢ Type@i[σ] ≈ Type@i : Type@j }}. +Proof. mauto 3. Qed. + +#[export] +Hint Resolve wf_exp_eq_typ_sub' : mcltt. + +#[export] +Hint Rewrite -> wf_exp_eq_typ_sub' using solve [lia | mauto 3] : mcltt. + +Corollary wf_exp_eq_nat_sub' : forall Γ σ Δ i, + {{ Γ ⊢s σ : Δ }} -> + {{ Γ ⊢ ℕ[σ] ≈ ℕ : Type@i }}. +Proof. + intros. + assert (0 <= i) by lia. + mauto. +Qed. + +#[export] +Hint Resolve wf_exp_eq_nat_sub' : mcltt. +#[export] +Remove Hints wf_exp_eq_nat_sub : mcltt. + +#[export] +Hint Rewrite -> wf_exp_eq_nat_sub' using mautosolve 3 : mcltt. + Corollary wf_exp_eq_natrec_cong' : forall {Γ A A' i MZ MZ' MS MS' M M'}, {{ Γ , ℕ ⊢ A ≈ A' : Type@i }} -> {{ Γ ⊢ MZ ≈ MZ' : A[Id,,zero] }} -> @@ -285,32 +328,3 @@ 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 solve [mauto 3] : mcltt. - - -Lemma wf_exp_eq_typ_sub' : forall Γ σ Δ i j, - {{ Γ ⊢s σ : Δ }} -> - i < j -> - {{ Γ ⊢ Type@i[σ] ≈ Type@i : Type@j }}. -Proof. mauto 3. Qed. - -#[export] - Hint Resolve wf_exp_eq_typ_sub' : mcltt. - -#[export] -Hint Rewrite -> wf_exp_eq_typ_sub' using solve [lia | mauto 3] : mcltt. diff --git a/theories/LibTactics.v b/theories/LibTactics.v index 3180d4d3..1075ddc0 100644 --- a/theories/LibTactics.v +++ b/theories/LibTactics.v @@ -410,18 +410,24 @@ Qed. solve [reflexivity || apply Equivalence_Reflexive]. (* Helper Instances for Generalized Rewriting *) +#[export] +Hint Extern 1 (subrelation (@predicate_equivalence ?Ts) _) => (let H := fresh "H" in intros ? ? H; exact H) : typeclass_instances. + +#[export] +Hint Extern 1 (subrelation iff Basics.impl) => exact iff_impl_subrelation : typeclass_instances. + +#[export] +Hint Extern 1 (subrelation iff (Basics.flip Basics.impl)) => exact iff_flip_impl_subrelation : typeclass_instances. + +#[export] +Hint Extern 1 (subrelation (@relation_equivalence ?A) _) => (let H := fresh "H" in intros ? ? H; exact H) : typeclass_instances. + Add Parametric Morphism A : PER with signature (@relation_equivalence A) ==> iff as PER_morphism. Proof. split; intros []; econstructor; unfold Symmetric, Transitive in *; intuition. Qed. -#[export] -Instance subrelation_relation_equivalence {A} : subrelation relation_equivalence (pointwise_relation A (pointwise_relation A iff)). -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) := diff --git a/theories/_CoqProject b/theories/_CoqProject index 2ffabbb0..01953116 100644 --- a/theories/_CoqProject +++ b/theories/_CoqProject @@ -52,14 +52,15 @@ ./Core/Syntactic/System/Tactics.v ./Core/Syntactic/SystemOpt.v ./Core/Soundness.v +./Core/Soundness/Cumulativity.v ./Core/Soundness/LogicalRelation.v ./Core/Soundness/LogicalRelation/CoreTactics.v ./Core/Soundness/LogicalRelation/Definitions.v ./Core/Soundness/LogicalRelation/Lemmas.v +./Core/Soundness/Realizability.v ./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