add 'syntactic' notion of lifetim inclusion and prove basic lemmas about it

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.

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]▷=∗ [†κ]).

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.