From 66320c79091c6ef7c5b1851cc3ad309b45a80129 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 23 Nov 2016 11:22:45 +0100
Subject: [PATCH] Some tweaks to minimal.

---
 prelude/collections.v | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

diff --git a/prelude/collections.v b/prelude/collections.v
index 1ff1e7b1f..dbce93e3b 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -999,6 +999,7 @@ End seq_set.
 Definition minimal `{ElemOf A C} (R : relation A) (x : A) (X : C) : Prop :=
   ∀ y, y ∈ X → R y x → R x y.
 Instance: Params (@minimal) 5.
+Typeclasses Opaque minimal.
 
 Section minimal.
   Context `{SimpleCollection A C} {R : relation A}.
@@ -1006,18 +1007,19 @@ 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 :
+  Lemma minimal_anti_symm_1 `{!AntiSymm (=) R} X x y :
+    minimal R x X → y ∈ X → R y x → x = y.
+  Proof. intros Hmin ??. apply (anti_symm _); auto. 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 :
+  Proof. unfold minimal; naive_solver eauto using minimal_anti_symm_1. Qed.
+
+  Lemma minimal_strict_1 `{!StrictOrder R} X x y :
+    minimal R x X → y ∈ X → ¬R y x.
+  Proof. intros Hmin ??. destruct (irreflexivity R x); trans y; 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.
+  Proof. unfold minimal; split; [eauto using minimal_strict_1|naive_solver]. Qed.
 
   Lemma empty_minimal x : minimal R x ∅.
   Proof. unfold minimal; set_solver. Qed.
@@ -1034,7 +1036,6 @@ Section minimal.
   Lemma minimal_weaken `{!Transitive R} X x x' :
     minimal R x X → R x' x → minimal R x' X.
   Proof.
-    intros Hmin ? y ??. trans x; [done|].
-    by eapply (Hmin y), transitivity.
+    intros Hmin ? y ??. trans x; [done|]. by eapply (Hmin y), transitivity.
   Qed.
 End minimal.
-- 
GitLab