From 80cfb658f05b103a69ea53c7258c04f3ca193b12 Mon Sep 17 00:00:00 2001 From: Jason Hu Date: Tue, 2 Jul 2024 21:15:00 -0400 Subject: [PATCH] subtyping in the PER model (#128) * subtyping in the PER model * prove cumulativity * add subtyping between contexts * subtyping lemma for contexts * prove transitivity of context subtyping * empty --- theories/Core/Semantic/PER/CoreTactics.v | 4 +- theories/Core/Semantic/PER/Definitions.v | 51 +++++ theories/Core/Semantic/PER/Lemmas.v | 275 +++++++++++++++++++++++ theories/LibTactics.v | 28 ++- 4 files changed, 345 insertions(+), 13 deletions(-) diff --git a/theories/Core/Semantic/PER/CoreTactics.v b/theories/Core/Semantic/PER/CoreTactics.v index 506b4a5a..597b40c6 100644 --- a/theories/Core/Semantic/PER/CoreTactics.v +++ b/theories/Core/Semantic/PER/CoreTactics.v @@ -45,12 +45,12 @@ Ltac destruct_rel_typ := (** Universe/Element PER Helper Tactics *) Ltac basic_invert_per_univ_elem H := - simp per_univ_elem in H; + progress simp per_univ_elem in H; inversion H; subst; try rewrite <- per_univ_elem_equation_1 in *. Ltac basic_per_univ_elem_econstructor := - simp per_univ_elem; + progress simp per_univ_elem; econstructor; try rewrite <- per_univ_elem_equation_1 in *. diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v index a26e915d..525e395b 100644 --- a/theories/Core/Semantic/PER/Definitions.v +++ b/theories/Core/Semantic/PER/Definitions.v @@ -227,6 +227,34 @@ Section Per_univ_elem_ind_def. | i, a, b, R, H := per_univ_elem_ind' i a b R _. End Per_univ_elem_ind_def. +Reserved Notation "'Sub' a <: b 'at' i" (in custom judg at level 90, a custom domain, b custom domain, i constr). + +Inductive per_subtyp : nat -> domain -> domain -> Prop := +| per_subtyp_neut : + `( {{ Dom b ≈ b' ∈ per_bot }} -> + {{ Sub ⇑ a b <: ⇑ a' b' at i }} ) +| per_subtyp_nat : + `( {{ Sub ℕ <: ℕ at i }} ) +| per_subtyp_univ : + `( i <= j -> + j < k -> + {{ Sub 𝕌@i <: 𝕌@j at k }} ) +| per_subtyp_pi : + `( forall (in_rel : relation domain) elem_rel elem_rel', + {{ DF a ≈ a' ∈ per_univ_elem i ↘ in_rel }} -> + (forall c c' b b', + {{ Dom c ≈ c' ∈ in_rel }} -> + {{ ⟦ B ⟧ p ↦ c ↘ b }} -> + {{ ⟦ B' ⟧ p' ↦ c' ↘ b' }} -> + {{ Sub b <: b' at i }}) -> + {{ DF Π a p B ≈ Π a p B ∈ per_univ_elem i ↘ elem_rel }} -> + {{ DF Π a' p' B' ≈ Π a' p' B' ∈ per_univ_elem i ↘ elem_rel' }} -> + {{ Sub Π a p B <: Π a' p' B' at i }}) +where "'Sub' a <: b 'at' i" := (per_subtyp i a b) (in custom judg) : type_scope. + +#[export] + Hint Constructors per_subtyp : mcltt. + (** Context/Environment PER *) Definition rel_typ (i : nat) (A : typ) (p : env) (A' : typ) (p' : env) R' := rel_mod_eval (per_univ_elem i) A p A' p' R'. @@ -263,3 +291,26 @@ Definition valid_ctx : ctx -> Prop := fun Γ => per_ctx Γ Γ. Hint Transparent valid_ctx : mcltt. #[export] Hint Unfold valid_ctx : mcltt. + +Reserved Notation "'SubE' Γ <: Δ" (in custom judg at level 90, Γ custom exp, Δ custom exp). + + +Inductive per_ctx_subtyp : ctx -> ctx -> Prop := +| per_ctx_subtyp_nil : + {{ SubE ⋅ <: ⋅ }} +| per_ctx_subtyp_cons : + `{ forall tail_rel env_rel env_rel', + {{ SubE Γ <: Γ' }} -> + {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ tail_rel }} -> + (forall p p' a a' + (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}), + {{ ⟦ A ⟧ p ↘ a }} -> + {{ ⟦ A' ⟧ p' ↘ a' }} -> + {{ Sub a <: a' at i }}) -> + {{ EF Γ , A ≈ Γ , A ∈ per_ctx_env ↘ env_rel }} -> + {{ EF Γ' , A' ≈ Γ' , A' ∈ per_ctx_env ↘ env_rel' }} -> + {{ SubE Γ, A <: Γ', A' }} } +where "'SubE' Γ <: Δ" := (per_ctx_subtyp Γ Δ) (in custom judg) : type_scope. + +#[export] +Hint Constructors per_ctx_subtyp : mcltt. diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v index de7efe87..8bf74077 100644 --- a/theories/Core/Semantic/PER/Lemmas.v +++ b/theories/Core/Semantic/PER/Lemmas.v @@ -615,6 +615,175 @@ Proof with mautosolve. assert (j <= max i j) by lia... Qed. +Lemma per_subtyp_to_univ_elem : forall a b i, + {{ Sub a <: b at i }} -> + exists R R', + {{ DF a ≈ a ∈ per_univ_elem i ↘ R }} /\ + {{ DF b ≈ b ∈ per_univ_elem i ↘ R' }}. +Proof. + destruct 1; do 2 eexists; mauto; + split; per_univ_elem_econstructor; mauto; + try apply Equivalence_Reflexive. + lia. +Qed. + + +Lemma PER_refl1 A (R : relation A) `(per : PER A R) : forall a b, R a b -> R a a. +Proof. + intros. + etransitivity; [eassumption |]. + symmetry. assumption. +Qed. + +Lemma PER_refl2 A (R : relation A) `(per : PER A R) : forall a b, R a b -> R b b. +Proof. + intros. symmetry in H. + apply PER_refl1 in H; + auto. +Qed. + +Ltac saturate_refl := + repeat match goal with + | H : ?R ?a ?b |- _ => + tryif unify a b + then fail + else + directed pose proof (PER_refl1 _ _ _ _ _ H); + directed pose proof (PER_refl2 _ _ _ _ _ H); + fail_if_dup + end. + +Ltac saturate_refl_for hd := + repeat match goal with + | H : ?R ?a ?b |- _ => + unify R hd; + tryif unify a b + then fail + else + directed pose proof (PER_refl1 _ _ _ _ _ H); + directed pose proof (PER_refl2 _ _ _ _ _ H); + fail_if_dup + end. + +Ltac solve_refl := + solve [reflexivity || apply Equivalence_Reflexive]. + +Lemma per_elem_subtyping : forall A B i, + {{ Sub A <: B at i }} -> + forall R R' a b, + {{ DF A ≈ A ∈ per_univ_elem i ↘ R }} -> + {{ DF B ≈ B ∈ per_univ_elem i ↘ R' }} -> + R a b -> + R' a b. +Proof. + induction 1; intros. + all:handle_per_univ_elem_irrel; + (on_all_hyp: fun H => directed invert_per_univ_elem H); + apply_equiv_left; + trivial. + - firstorder mauto. + - intros. + handle_per_univ_elem_irrel. + assert (in_rel c c') by (apply_equiv_left; trivial). + assert (in_rel1 c c') by (apply_equiv_left; trivial). + destruct_rel_mod_eval. + destruct_rel_mod_app. + econstructor; eauto. + saturate_refl. + deepexec H1 ltac:(fun H => apply H). +Qed. + +Lemma per_subtyp_refl1 : forall a b i R, + {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} -> + {{ Sub a <: b at i }}. +Proof. + simpl; induction 1 using per_univ_elem_ind; + subst; + mauto; + destruct_all. + assert ({{ DF Π A p B ≈ Π A' p' B' ∈ per_univ_elem i ↘ elem_rel }}) + by (eapply per_univ_elem_pi'; eauto; intros; destruct_rel_mod_eval; mauto). + saturate_refl. + econstructor; eauto. + intros; + destruct_rel_mod_eval; + functional_eval_rewrite_clear; + trivial. +Qed. + +Lemma per_subtyp_refl2 : forall a b i R, + {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} -> + {{ Sub b <: a at i }}. +Proof. + intros. + symmetry in H. + eauto using per_subtyp_refl1. +Qed. + +Lemma per_subtyp_trans : forall A1 A2 i, + {{ Sub A1 <: A2 at i }} -> + forall A3, + {{ Sub A2 <: A3 at i }} -> + {{ Sub A1 <: A3 at i }}. +Proof. + induction 1; intros ? Hsub; simpl in *. + 1-3:progressive_inversion; + mauto. + - econstructor; lia. + - dependent destruction Hsub. + handle_per_univ_elem_irrel. + econstructor; eauto. + + etransitivity; eassumption. + + intros. + saturate_refl. + directed invert_per_univ_elem H6. + directed invert_per_univ_elem H7. + destruct_rel_mod_eval. + functional_eval_rewrite_clear. + deepexec (H0 c c') ltac:(fun H => pose proof H). + deepexec (H5 c' c') ltac:(fun H => pose proof H); + [ apply_equiv_left; trivial |]. + eauto. +Qed. + +#[export] + Hint Resolve per_subtyp_trans : mcltt. + +#[export] + Instance per_subtyp_trans_ins i : Transitive (per_subtyp i). +Proof. + eauto using per_subtyp_trans. +Qed. + +Lemma per_subtyp_cumu : forall A1 A2 i, + {{ Sub A1 <: A2 at i }} -> + forall j, + i <= j -> + {{ Sub A1 <: A2 at j }}. +Proof. + induction 1; intros; econstructor; mauto. + lia. +Qed. + +#[export] + Hint Resolve per_subtyp_cumu : mcltt. + +Lemma per_subtyp_cumu_left : forall A1 A2 i j, + {{ Sub A1 <: A2 at i }} -> + {{ Sub A1 <: A2 at max i j }}. +Proof. + intros. eapply per_subtyp_cumu; try eassumption. + lia. +Qed. + +Lemma per_subtyp_cumu_right : forall A1 A2 i j, + {{ Sub A1 <: A2 at i }} -> + {{ Sub A1 <: A2 at max j i }}. +Proof. + intros. eapply per_subtyp_cumu; try eassumption. + lia. +Qed. + Add Parametric Morphism : per_ctx_env with signature (@relation_equivalence env) ==> eq ==> eq ==> iff as per_ctx_env_morphism_iff. Proof with mautosolve. @@ -891,3 +1060,109 @@ Proof. intros * [? H]. induction H; simpl; congruence. Qed. + +Lemma per_ctx_subtyp_to_env : forall Γ Δ, + {{ SubE Γ <: Δ }} -> + exists R R', + {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ R }} /\ + {{ EF Δ ≈ Δ ∈ per_ctx_env ↘ R' }}. +Proof. + destruct 1; destruct_all. + - repeat eexists; econstructor; apply Equivalence_Reflexive. + - eauto. +Qed. + +Lemma per_ctx_env_subtyping : forall Γ Δ, + {{ SubE Γ <: Δ }} -> + forall R R' p p', + {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ R }} -> + {{ EF Δ ≈ Δ ∈ per_ctx_env ↘ R' }} -> + R p p' -> + R' p p'. +Proof. + induction 1; intros. + all:handle_per_ctx_env_irrel; + (on_all_hyp: fun H => directed invert_per_ctx_env H); + apply_equiv_left; + trivial. + + handle_per_ctx_env_irrel. + destruct_all. + deepexec IHper_ctx_subtyp ltac:(fun H => pose proof H). + deepexec H2 ltac:(fun H => destruct H as []). + deepexec H11 ltac:(fun H => destruct H as []). + deepexec H1 ltac:(fun H => pose proof H). + destruct (per_subtyp_to_univ_elem _ _ _ H15) as [? [? [? ?]]]. + handle_per_univ_elem_irrel. + eexists; try eassumption. + + eapply per_elem_subtyping with (i := max x (max i0 i)). + - eauto using per_subtyp_cumu_right. + - saturate_refl. + eauto using per_univ_elem_cumu_max_left. + - saturate_refl. + eauto using per_univ_elem_cumu_max_left, per_univ_elem_cumu_max_right. + - trivial. +Qed. + +Lemma per_ctx_subtyp_refl1 : forall Γ Δ R, + {{ EF Γ ≈ Δ ∈ per_ctx_env ↘ R }} -> + {{ SubE Γ <: Δ }}. +Proof. + induction 1; mauto. + + assert (exists R, {{ EF Γ , A ≈ Γ' , A' ∈ per_ctx_env ↘ R }}) by + (eexists; eapply @per_ctx_env_cons' with (i := i); eassumption). + destruct_all. + econstructor; try solve [saturate_refl; mauto 2]. + intros. + unfold rel_typ in *. + destruct_rel_mod_eval. + simplify_evals. + eauto using per_subtyp_refl1. +Qed. + +Lemma per_ctx_subtyp_refl2 : forall Γ Δ R, + {{ EF Γ ≈ Δ ∈ per_ctx_env ↘ R }} -> + {{ SubE Δ <: Γ }}. +Proof. + intros. symmetry in H. eauto using per_ctx_subtyp_refl1. +Qed. + +Lemma per_ctx_subtyp_trans : forall Γ1 Γ2, + {{ SubE Γ1 <: Γ2 }} -> + forall Γ3, + {{ SubE Γ2 <: Γ3 }} -> + {{ SubE Γ1 <: Γ3 }}. +Proof. + induction 1; intros; + progressive_inversion; + mauto 1; + clear_PER. + + handle_per_ctx_env_irrel. + econstructor; try eassumption. + - firstorder. + - instantiate (1 := max i i0). + intros. + cutexec per_ctx_env_subtyping H ltac:(fun H => deepexec H ltac:(fun H => pose proof H)). + cutexec per_ctx_env_subtyping H7 ltac:(fun H => deepexec H ltac:(fun H => pose proof H)). + deepexec H22 ltac:(fun H => destruct H as []). + + etransitivity. + + saturate_refl_for tail_rel4. + apply_equiv_right. + deepexec (H1 p p) ltac:(fun H => eauto using per_subtyp_cumu_left, H). + + eapply per_subtyp_cumu_right. + eapply H9; eauto. + apply_equiv_left; trivial. +Qed. + +#[export] + Hint Resolve per_ctx_subtyp_trans : mcltt. + +#[export] + Instance per_ctx_subtyp_trans_ins : Transitive per_ctx_subtyp. +Proof. + eauto using per_ctx_subtyp_trans. +Qed. diff --git a/theories/LibTactics.v b/theories/LibTactics.v index 8ed1439f..d1f5c4f6 100644 --- a/theories/LibTactics.v +++ b/theories/LibTactics.v @@ -266,12 +266,11 @@ Ltac deepexec lem tac := exvar T ltac:(fun x => lazymatch type of T with | Prop => match goal with - | H : _ |- _ => unify x H - | _ => idtac + | H : _ |- _ => unify x H; deepexec constr:(lem x) tac + | _ => deepexec constr:(lem x) tac end - | _ => idtac - end; - deepexec constr:(lem x) tac) + | _ => deepexec constr:(lem x) tac + end) | _ => tac lem end. @@ -291,14 +290,13 @@ Ltac cutexec lem C tac := unify x C; tac lem else - (lazymatch type of T with + lazymatch type of T with | Prop => match goal with - | H : _ |- _ => unify x H - | _ => idtac + | H : _ |- _ => unify x H; cutexec constr:(lem x) C tac + | _ => cutexec constr:(lem x) C tac end - | _ => idtac - end; - cutexec constr:(lem x) C tac)) + | _ => cutexec constr:(lem x) C tac + end) | _ => tac lem end. @@ -348,3 +346,11 @@ Ltac unify_args H P := #[global] Ltac apply_equiv_right := repeat apply_equiv_right1. + +#[global] + Ltac clear_PER := + repeat match goal with + | H : PER _ |- _ => clear H + | H : Symmetric _ |- _ => clear H + | H : Transitive _ |- _ => clear H + end.