From 590f19bb5a9a8b74726771f82df5f65c0702b10b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Fri, 30 Aug 2024 16:22:38 +0200
Subject: [PATCH] adjust name + use new stdpp lemma
---
lifetime/lifetime_sig.v | 2 +-
lifetime/model/creation.v | 14 ++------------
2 files changed, 3 insertions(+), 13 deletions(-)
diff --git a/lifetime/lifetime_sig.v b/lifetime/lifetime_sig.v
index 241b2b4b..343976ac 100644
--- a/lifetime/lifetime_sig.v
+++ b/lifetime/lifetime_sig.v
@@ -122,7 +122,7 @@ Module Type lifetime_sig.
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,
+ Parameter lft_fresh : ∀ κ κ', ∃ i : positive,
∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.
Parameter bor_create : ∀ E κ P,
diff --git a/lifetime/model/creation.v b/lifetime/model/creation.v
index 46c32bbd..5eccf4b9 100644
--- a/lifetime/model/creation.v
+++ b/lifetime/model/creation.v
@@ -185,21 +185,11 @@ Proof.
+ 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 κ κ' :
+Lemma lft_fresh κ κ' :
∃ 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).
+ destruct (minimal_exists (flip Pos.le) (dom κ)) as (i & Ha).
exists (i + 1)%positive.
intros k Hik Heq. subst κ.
ospecialize (Ha k _ _); simpl in *; [ | lia..].
--
GitLab