From eaf53dcf2ae4ed4a836974f6b8ee08fffc4c8640 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> Date: Wed, 11 Sep 2019 06:07:18 +0200 Subject: [PATCH] lft_intersect is a Meet instance. --- theories/lifetime/lifetime.v | 2 +- theories/lifetime/lifetime_sig.v | 15 +++++++-------- theories/lifetime/model/definitions.v | 4 +--- theories/lifetime/model/primitive.v | 14 +++++++------- theories/typing/lft_contexts.v | 6 +++--- 5 files changed, 19 insertions(+), 22 deletions(-) diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v index c169f25e..4a2eb931 100644 --- a/theories/lifetime/lifetime.v +++ b/theories/lifetime/lifetime.v @@ -16,7 +16,7 @@ Module Export lifetime : lifetime_sig. Include creation. End lifetime. -Notation lft_intersect_list l := (foldr lft_intersect static l). +Notation lft_intersect_list l := (foldr (⊓) static l). Instance lft_inhabited : Inhabited lft := populate static. diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v index eb1d9569..77311728 100644 --- a/theories/lifetime/lifetime_sig.v +++ b/theories/lifetime/lifetime_sig.v @@ -21,7 +21,7 @@ Module Type lifetime_sig. (** Definitions *) Parameter lft : Type. Parameter static : lft. - Parameter lft_intersect : lft → lft → lft. + Declare Instance lft_intersect : Meet lft. Parameter lft_ctx : ∀ `{!invG Σ, !lftG Σ}, iProp Σ. @@ -44,7 +44,6 @@ Module Type lifetime_sig. Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : bi_scope. Infix "⊑" := lft_incl (at level 70) : bi_scope. - Infix "⊓" := lft_intersect (at level 40) : stdpp_scope. Section properties. Context `{!invG Σ, !lftG Σ}. @@ -53,12 +52,12 @@ Module Type lifetime_sig. Global Declare Instance lft_inhabited : Inhabited lft. Global Declare Instance bor_idx_inhabited : Inhabited bor_idx. - Global Declare Instance lft_intersect_comm : Comm eq lft_intersect. - Global Declare Instance lft_intersect_assoc : Assoc eq lft_intersect. - Global Declare Instance lft_intersect_inj_1 κ : Inj eq eq (lft_intersect κ). - Global Declare Instance lft_intersect_inj_2 κ : Inj eq eq (λ κ', lft_intersect κ' κ). - Global Declare Instance lft_intersect_left_id : LeftId eq static lft_intersect. - Global Declare Instance lft_intersect_right_id : RightId eq static lft_intersect. + Global Declare Instance lft_intersect_comm : Comm (A:=lft) eq (⊓). + Global Declare Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓). + Global Declare Instance lft_intersect_inj_1 (κ : lft) : Inj eq eq (κ ⊓). + Global Declare Instance lft_intersect_inj_2 (κ : lft) : Inj eq eq (⊓ κ). + Global Declare Instance lft_intersect_left_id : LeftId eq static meet. + Global Declare Instance lft_intersect_right_id : RightId eq static meet. Global Declare Instance lft_ctx_persistent : Persistent lft_ctx. Global Declare Instance lft_dead_persistent κ : Persistent ([†κ]). diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v index ede0dc16..f2acef14 100644 --- a/theories/lifetime/model/definitions.v +++ b/theories/lifetime/model/definitions.v @@ -17,9 +17,7 @@ Module Export lft_notation. End lft_notation. Definition static : lft := (∅ : gmultiset _). -Definition lft_intersect (κ κ' : lft) : lft := κ ⊎ κ'. - -Infix "⊓" := lft_intersect (at level 40) : stdpp_scope. +Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'. Inductive bor_state := | Bor_in diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v index 377a8108..e3ab4f51 100644 --- a/theories/lifetime/model/primitive.v +++ b/theories/lifetime/model/primitive.v @@ -256,12 +256,12 @@ Qed. (** Basic rules about lifetimes *) Instance lft_inhabited : Inhabited lft := _. Instance bor_idx_inhabited : Inhabited bor_idx := _. -Instance lft_intersect_comm : Comm eq lft_intersect := _. -Instance lft_intersect_assoc : Assoc eq lft_intersect := _. -Instance lft_intersect_inj_1 κ : Inj eq eq (lft_intersect κ) := _. -Instance lft_intersect_inj_2 κ : Inj eq eq (λ κ', lft_intersect κ' κ) := _. -Instance lft_intersect_left_id : LeftId eq static lft_intersect := _. -Instance lft_intersect_right_id : RightId eq static lft_intersect := _. +Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _. +Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _. +Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓) := _. +Instance lft_intersect_inj_2 κ : Inj eq eq (⊓ κ) := _. +Instance lft_intersect_left_id : LeftId eq static (⊓) := _. +Instance lft_intersect_right_id : RightId eq static (⊓) := _. Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2]. Proof. by rewrite /lft_tok -big_sepMS_disj_union. Qed. @@ -269,7 +269,7 @@ Proof. by rewrite /lft_tok -big_sepMS_disj_union. Qed. Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ⊓ κ2]. Proof. rewrite /lft_dead -or_exist. apply exist_proper=> Λ. - rewrite -sep_or_r -pure_or. do 2 f_equiv. unfold lft_intersect. set_solver. + rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver. Qed. Lemma lft_tok_dead q κ : q.[κ] -∗ [† κ] -∗ False. diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v index 89829f2e..28fa316e 100644 --- a/theories/typing/lft_contexts.v +++ b/theories/typing/lft_contexts.v @@ -51,7 +51,7 @@ Section lft_contexts. - iDestruct "H" as "[Hq Hq']". iDestruct "Hq" as (κ0) "(% & Hq & #?)". iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *. - rewrite (inj (lft_intersect (foldr lft_intersect static κs)) κ0' κ0); last congruence. + rewrite (inj ((lft_intersect_list κs) ⊓) κ0' κ0); last congruence. iExists κ0. by iFrame "∗%". Qed. @@ -229,8 +229,8 @@ Section lft_contexts. iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp. iDestruct (big_sepL_lookup_acc with "HL2") as "[Hκ Hclose]". done. iDestruct "Hκ" as (κ0) "(EQ & Htok & #Hend)". simpl. iDestruct "EQ" as %->. - iAssert (∃ q', q'.[foldr lft_intersect static κs] ∗ - (q'.[foldr lft_intersect static κs] ={F}=∗ llctx_interp L (qL / 2)))%I + iAssert (∃ q', q'.[lft_intersect_list κs] ∗ + (q'.[lft_intersect_list κs] ={F}=∗ llctx_interp L (qL / 2)))%I with "[> HE HL1]" as "H". { move:(qL/2)%Qp=>qL'. clear HL. iClear "Hend". iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qL'). -- GitLab