Merge branch 'ci/lennard/lowerbound' into 'master'

Add lower bound lemma for finite sets

See merge request !562

CHANGELOG.md

@@ -15,7 +15,10 @@ API-breaking change is listed.
   overview. This follows https://github.com/coq/coq/pull/18564.
 - Redefine `map_imap` so its closure argument can contain recursive
   occurrences of a `Fixpoint`.
-* Add lemma `fmap_insert_inv`.
+- Add lemma `fmap_insert_inv`.
+- Rename `minimal_exists` to `minimal_exists_elem_of` and
+  `minimal_exists_L` to `minimal_exists_elem_of_L`.
+  Add new `minimal_exists` lemma. (by Lennard Gäher)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -64,6 +67,9 @@ s/\bfresh_list_length\b/length_fresh_list/g
 s/\bbv_to_little_endian_length\b/length_bv_to_little_endian/g
 s/\bbv_seq_length\b/length_bv_seq/g
 s/\bbv_to_bits_length\b/length_bv_to_bits/g
+# renaming of minimal_exists
+s/\bminimal_exists_L\b/minimal_exists_elem_of_L/g
+s/\bminimal_exists\b/minimal_exists_elem_of/g
 EOF
 ```
 

stdpp/fin_sets.v

@@ -345,7 +345,7 @@ Lemma set_fold_comm_acc {B} (f : A → B → B) (g : B → B) (b : B) X :
 Proof. intros. apply (set_fold_comm_acc_strong _); [solve_proper|auto]. Qed.
 
 (** * Minimal elements *)
-Lemma minimal_exists R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) :
+Lemma minimal_exists_elem_of R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) :
   X ≢ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
 Proof.
   pattern X; apply set_ind; clear X.
@@ -361,10 +361,20 @@ Proof.
   exists x; split; [set_solver|].
   rewrite HX, (right_id _ (∪)). apply singleton_minimal.
 Qed.
-Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
+Lemma minimal_exists_elem_of_L R `{!LeibnizEquiv C, !Transitive R,
     ∀ x y, Decision (R x y)} (X : C) :
   X ≠ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
-Proof. unfold_leibniz. apply (minimal_exists R). Qed.
+Proof. unfold_leibniz. apply (minimal_exists_elem_of R). Qed.
+
+Lemma minimal_exists 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_elem_of R X) as (x & Hel & Hmin); first set_solver.
+    exists x. done.
+  - exists inhabitant. intros y Hel. set_solver.
+Qed.
 
 (** * Filter *)
 Lemma elem_of_filter (P : A → Prop) `{!∀ x, Decision (P x)} X x :