From 588b95597988f0b55be24e96b2c67269c260fb73 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sun, 20 Nov 2016 13:04:30 +0100 Subject: [PATCH] Minimal elements in a set. --- prelude/collections.v | 31 +++++++++++++++++++++++++++++++ prelude/fin_collections.v | 21 +++++++++++++++++++++ 2 files changed, 52 insertions(+) diff --git a/prelude/collections.v b/prelude/collections.v index 15920610..08f289b4 100644 --- a/prelude/collections.v +++ b/prelude/collections.v @@ -993,3 +993,34 @@ Section seq_set. seq_set start (S len) = {[ start + len ]} ∪ seq_set start len. Proof. unfold_leibniz. apply seq_set_S_union. Qed. End seq_set. + +(** Mimimal elements *) +Definition minimal `{ElemOf A C} (R : relation A) (x : A) (X : C) : Prop := + ∀ y, y ∈ X → R y x → y = x. +Instance: Params (@minimal) 5. + +Section minimal. + Context `{SimpleCollection A C} {R : relation A}. + + Global Instance minimal_proper x : Proper (@equiv C _ ==> iff) (minimal R x). + Proof. intros X X' y; unfold minimal; set_solver. Qed. + Lemma empty_minimal x : minimal R x ∅. + Proof. unfold minimal; set_solver. Qed. + Lemma singleton_minimal x : minimal R x {[ x ]}. + Proof. unfold minimal; set_solver. Qed. + Lemma singleton_minimal_not_above y x : ¬R y x → minimal R x {[ y ]}. + Proof. unfold minimal; set_solver. Qed. + Lemma union_minimal X Y x : + minimal R x X → minimal R x Y → minimal R x (X ∪ Y). + Proof. unfold minimal; set_solver. Qed. + Lemma minimal_subseteq X Y x : minimal R x X → Y ⊆ X → minimal R x Y. + Proof. unfold minimal; set_solver. Qed. + + Lemma minimal_weaken `{!StrictOrder R} X x x' : + minimal R x X → R x' x → minimal R x' X. + Proof. + intros Hmin ? y ??. + assert (y = x) as -> by (apply (Hmin y); [done|by trans x']). + destruct (irreflexivity R x). by trans x'. + Qed. +End minimal. diff --git a/prelude/fin_collections.v b/prelude/fin_collections.v index 8b493835..237467b6 100644 --- a/prelude/fin_collections.v +++ b/prelude/fin_collections.v @@ -184,6 +184,27 @@ Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R} Proper ((≡) ==> R) (collection_fold f b : C → B). Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed. +Lemma minimal_exists `{!StrictOrder R, ∀ x y, Decision (R x y)} (X : C) : + X ≢ ∅ → ∃ x, x ∈ X ∧ minimal R x X. +Proof. + pattern X; apply collection_ind; clear X. + { by intros X X' HX; setoid_rewrite HX. } + { done. } + intros x X ? IH Hemp. destruct (collection_choose_or_empty X) as [[z ?]|HX]. + { destruct IH as (x' & Hx' & Hmin); [set_solver|]. + destruct (decide (R x x')). + - exists x; split; [set_solver|]. + eauto using union_minimal, singleton_minimal, minimal_weaken. + - exists x'; split; [set_solver|]. + auto using union_minimal, singleton_minimal_not_above. } + exists x; split; [set_solver|]. + rewrite HX, (right_id _ (∪)). apply singleton_minimal. +Qed. +Lemma minimal_exists_L + `{!LeibnizEquiv C, !StrictOrder R, ∀ x y, Decision (R x y)} (X : C) : + X ≠ ∅ → ∃ x, x ∈ X ∧ minimal R x X. +Proof. unfold_leibniz. apply minimal_exists. Qed. + (** * Decision procedures *) Global Instance set_Forall_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (set_Forall P X) | 100. -- GitLab