Commit 64cafa57 authored by Robbert Krebbers's avatar Robbert Krebbers

Minimal elements in a set.

parent b29200a2
......@@ -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.
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment