diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v index ae9358d09961adbdba739339d0fdbd81e81a6dfc..6002b01a9439931f999c3ff1188b647fadc480bf 100644 --- a/theories/lifetime/lifetime.v +++ b/theories/lifetime/lifetime.v @@ -22,6 +22,9 @@ Instance lft_inhabited : Inhabited lft := populate static. Canonical lftO := leibnizO lft. +Definition lft_incl_syntactic (κ κ' : lft) : Prop := ∃ κ'', κ'' ⊓ κ' = κ. +Infix "⊑ˢʸⁿ" := lft_incl_syntactic (at level 40) : stdpp_scope. + Section derived. Context `{!invG Σ, !lftG Σ}. Implicit Types κ : lft. @@ -223,4 +226,62 @@ Proof. iDestruct (lft_tok_dead with "Hκ H†") as "[]". Qed. +(** Syntactic lifetime inclusion *) +Lemma lft_incl_syn_sem κ κ' : + κ ⊑ˢʸⁿ κ' → ⊢ κ ⊑ κ'. +Proof. intros [z Hxy]. rewrite -Hxy. by apply lft_intersect_incl_r. Qed. + +Lemma lft_intersect_incl_syn_l κ κ' : κ ⊓ κ' ⊑ˢʸⁿ κ. +Proof. by exists κ'; rewrite (comm _ κ κ'). Qed. + +Lemma lft_intersect_incl_syn_r κ κ' : κ ⊓ κ' ⊑ˢʸⁿ κ'. +Proof. by exists κ. Qed. + +Lemma lft_incl_syn_refl κ : κ ⊑ˢʸⁿ κ. +Proof. exists static; by rewrite left_id. Qed. + +Lemma lft_incl_syn_trans κ κ' κ'' : + κ ⊑ˢʸⁿ κ' → κ' ⊑ˢʸⁿ κ'' → κ ⊑ˢʸⁿ κ''. +Proof. + intros [κ0 Hκ0] [κ'0 Hκ'0]. + rewrite -Hκ0 -Hκ'0 assoc. + by apply lft_intersect_incl_syn_r. +Qed. + +Lemma lft_intersect_mono_syn κ1 κ1' κ2 κ2' : + κ1 ⊑ˢʸⁿ κ1' → κ2 ⊑ˢʸⁿ κ2' → (κ1 ⊓ κ2) ⊑ˢʸⁿ (κ1' ⊓ κ2'). +Proof. + intros [κ1'' Hκ1] [κ2'' Hκ2]. + exists (κ1'' ⊓ κ2''). + rewrite -!assoc (comm _ κ2'' _). + rewrite -assoc assoc (comm _ κ2' _). + by f_equal. +Qed. + +Lemma lft_incl_syn_static κ : κ ⊑ˢʸⁿ static. +Proof. + exists κ; by apply lft_intersect_right_id. +Qed. + +Lemma lft_intersect_list_elem_of_incl_syn κs κ : + κ ∈ κs → lft_intersect_list κs ⊑ˢʸⁿ κ. +Proof. + induction 1 as [κ|κ κ' κs Hin IH]. + - apply lft_intersect_incl_syn_l. + - eapply lft_incl_syn_trans; last done. + apply lft_intersect_incl_syn_r. +Qed. + +Global Instance lft_incl_syn_anti_symm : AntiSymm eq (λ x y, x ⊑ˢʸⁿ y). +Proof. + intros κ1 κ2 [κ12 Hκ12] [κ21 Hκ21]. + assert (κ21 = static) as Hstatic. + { apply (lft_intersect_static_cancel_l _ κ12). + eapply (inj (κ1 ⊓.)). + rewrite assoc right_id. + eapply (inj (.⊓ κ2)). + rewrite (comm _ κ1 κ21) -assoc Hκ21 Hκ12 (comm _ κ2). done. } + by rewrite Hstatic left_id in Hκ21. +Qed. + End derived. diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v index e1607db0bf7f7248872aea468a20354222b9cc64..67597d1225df4a5cda2c44b0c73b66b3bf72513d 100644 --- a/theories/lifetime/lifetime_sig.v +++ b/theories/lifetime/lifetime_sig.v @@ -21,7 +21,7 @@ Module Type lifetime_sig. Global Notation lftPreG := lftPreG'. Existing Class lftPreG'. - (** Definitions *) + (** * Definitions *) Parameter lft : Type. Parameter static : lft. Declare Instance lft_intersect : Meet lft. @@ -38,7 +38,7 @@ Module Type lifetime_sig. Parameter idx_bor_own : ∀ `{!lftG Σ} (q : frac) (i : bor_idx), iProp Σ. Parameter idx_bor : ∀ `{!invG Σ, !lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ. - (** Notation *) + (** * Notation *) Notation "q .[ κ ]" := (lft_tok q κ) (format "q .[ κ ]", at level 0) : bi_scope. Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope. @@ -51,7 +51,7 @@ Module Type lifetime_sig. Section properties. Context `{!invG Σ, !lftG Σ}. - (** Instances *) + (** * Instances *) Global Declare Instance lft_inhabited : Inhabited lft. Global Declare Instance bor_idx_inhabited : Inhabited bor_idx. @@ -88,12 +88,13 @@ Module Type lifetime_sig. Global Declare Instance idx_bor_own_as_fractional i q : AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q. - (** Laws *) + (** * Laws *) Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2]. Parameter lft_dead_or : ∀ κ1 κ2, [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ⊓ κ2]. Parameter lft_tok_dead : ∀ q κ, q.[κ] -∗ [† κ] -∗ False. Parameter lft_tok_static : ∀ q, ⊢ q.[static]. Parameter lft_dead_static : [† static] -∗ False. + Parameter lft_intersect_static_cancel_l : ∀ κ κ', κ ⊓ κ' = static → κ = static. Parameter lft_create : ∀ E, ↑lftN ⊆ E → lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†κ]). diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v index 0f5673c48e5ff5a6dd8e72b10eba92e601945e94..bfe5b0c8f4fcafcabb78c633fe3209e31ed687e6 100644 --- a/theories/lifetime/model/primitive.v +++ b/theories/lifetime/model/primitive.v @@ -286,6 +286,13 @@ Proof. by rewrite /lft_tok big_sepMS_empty. Qed. Lemma lft_dead_static : [† static] -∗ False. Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed. +Lemma lft_intersect_static_cancel_l κ κ' : κ ⊓ κ' = static → κ = static. +Proof. + rewrite !gmultiset_eq=>Heq Λ. move:(Heq Λ). + rewrite multiplicity_disj_union multiplicity_empty Nat.eq_add_0. + naive_solver. +Qed. + (* Fractional and AsFractional instances *) Global Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I. Proof.