From 74d3c46b352173db8eae63016822090b5c37c0d6 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 7 Jul 2019 01:10:16 +0200 Subject: [PATCH] olty: switch to higher-order semantic types Also switch experiments, but now we must merge both experiments and introduce higher-order type members and kinds. --- theories/olty.v | 217 +++++++++++++++++++----------------- theories/olty_experiments.v | 97 +++++++++------- 2 files changed, 172 insertions(+), 142 deletions(-) diff --git a/theories/olty.v b/theories/olty.v index f46cbf578..2c888f523 100644 --- a/theories/olty.v +++ b/theories/olty.v @@ -11,26 +11,28 @@ Module Type OLty (Import VS: VlSortsFullSig). Include LiftWp VS. Section olty_limit_preserving. - Context `{Σ : gFunctors}. + Context `{Σ : gFunctors} {i : nat}. - Definition envD_persistent (A : envD Σ) := ∀ ρ w, Persistent (A ρ w). + Definition hoEnvD_persistent (A : hoEnvD Σ i) := ∀ args ρ w, Persistent (A args ρ w). - Instance: LimitPreserving envD_persistent. + Instance: LimitPreserving hoEnvD_persistent. Proof. + apply limit_preserving_forall=> args; apply limit_preserving_forall=> ρ; apply limit_preserving_forall=> w. - apply bi.limit_preserving_Persistent => n ?? H. exact: H. + apply bi.limit_preserving_Persistent => n f g Heq. exact: Heq. Qed. - Definition vclosed (A : envD Σ) := ∀ ρ v, A ρ v ⊢ ⌜ nclosed_vl v 0 ⌝. + Definition vclosed (A : hoEnvD Σ i) := ∀ args ρ v, A args ρ v ⊢ ⌜ nclosed_vl v 0 ⌝. Instance: LimitPreserving vclosed. Proof. + apply limit_preserving_forall=> args; apply limit_preserving_forall=> ρ; apply limit_preserving_forall=> w. apply limit_preserving_entails; last apply _. - solve_proper_ho. + move => n f g Heq. exact: Heq. Qed. - Definition restrict A := vclosed A ∧ envD_persistent A. + Definition restrict A := vclosed A ∧ hoEnvD_persistent A. Global Instance: LimitPreserving restrict. Proof. apply limit_preserving_and; apply _. @@ -41,84 +43,86 @@ End olty_limit_preserving. "Open Logical TYpes": persistent Iris predicates over environments and values. Adapted from https://gitlab.mpi-sws.org/iris/examples/blob/d4f4153920ea82617c7222aeeb00b6710d51ee03/theories/logrel_heaplang/ltyping.v#L5. *) -Record olty Σ := Olty { - olty_car :> (var → vl) → vl → iProp Σ; +Record olty Σ i := Olty { + olty_car :> vec vl i → (var → vl) → vl → iProp Σ; olty_vclosed : vclosed olty_car; - olty_persistent ρ v : Persistent (olty_car ρ v); + olty_persistent args ρ v : Persistent (olty_car args ρ v); }. -Global Arguments Olty {_} _%I _ {_}. -Global Arguments olty_car {_} _ _ _: simpl never. -Global Arguments olty_vclosed {_} _ _ _ /. +Global Arguments Olty {_ _} _%I _ {_}. +Global Arguments olty_car {_ _} _ _ _ _: simpl never. +Global Arguments olty_vclosed {_ _} _ _ _. Bind Scope olty_scope with olty. Delimit Scope olty_scope with T. Global Existing Instance olty_persistent. (* Different from normal TyInterp. Better? *) -Class OTyInterp ty Σ := - oty_interp: ty → olty Σ. +Class OTyInterp (ty : nat → Type) Σ := + oty_interp : ∀ {i}, ty i → olty Σ i. +(* Forces inserting coercions to -d>. *) +Notation oApp := (olty_car : olty _ _ → hoEnvD _ _). -Local Definition testCoerce `(τ : olty Σ) ρ := τ ρ. +Local Definition testCoerce `(τ : olty Σ 0) := vclose (oApp τ). Section olty_ofe. - Context `{Σ : gFunctors}. - Implicit Types (φ : envD Σ) (τ : olty Σ). + Context `{Σ : gFunctors} {i : nat}. + Implicit Types (φ : hoEnvD Σ i) (τ : olty Σ i). - Instance olty_equiv : Equiv (olty Σ) := λ A B, A ≡@{envD Σ} B. - Instance olty_dist : Dist (olty Σ) := λ n A B, A ≡{n}@{envD Σ}≡ B. - Lemma olty_ofe_mixin : OfeMixin (olty Σ). - Proof. by apply (iso_ofe_mixin (olty_car : _ → (var → vl) -d> vl -d> _)). Qed. - Canonical Structure oltyO := OfeT (olty Σ) olty_ofe_mixin. + Instance olty_equiv : Equiv (olty Σ i) := λ A B, oApp A ≡ B. + Instance olty_dist : Dist (olty Σ i) := λ n A B, oApp A ≡{n}≡ B. + Lemma olty_ofe_mixin : OfeMixin (olty Σ i). + Proof. by apply (iso_ofe_mixin oApp). Qed. + Canonical Structure oltyO := OfeT (olty Σ i) olty_ofe_mixin. (* Only needed to define Olty using Iris fixpoints (e.g. for normal recursive types). *) Global Instance olty_cofe : Cofe oltyO. Proof. - set curry_olty : ∀ A, restrict A → olty Σ := λ A '(conj P1 P2), @Olty Σ A P1 P2. + set curry_olty : ∀ A, restrict A → olty Σ i := λ A '(conj P1 P2), @Olty Σ i A P1 P2. apply (iso_cofe_subtype' restrict curry_olty olty_car) => //. - by move => []. - by move => ? []. - apply _. Qed. - Global Program Instance olty_inhabited : Inhabited (olty Σ) := populate (Olty (λ _ _, False)%I _). + Global Program Instance olty_inhabited : Inhabited (olty Σ i) := populate (Olty (λ _ _ _, False)%I _). Next Obligation. by unseal=>?. Qed. - Global Instance olty_car_ne : NonExpansive (@olty_car Σ : olty Σ -> envD Σ). + Global Instance olty_car_ne : NonExpansive oApp. Proof. intros n f g Heq. apply Heq. Qed. - Global Instance lty_car_proper : Proper ((≡) ==> (≡)) (@olty_car Σ : olty Σ -> envD Σ). + Global Instance lty_car_proper : Proper ((≡) ==> (≡)) oApp. Proof. apply ne_proper, olty_car_ne. Qed. - Program Definition pack φ (Hvc : vclosed φ) := Olty (λ ρ v, □ φ ρ v)%I _. + Program Definition pack φ (Hvc : vclosed φ) := Olty (λ args ρ v, □ φ args ρ v)%I _. Next Obligation. rewrite /vclosed; intros. iIntros "?". by iApply Hvc. Qed. Lemma persistently_id (P : iProp Σ) `{!Persistent P}: □P ⊣⊢ P. (* Proof. by iSplit; iIntros. Qed. *) Proof. apply: intuitionistic_intuitionistically. Qed. - Lemma olty_car_pack_id φ (H : vclosed φ) `{∀ ρ v, Persistent (φ ρ v)} : - olty_car (pack φ H) ≡@{envD Σ} φ. + Lemma olty_car_pack_id φ (H : vclosed φ) `{∀ args ρ v, Persistent (φ args ρ v)} : + oApp (pack φ H) ≡ φ. Proof. - move => ?? /=. + move => ??? /=. apply: intuitionistic_intuitionistically. Qed. Lemma pack_olty_car_id τ : pack (olty_car τ) (olty_vclosed τ) ≡ τ. Proof. - move: τ => []?????/=. + move: τ => [τ Hp Hvc] args ρ v; rewrite /olty_car/=. apply: intuitionistic_intuitionistically. Qed. - Global Instance ids_envD : Ids (envD Σ) := λ _, inhabitant. - Global Instance rename_envD : Rename (envD Σ) := - λ r φ ρ, φ (r >>> ρ). - Global Instance hsubst_envD : HSubst vl (envD Σ) := - λ sb φ ρ, φ (sb >> ρ). + Global Instance ids_hoEnvD : Ids (hoEnvD Σ i) := λ _, inhabitant. + Global Instance rename_hoEnvD : Rename (hoEnvD Σ i) := + λ r φ args ρ, φ args (r >>> ρ). + Global Instance hsubst_hoEnvD : HSubst vl (hoEnvD Σ i) := + λ sb φ args ρ, φ args (sb >> ρ). - Ltac renLemmas_envD := - hnf; rewrite /hsubst /hsubst_envD => /= *; - try (apply FunctionalExtensionality.functional_extensionality_dep => ?); by asimpl. + Ltac renLemmas_hoEnvD := + hnf; rewrite /hsubst /hsubst_hoEnvD => /= *; + do 2 (apply FunctionalExtensionality.functional_extensionality_dep => ?); by asimpl. - Global Instance HSubstLemmas_envD : HSubstLemmas vl (envD Σ). - Proof. split => //; renLemmas_envD. Qed. + Global Instance HSubstLemmas_hoEnvD : HSubstLemmas vl (hoEnvD Σ i). + Proof. split => //; renLemmas_hoEnvD. Qed. (* Since substitution lemmas don't use setoids, @@ -127,30 +131,30 @@ Section olty_ofe. Lemma olty_eq τ1 τ2: olty_car τ1 = olty_car τ2 → τ1 = τ2. Proof. - move: τ1 τ2 => [φ1 ??] [φ2 ??]; rewrite /olty_car. - destruct 1. f_equal; exact: ProofIrrelevance.proof_irrelevance. + move: τ1 τ2 => [φ1 Hp1 Hvc1] [φ2 Hp2 Hvc2]. rewrite /olty_car /=. + intros ->. f_equal; exact: ProofIrrelevance.proof_irrelevance. Qed. - Global Instance ids_olty : Ids (olty Σ) := λ _, inhabitant. - Global Program Instance rename_olty : Rename (olty Σ) := + Global Instance ids_olty : Ids (olty Σ i) := λ _, inhabitant. + Global Program Instance rename_olty : Rename (olty Σ i) := λ r τ, Olty (rename r (olty_car τ)) _. Next Obligation. rewrite /vclosed; intros. exact: olty_vclosed. Qed. - Global Program Instance hsubst_olty : HSubst vl (olty Σ) := + Global Program Instance hsubst_olty : HSubst vl (olty Σ i) := λ sb τ, Olty ((olty_car τ).|[sb]) (_ (olty_car τ).|[sb]). Next Obligation. rewrite /vclosed; intros. exact: olty_vclosed. Qed. - Global Instance hsubstLemmas_olty : HSubstLemmas vl (olty Σ). + Global Instance hsubstLemmas_olty : HSubstLemmas vl (olty Σ i). Proof. split=> [s|??|?? s]; apply olty_eq => //; case: s => [φ??]; rewrite /hsubst /hsubst_olty /olty_car. all: trivial using hsubst_id, id_hsubst, hsubst_comp. Qed. -(* Global Instance rename_olty2 : Rename (olty Σ) := +(* Global Instance rename_olty2 : Rename (olty Σ i) := λ r τ, Olty (λ ρ, τ (r >>> ρ)) (λ ρ, olty_vclosed τ _). - Global Instance hsubst_olty2 : HSubst vl (olty Σ) := + Global Instance hsubst_olty2 : HSubst vl (olty Σ i) := λ sb τ, Olty (λ ρ, τ (sb >> ρ)) (λ ρ, olty_vclosed τ _). - Global Instance HSubstLemmas_olty2 : HSubstLemmas vl (olty Σ). + Global Instance HSubstLemmas_olty2 : HSubstLemmas vl (olty Σ i). Proof. split=> [s|??|?? s]; apply olty_eq => //; case: s => [φ??]; (apply functional_extensionality_dep => ?); @@ -158,47 +162,53 @@ Section olty_ofe. all: by asimpl. Qed. *) - Lemma envD_weaken ρ1 ρ2 ρ3 φ : - φ.|[upn (length ρ1) (ren (+ length ρ2))] (to_subst (ρ1 ++ ρ2 ++ ρ3)) - = φ (to_subst (ρ1 ++ ρ3)). - Proof. rewrite /hsubst_envD /hsubst to_subst_weaken //. Qed. + Lemma hoEnvD_weaken ρ1 ρ2 ρ3 φ args : + φ.|[upn (length ρ1) (ren (+ length ρ2))] args (to_subst (ρ1 ++ ρ2 ++ ρ3)) + = φ args (to_subst (ρ1 ++ ρ3)). + Proof. rewrite /hsubst_hoEnvD /hsubst to_subst_weaken //. Qed. - Lemma envD_subst_up ρ1 ρ2 v φ : - φ.|[upn (length ρ1) (v.[ren (+length ρ2)] .: ids)] (to_subst (ρ1 ++ ρ2)) - ≡ φ (to_subst (ρ1 ++ v :: ρ2)). - Proof. rewrite /hsubst_envD /hsubst to_subst_up //. Qed. + Lemma hoEnvD_subst_up ρ1 ρ2 v φ args : + φ.|[upn (length ρ1) (v.[ren (+length ρ2)] .: ids)] args (to_subst (ρ1 ++ ρ2)) + ≡ φ args (to_subst (ρ1 ++ v :: ρ2)). + Proof. rewrite /hsubst_hoEnvD /hsubst to_subst_up //. Qed. - Lemma olty_weaken ρ1 ρ2 ρ3 τ : - τ.|[upn (length ρ1) (ren (+ length ρ2))] (to_subst (ρ1 ++ ρ2 ++ ρ3)) - = τ (to_subst (ρ1 ++ ρ3)). + Lemma olty_weaken ρ1 ρ2 ρ3 τ args : + τ.|[upn (length ρ1) (ren (+ length ρ2))] args (to_subst (ρ1 ++ ρ2 ++ ρ3)) + = τ args (to_subst (ρ1 ++ ρ3)). Proof. - (* rewrite /hsubst_olty /hsubst_envD /hsubst /= to_subst_weaken //. *) + (* rewrite /hsubst_olty /hsubst_hoEnvD /hsubst /= to_subst_weaken //. *) rewrite [@hsubst _ _ hsubst_olty]/hsubst /hsubst_olty /=. - exact: envD_weaken. + exact: hoEnvD_weaken. Qed. - Lemma envD_weaken_one v φ ρ: - φ.|[ren (+1)] (v .: to_subst ρ) = φ (to_subst ρ). - Proof. by rewrite (envD_weaken [] [v]). Qed. + Lemma hoEnvD_weaken_one v φ ρ args : + φ.|[ren (+1)] args (v .: to_subst ρ) = φ args (to_subst ρ). + Proof. by rewrite (hoEnvD_weaken [] [v]). Qed. - Lemma olty_weaken_one v τ ρ: - τ.|[ren (+1)] (v .: to_subst ρ) ≡@{vl -d> _} τ (to_subst ρ). + Lemma olty_weaken_one v τ ρ args : + oApp τ.|[ren (+1)] args (v .: to_subst ρ) ≡ τ args (to_subst ρ). Proof. by rewrite (olty_weaken [] [v]). Qed. - Lemma olty_subst_up ρ1 ρ2 v τ : - τ.|[upn (length ρ1) (v.[ren (+length ρ2)] .: ids)] (to_subst (ρ1 ++ ρ2)) - ≡@{vl -d> _} τ (to_subst (ρ1 ++ v :: ρ2)). + Lemma olty_subst_up ρ1 ρ2 v τ args : + oApp τ.|[upn (length ρ1) (v.[ren (+length ρ2)] .: ids)] args (to_subst (ρ1 ++ ρ2)) + ≡ τ args (to_subst (ρ1 ++ v :: ρ2)). Proof. - (* rewrite /hsubst_olty /hsubst_envD /hsubst /= to_subst_up //. *) + (* rewrite /hsubst_olty /hsubst_hoEnvD /hsubst /= to_subst_up //. *) rewrite [@hsubst _ _ hsubst_olty]/hsubst /hsubst_olty /=. - exact: envD_subst_up. + exact: hoEnvD_subst_up. Qed. +End olty_ofe. + +Notation oClose φ := (olty_car φ vnil : envD _). +Section olty_ofe_2. + Context `{Σ : gFunctors} {i : nat}. + Implicit Types (φ : hoEnvD Σ i) (τ : olty Σ i). - Definition sCtx := list (olty Σ). + Definition sCtx := list (olty Σ 0). Fixpoint env_oltyped (Γ : sCtx) (ρ : var → vl) : iProp Σ := match Γ with - | φ :: Γ' => env_oltyped Γ' ((+1) >>> ρ) ∗ φ ρ (ρ 0) + | φ :: Γ' => env_oltyped Γ' ((+1) >>> ρ) ∗ oClose φ ρ (ρ 0) | nil => True end%I. @@ -209,7 +219,7 @@ Section olty_ofe. env_oltyped Γ ρ -∗ ⌜ nclosed_sub (length Γ) 0 ρ ⌝. Proof. elim: Γ ρ => [|φ Γ IHΓ] ρ /=; [| rewrite IHΓ olty_vclosed ]; iIntros "!% //". - - move => [Hclρ Hclp0] [|i /lt_S_n] Hle. exact Hclp0. apply Hclρ, Hle. + - move => [Hclρ Hclp0] [|n /lt_S_n] Hle. exact Hclp0. apply Hclρ, Hle. Qed. Lemma env_oltyped_cl_app `{Sort X} (x : X) Γ ρ: @@ -224,7 +234,7 @@ Section olty_ofe. Fixpoint env_oltyped_fin (Γ : sCtx) vs : iProp Σ := match Γ, vs with - | φ :: Γ', v :: vs => env_oltyped_fin Γ' vs ∗ φ (v .: to_subst vs) v + | φ :: Γ', v :: vs => env_oltyped_fin Γ' vs ∗ oClose φ (v .: to_subst vs) v | nil, nil => True | _, _ => False end%I. @@ -276,9 +286,9 @@ Section olty_ofe. by iIntros "!%". Qed. - Lemma interp_env_lookup Γ ρ τ x: + Lemma interp_env_lookup Γ ρ (τ : olty Σ 0) x: Γ !! x = Some τ → - ⟦ Γ ⟧* ρ -∗ τ.|[ren (+x)] (to_subst ρ) (to_subst ρ x). + ⟦ Γ ⟧* ρ -∗ oClose τ.|[ren (+x)] (to_subst ρ) (to_subst ρ x). Proof. elim: Γ ρ x => [//|τ' Γ' IHΓ] [|v ρ] x Hx /=. by iIntros "[]". iDestruct 1 as "[Hg Hv]". move: x Hx => [ [->] | x Hx] /=. @@ -288,38 +298,43 @@ Section olty_ofe. iApply (IHΓ ρ x Hx with "Hg"). Qed. - Program Definition closed_olty (φ : envD Σ) `{∀ ρ v, Persistent (φ ρ v)} : olty Σ := - Olty (λ ρ v, ⌜ nclosed_vl v 0 ⌝ ∗ φ ρ v)%I _. - Next Obligation. iIntros (????) "[$_]". Qed. + Program Definition ho_closed_olty {i} (φ : hoEnvD Σ i) `{∀ args ρ v, Persistent (φ args ρ v)} : olty Σ i := + Olty (λ args ρ v, ⌜ nclosed_vl v 0 ⌝ ∗ φ args ρ v)%I _. + Next Obligation. iIntros (??????) "[$_]". Qed. + + Definition closed_olty (φ : envD Σ)`{∀ ρ v, Persistent (φ ρ v)} : olty Σ 0 := + ho_closed_olty (vopen φ). (** We can define once and for all basic "logical" types: top, bottom, and, or, later and μ. *) - Definition oTop := closed_olty (λ ρ v, True)%I. + Definition oTop : olty Σ i := ho_closed_olty (λ args ρ v, True)%I. - Program Definition oBot : olty Σ := Olty (λ ρ v, False)%I _. + Program Definition oBot : olty Σ i := Olty (λ args ρ v, False)%I _. Next Obligation. intros **?**. exact: False_elim. Qed. - Program Definition oAnd τ1 τ2 : olty Σ := Olty (λ ρ v, τ1 ρ v ∧ τ2 ρ v)%I _. + Program Definition oAnd τ1 τ2 : olty Σ i := Olty (λ args ρ v, τ1 args ρ v ∧ τ2 args ρ v)%I _. Next Obligation. intros **?**. rewrite olty_vclosed. iIntros "[$ _]". Qed. - Program Definition oOr τ1 τ2 : olty Σ := Olty (λ ρ v, τ1 ρ v ∨ τ2 ρ v)%I _. + Program Definition oOr τ1 τ2 : olty Σ i := Olty (λ args ρ v, τ1 args ρ v ∨ τ2 args ρ v)%I _. Next Obligation. intros **?**. rewrite !olty_vclosed. iIntros "[$ | $]". Qed. - Definition eLater i (φ : envD Σ) : envD Σ := (λ ρ v, ▷^i φ ρ v)%I. - Definition oLater τ := closed_olty (eLater 1 τ). + Definition eLater n (φ : hoEnvD Σ i) : hoEnvD Σ i := (λ args ρ v, ▷^n φ args ρ v)%I. + Definition oLater τ := ho_closed_olty (eLater 1 τ). - Program Definition oMu τ : olty Σ := Olty (λ ρ v, τ (v .: ρ) v) _. + Program Definition ho_oMu {i} (τ : olty Σ i) : olty Σ i := Olty (λ args ρ v, τ args (v .: ρ) v) _. Next Obligation. rewrite /vclosed; intros. exact: olty_vclosed. Qed. - Lemma interp_TMu_ren T ρ v: oMu T.|[ren (+1)] (to_subst ρ) v ≡ T (to_subst ρ) v. - Proof. rewrite [_ (oMu _)]/olty_car /= (olty_weaken_one v T ρ v). by []. Qed. + Definition oMu (τ : olty Σ 0) : olty Σ 0 := ho_oMu τ. - Definition interp_expr `{dlangG Σ} (φ : envD Σ) : envPred tm Σ := - λ ρ t, WP t {{ φ ρ }} %I. + Lemma interp_TMu_ren (T : olty Σ i) args ρ v: ho_oMu T.|[ren (+1)] args (to_subst ρ) v ≡ T args (to_subst ρ) v. + Proof. rewrite [_ (ho_oMu _)]/olty_car /= (olty_weaken_one v T ρ args v). by []. Qed. + + Definition interp_expr `{dlangG Σ} (φ : hoEnvD Σ 0) : envPred tm Σ := + λ ρ t, WP t {{ vclose φ ρ }} %I. Global Arguments interp_expr /. Definition oTSel0 `{dlangG Σ} s σ := closed_olty (λ ρ v, ∃ ψ, s ↗[ σ ] ψ ∧ ▷ □ ψ v)%I. -End olty_ofe. +End olty_ofe_2. Notation "⟦ Γ ⟧*" := (env_oltyped_fin Γ). Arguments oltyO : clear implicits. @@ -329,11 +344,11 @@ Module Type OLtyJudgements (Import VS: VlSortsFullSig). Include OLty VS. Section judgments. Context `{dlangG Σ}. - Implicit Types (τ : olty Σ). + Implicit Types (τ : olty Σ 0). Definition step_indexed_ivstp Γ τ1 τ2 i j: iProp Σ := (□∀ ρ v, ⌜ nclosed_vl v 0 ⌝ → - ⟦Γ⟧*ρ → (▷^i τ1 (to_subst ρ) v) → ▷^j τ2 (to_subst ρ) v)%I. + ⟦Γ⟧*ρ → (▷^i oClose τ1 (to_subst ρ) v) → ▷^j oClose τ2 (to_subst ρ) v)%I. Global Arguments step_indexed_ivstp /. Definition ietp Γ τ e : iProp Σ := (⌜ nclosed e (length Γ) ⌝ ∗ @@ -342,7 +357,7 @@ Section judgments. Definition step_indexed_ietp Γ τ e i: iProp Σ := (⌜ nclosed e (length Γ) ⌝ ∗ □∀ ρ, ⟦Γ⟧* ρ → - interp_expr (λ ρ v, ▷^i τ ρ v) (to_subst ρ) (e.|[to_subst ρ]))%I. + interp_expr (eLater i τ) (to_subst ρ) (e.|[to_subst ρ]))%I. Global Arguments step_indexed_ietp /. End judgments. @@ -353,11 +368,11 @@ Notation "Γ ⊨ [ τ1 , i ] <: [ τ2 , j ]" := (step_indexed_ivstp Γ τ1 τ2 Section typing. Context `{dlangG Σ}. - Implicit Types (τ : olty Σ). + Implicit Types (τ : olty Σ 0). - Lemma iterate_TLater_later i (τ : olty Σ) ρ v: + Lemma iterate_TLater_later i τ ρ v: nclosed_vl v 0 → - (iterate oLater i τ) ρ v ≡ (▷^i τ ρ v)%I. + oClose (iterate oLater i τ) ρ v ≡ (vclose (eLater i τ) ρ v). Proof. elim: i => [|i IHi] // => Hcl. rewrite iterate_S [_ ρ]/olty_car/= /eLater IHi //. iSplit; by [iIntros "#[_ $]" | iIntros "$"]. diff --git a/theories/olty_experiments.v b/theories/olty_experiments.v index 3c20af14b..e8ee7756e 100644 --- a/theories/olty_experiments.v +++ b/theories/olty_experiments.v @@ -34,9 +34,9 @@ Implicit Types (v: vl) (vs : vls) (ρ : env). Section judgments. Context `{dlangG Σ} `{OTyInterp ty Σ}. -Implicit Type (τ : olty Σ). +Implicit Type (τ : olty Σ 0). -Notation ctx := (list ty). +Notation ctx := (list (ty 0)). Notation "⟦ T ⟧" := (oty_interp T). @@ -56,7 +56,7 @@ Definition judgment_holds `{Closeable s} (Γ : sCtx) (J : judgment Σ s): iProp Notation "Γ ⊨ J" := (judgment_holds Γ J) (at level 74, J at next level). Global Arguments judgment_holds /. -Program Definition ivtp τ v : judgment Σ vl := subj_judgment_to_judgment (v, τ). +Program Definition ivtp τ v : judgment Σ vl := subj_judgment_to_judgment (v, oClose τ). Global Arguments ivtp /. (* DOT/D<: judgments are indexed by [⋅]. *) @@ -74,13 +74,13 @@ Definition test_judge_me2 Γ t τ := Γ ⊨ t t⋅: τ. Program Definition nosubj_judgment_to_judgment {Σ} : nosubj_judgment Σ → judgment Σ vl := λ φ, (None, λ ρ _, φ ρ). -Definition ivstp τ1 τ2 : nosubj_judgment Σ := (λ ρ, ∀ v, ⌜ nclosed_vl v 0 ⌝ → τ1 ρ v → τ2 ρ v)%I. +Definition ivstp τ1 τ2 : nosubj_judgment Σ := (λ ρ, ∀ v, ⌜ nclosed_vl v 0 ⌝ → oClose τ1 ρ v → oClose τ2 ρ v)%I. Program Definition step_indexed_ivstp τ1 i1 τ2 i2 := nosubj_judgment_to_judgment (Σ := Σ) - (λ ρ, ∀ v, ⌜ nclosed_vl v 0 ⌝ → (▷^i1 τ1 ρ v) → ▷^i2 τ2 ρ v)%I. + (λ ρ, ∀ v, ⌜ nclosed_vl v 0 ⌝ → (▷^i1 oClose τ1 ρ v) → ▷^i2 oClose τ2 ρ v)%I. Notation "[ τ1 , i1 ] <: [ τ2 , i2 ]" := (step_indexed_ivstp τ1 i1 τ2 i2) (at level 73). Lemma equiv_vstp Γ τ1 τ2 i1 i2: Γ ⊨ [τ1 , i1] <: [τ2 , i2] ⊣⊢ - (□∀ vs v, ⌜ nclosed_vl v 0 ⌝ → env_oltyped_fin Γ vs → (▷^i1 τ1 (to_subst vs) v) → ▷^i2 τ2 (to_subst vs) v)%I. + (□∀ vs v, ⌜ nclosed_vl v 0 ⌝ → env_oltyped_fin Γ vs → (▷^i1 oClose τ1 (to_subst vs) v) → ▷^i2 oClose τ2 (to_subst vs) v)%I. Proof. iSplit; [iIntros "#[_ H] /= !>" (???) "#?" | iIntros "#H"; iSplit; first done; iIntros "!>" (?) "#? /="; iIntros (??)]. @@ -123,25 +123,26 @@ Notation "Γ ⊨d{ l := d } : T" := (idtp Γ l T d) (at level 64, d, l, T at ne Section SemTypes. Context `{HdotG: dlangG Σ}. - Implicit Types (φ : envD Σ) (τ : olty Σ) (ψ : vl -d> iProp Σ). + Implicit Types (τ : olty Σ 0). + (* (ψ : vl -d> iProp Σ) (φ : envD Σ) *) - Program Definition lift_dinterp_vl (T : dlty Σ): olty Σ := + Program Definition lift_dinterp_vl (T : dlty Σ): olty Σ 0 := closed_olty (λ ρ v, (∃ d, ⌜v @ dlty_label T ↘ d⌝ ∧ dlty_car T ρ d)%I). - Definition dm_to_type d ψ : iProp Σ := - (∃ s σ, ⌜ d = dtysem σ s ⌝ ∗ s ↗[ σ ] ψ)%I. - Notation "d ↗ ψ" := (dm_to_type d ψ) (at level 20). - Global Instance dm_to_type_persistent d ψ: Persistent (d ↗ ψ) := _. + Definition dm_to_type d i (ψ : hoD Σ i) : iProp Σ := + (∃ s σ, ⌜ d = dtysem σ s ⌝ ∗ s ↗n[ σ , i ] ψ)%I. + Notation "d ↗n[ i ] ψ" := (dm_to_type d i ψ) (at level 20). + Global Instance dm_to_type_persistent d i ψ: Persistent (d ↗n[ i ] ψ) := _. - Lemma dm_to_type_agree d ψ1 ψ2 v : d ↗ ψ1 -∗ d ↗ ψ2 -∗ ▷ (ψ1 v ≡ ψ2 v). + Lemma dm_to_type_agree d i ψ1 ψ2 args v : d ↗n[ i ] ψ1 -∗ d ↗n[ i ] ψ2 -∗ ▷ (ψ1 args v ≡ ψ2 args v). Proof. iDestruct 1 as (s σ ?) "#Hs1". iDestruct 1 as (s' σ' ?) "#Hs2". - simplify_eq. by iApply (stamp_σ_to_type_agree vnil with "Hs1 Hs2"). + simplify_eq. by iApply (stamp_σ_to_type_agree args with "Hs1 Hs2"). Qed. - Lemma dm_to_type_intro d s σ φ : - d = dtysem σ s → s ↝ φ -∗ d ↗ φ (to_subst σ). + Lemma dm_to_type_intro d i s σ φ : + d = dtysem σ s → s ↝n[ i ] φ -∗ d ↗n[ i ] hoEnvD_inst φ σ. Proof. iIntros. iExists s, σ. iFrame "%". by iApply stamp_σ_to_type_intro. @@ -149,17 +150,18 @@ Section SemTypes. Global Opaque dm_to_type. + (* Rewrite using (higher) semantic kinds! *) Definition oDTMem l τ1 τ2 : dlty Σ := Dlty l (λ ρ d, - ∃ ψ, (d ↗ ψ) ∗ - □ ((∀ v, ⌜ nclosed_vl v 0 ⌝ → ▷ τ1 ρ v → ▷ □ ψ v) ∗ - (∀ v, ⌜ nclosed_vl v 0 ⌝ → ▷ □ ψ v → ▷ τ2 ρ v)))%I. + ∃ ψ, (d ↗n[ 0 ] ψ) ∗ + □ ((∀ v, ⌜ nclosed_vl v 0 ⌝ → ▷ τ1 vnil ρ v → ▷ □ ψ vnil v) ∗ + (∀ v, ⌜ nclosed_vl v 0 ⌝ → ▷ □ ψ vnil v → ▷ τ2 vnil ρ v)))%I. Definition oTTMem l τ1 τ2 := lift_dinterp_vl (oDTMem l τ1 τ2). Definition oDVMem l τ : dlty Σ := Dlty l - (λ ρ d, ∃ vmem, ⌜d = dvl vmem⌝ ∧ ▷ τ ρ vmem)%I. + (λ ρ d, ∃ vmem, ⌜d = dvl vmem⌝ ∧ ▷ oClose τ ρ vmem)%I. Definition oTVMem l τ := lift_dinterp_vl (oDVMem l τ). @@ -169,7 +171,7 @@ Section SemTypes. Definition oTSel p (l : label) := closed_olty (λ ρ v, path_wp p.|[ρ] - (λ vp, ∃ ψ d, ⌜vp @ l ↘ d⌝ ∧ d ↗ ψ ∧ ▷ □ ψ v))%I. + (λ vp, ∃ ψ d, ⌜vp @ l ↘ d⌝ ∧ d ↗n[ 0 ] ψ ∧ ▷ □ ψ vnil v))%I. Lemma Sub_Sel Γ L U va l i: Γ ⊨ tv va : oTTMem l L U, i -∗ @@ -191,7 +193,7 @@ Section SemTypes. iNext. iDestruct "Hva" as (Hclvas d Hl ψ) "#[Hlψ [#HLψ #HψU]]". iDestruct "Hψ" as (ψ1 d1 Hva) "[Hγ #Hψ1v]". - objLookupDet; subst. iDestruct (dm_to_type_agree d _ _ v with "Hlψ Hγ") as "#Hag". + objLookupDet; subst. iDestruct (dm_to_type_agree d _ _ _ vnil v with "Hlψ Hγ") as "#Hag". iApply "HψU" => //. iNext. by iRewrite "Hag". Qed. @@ -239,18 +241,25 @@ End SemTypes. *) Module FinSubst. Section Sec. - Context `{HdotG: dlangG Σ}. - Implicit Types (φ : envD Σ) (τ : olty Σ). + Context `{HdotG: dlangG Σ} {i : nat}. + Implicit Types (φ : hoEnvD Σ i) (τ : olty Σ i). Definition envD_equiv n φ1 φ2 : iProp Σ := - (∀ ρ v, ⌜ length ρ = n ⌝ → ⌜ cl_ρ ρ ⌝ → φ1 (to_subst ρ) v ≡ φ2 (to_subst ρ) v)%I. - Notation "φ1 ≈[ n ] φ2" := (envD_equiv n φ1 φ2) (at level 70). + (∀ args ρ v, ⌜ length ρ = n ⌝ → ⌜ cl_ρ ρ ⌝ → + φ1 args (to_subst ρ) v ≡ φ2 args (to_subst ρ) v)%I. Definition leadsto_envD_equiv (sσ : extractedTy) n φ : iProp Σ := let '(s, σ) := sσ in - (⌜nclosed_σ σ n⌝ ∧ ∃ (φ' : envD Σ), s ↝ φ' ∗ envD_equiv n φ (λ ρ, φ' (to_subst σ.|[ρ])))%I. + (⌜nclosed_σ σ n⌝ ∧ ∃ (φ' : hoEnvD Σ i), s ↝n[ i ] φ' ∗ + envD_equiv n φ (λ args ρ, φ' args (to_subst σ.|[ρ])))%I. Arguments leadsto_envD_equiv /. - Notation "sσ ↝[ n ] φ" := (leadsto_envD_equiv sσ n φ) (at level 20). +End Sec. + +Notation "φ1 ≈[ n ] φ2" := (envD_equiv n φ1 φ2) (at level 70). +Notation "sσ ↝[ n ] φ" := (leadsto_envD_equiv sσ n φ) (at level 20). + +Section Sec2. + Context `{HdotG: dlangG Σ}. Lemma D_Typ Γ T L U s σ l : Γ ⊨ [T, 1] <: [U, 1] -∗ @@ -263,7 +272,8 @@ Section Sec. iDestruct (interp_env_props with "Hg") as %[Hclp Hlen]; rewrite <- Hlen in *. (* iDestruct (env_oltyped_fin_cl_ρ with "Hg") as %Hclp. *) iDestruct "Hs" as (φ) "[Hγ Hγφ]". - iExists (φ (to_subst σ.|[to_subst ρ])); iSplit. + rewrite /dlty_car /=. + iExists (hoEnvD_inst φ (σ.|[to_subst ρ])); iSplit. by iApply dm_to_type_intro. rewrite /envD_equiv. iModIntro; repeat iSplitL; iIntros (v Hclv) "#HL"; rewrite later_intuitionistically. @@ -273,28 +283,32 @@ Section Sec. by iApply (internal_eq_iff with "(Hγφ [#//] [#//])"). Qed. - Lemma D_Typ_Concr Γ τ s σ l: + Lemma D_Typ_Concr Γ (τ : olty Σ 0) s σ l: (s, σ) ↝[ length Γ ] τ -∗ Γ ⊨d{ l := dtysem σ s } : oDTMem l τ τ. Proof. iIntros "#Hs"; iApply D_Typ; by [| iIntros "!> **"]. Qed. -End Sec. +End Sec2. End FinSubst. Module InfSubst. Section Sec. - Context `{HdotG: dlangG Σ}. - Implicit Types (φ : envD Σ) (τ : olty Σ). + Context `{HdotG: dlangG Σ} {i : nat}. + Implicit Types (φ : hoEnvD Σ i) (τ : olty Σ i). Definition infEnvD_equiv n φ1 φ2 : iProp Σ := - (∀ ρ v, ⌜ nclosed_sub n 0 ρ ⌝ → φ1 ρ v ≡ φ2 ρ v)%I. - Notation "φ1 ≈[ n ] φ2" := (infEnvD_equiv n φ1 φ2) (at level 70). + (∀ args ρ v, ⌜ nclosed_sub n 0 ρ ⌝ → φ1 args ρ v ≡ φ2 args ρ v)%I. Definition leadsto_infEnvD_equiv (sσ: extractedTy) n φ : iProp Σ := let '(s, σ) := sσ in - (⌜nclosed_σ σ n⌝ ∧ ∃ (φ' : envD Σ), s ↝ φ' ∗ - infEnvD_equiv n φ (λ ρ, φ' (to_subst σ.|[ρ])))%I. - Notation "sσ ↝[ n ] φ" := (leadsto_infEnvD_equiv sσ n φ) (at level 20). + (⌜nclosed_σ σ n⌝ ∧ ∃ (φ' : hoEnvD Σ i), s ↝n[ i ] φ' ∗ + infEnvD_equiv n φ (λ args ρ, φ' args (to_subst σ.|[ρ])))%I. +End Sec. + +Notation "φ1 ≈[ n ] φ2" := (infEnvD_equiv n φ1 φ2) (at level 70). +Notation "sσ ↝[ n ] φ" := (leadsto_infEnvD_equiv sσ n φ) (at level 20). +Section Sec2. + Context `{HdotG: dlangG Σ}. Lemma D_Typ Γ T L U s σ l : Γ ⊨ [T, 1] <: [U, 1] -∗ Γ ⊨ [L, 1] <: [T, 1] -∗ @@ -305,7 +319,8 @@ Section Sec. iIntros "!>" (ρ) "#Hg /=". iDestruct (env_oltyped_fin_cl_ρ with "Hg") as %Hclp. iDestruct "Hs" as (φ) "[Hγ Hγφ]". - iExists (φ (to_subst σ.|[to_subst ρ])); iSplit. + iExists (hoEnvD_inst φ (σ.|[to_subst ρ])); iSplit. + (* iExists (φ (to_subst σ.|[to_subst ρ])); iSplit. *) by iApply dm_to_type_intro. iModIntro; repeat iSplitL; iIntros (v Hclv) "#HL"; rewrite later_intuitionistically. - iIntros "!>". iApply (internal_eq_iff with "(Hγφ [#//])"). @@ -314,11 +329,11 @@ Section Sec. by iApply (internal_eq_iff with "(Hγφ [#//])"). Qed. - Lemma D_Typ_Concr Γ τ s σ l: + Lemma D_Typ_Concr Γ (τ : olty Σ 0) s σ l: (s, σ) ↝[ length Γ ] τ -∗ Γ ⊨d{ l := dtysem σ s } : oDTMem l τ τ. Proof. iIntros "#Hs"; iApply D_Typ; by [| iIntros "!> **"]. Qed. -End Sec. +End Sec2. End InfSubst. End SemTypes.