Add lemmas used by RefinedRust

lifetime/lifetime_sig.v

@@ -107,6 +107,7 @@ Module Type lifetime_sig.
   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_tok_valid : ∀ q κ, q.[κ] -∗ ⌜(q ≤ 1)%Qp⌝ ∨ ⌜κ = static⌝.
   Parameter lft_dead_static : [† static] -∗ False.
   Parameter lft_intersect_static_cancel_l : ∀ κ κ', κ ⊓ κ' = static → κ = static.
 
@@ -117,6 +118,13 @@ Module Type lifetime_sig.
     lft_ctx ={E}=∗
     ∃ p : positive, let κ := positive_to_lft p in ⌜P p⌝ ∗
          (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
+  (** Given two lifetimes [κ] and [κ'], find a lower bound on atomic lifetimes [m]
+     such that [m ⊓ κ'] is syntactically different from [κ].
+     This is useful in conjunction with [lft_create_strong] to generate
+     fresh lifetimes when using lifetimes as keys to index into a map. *)
+  Parameter lft_fresh_strong : ∀ κ κ', ∃ i : positive,
+    ∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.
+
   Parameter bor_create : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
   Parameter bor_fake : ∀ E κ P,

lifetime/model/creation.v

@@ -184,4 +184,27 @@ Proof.
       eapply HK'', Hκ. rewrite elem_of_union. auto.
     + iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
 Qed.
+
+(* TODO: remove once stdpp!562 is merged *)
+Lemma lower_bound_exists `{FinSet A C} R `{!Transitive R,
+    ∀ x y, Decision (R x y)} `{!Inhabited A} (X : C) :
+  ∃ x, minimal R x X.
+Proof.
+  destruct (set_choose_or_empty X) as [ (y & Ha) | Hne].
+  - edestruct (minimal_exists R X) as (x & Hel & Hmin); first set_solver.
+    exists x. done.
+  - exists inhabitant. intros y Hel. set_solver.
+Qed.
+Lemma lft_fresh_strong κ κ' :
+  ∃ i : positive, ∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.
+Proof.
+  unfold meet, lft_intersect.
+  destruct (lower_bound_exists (flip Pos.le) (dom κ)) as (i & Ha).
+  exists (i + 1)%positive.
+  intros k Hik Heq. subst κ.
+  ospecialize (Ha k _ _); simpl in *; [ | lia..].
+  apply gmultiset_elem_of_dom.
+  apply gmultiset_elem_of_disj_union.
+  left. by apply gmultiset_elem_of_singleton.
+Qed.
 End creation.

lifetime/model/primitive.v

@@ -313,6 +313,17 @@ Proof.
   naive_solver.
 Qed.
 
+Lemma lft_tok_valid q κ : 
+  q.[κ] -∗ ⌜(q ≤ 1)%Qp⌝ ∨ ⌜κ = static⌝.
+Proof.
+  rewrite /lft_tok. 
+  destruct (decide (κ = static)) as [-> | Hneq]; first by eauto.
+  edestruct (gmultiset_choose _ Hneq) as (Λ & Hel).
+  iIntros "Hm". iPoseProof (big_sepMS_elem_of with "Hm") as "Hm"; first done.
+  iPoseProof (own_valid with "Hm") as "%Hv".
+  iLeft. iPureIntro. rewrite auth_frag_valid in Hv. apply singleton_valid in Hv. done.
+Qed.
+
 (* Fractional and AsFractional instances *)
 Global Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
 Proof.