Commit 40e98b1b authored by Robbert Krebbers's avatar Robbert Krebbers

More generic definition of minimal that also for for anti-symmetric relations.

parent 32abe0c0
......@@ -996,7 +996,7 @@ 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.
y, y X R y x R x y.
Instance: Params (@minimal) 5.
Section minimal.
......@@ -1004,6 +1004,20 @@ Section minimal.
Global Instance minimal_proper x : Proper (@equiv C _ ==> iff) (minimal R x).
Proof. intros X X' y; unfold minimal; set_solver. Qed.
Lemma minimal_anti_symm `{!AntiSymm (=) R} x X :
minimal R x X y, y X R y x x = y.
Proof.
unfold minimal; split; [|naive_solver].
intros Hmin y ??. apply (anti_symm _); auto.
Qed.
Lemma minimal_strict `{!StrictOrder R} x X :
minimal R x X y, y X ¬R y x.
Proof.
unfold minimal; split; [|naive_solver].
intros Hmin y ??. destruct (irreflexivity R x); trans y; auto.
Qed.
Lemma empty_minimal x : minimal R x .
Proof. unfold minimal; set_solver. Qed.
Lemma singleton_minimal x : minimal R x {[ x ]}.
......@@ -1016,11 +1030,10 @@ Section minimal.
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' :
Lemma minimal_weaken `{!Transitive 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'.
intros Hmin ? y ??. trans x; [done|].
by eapply (Hmin y), transitivity.
Qed.
End minimal.
......@@ -189,7 +189,7 @@ Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
(** * Minimal elements *)
Lemma minimal_exists `{!StrictOrder R, x y, Decision (R x y)} (X : C) :
Lemma minimal_exists R `{!Transitive 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.
......@@ -205,10 +205,10 @@ Proof.
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) :
Lemma minimal_exists_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. Qed.
Proof. unfold_leibniz. apply (minimal_exists R). Qed.
(** * Filter *)
Lemma elem_of_filter (P : A Prop) `{! x, Decision (P x)} X x :
......
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