Add more lemmas about pick

util/pick.v

@@ -53,10 +53,8 @@ Notation "[ 'pick-max' x < N | P ]" :=
   (pick_max N (fun x : 'I_N => P%B))
   (at level 0, x ident, only parsing) : form_scope.
 
-(** Lemmas *)
+(** Lemmas about pick_any *)
 
-(* First, we show that any property P of (pick_any n p) can be proven by showing that
-   P holds for any number < n that satisfies p. *)
 Section PickAny.
 
   Variable n: nat.
@@ -68,6 +66,8 @@ Section PickAny.
 
   Hypothesis HOLDS: forall x, p x -> P x.
 
+  (* First, we show that any property P of (pick_any n p) can be proven by showing
+     that P holds for any number < n that satisfies p. *)
   Lemma pick_any_holds: P (pick_any n p).
   Proof.
     rewrite /pick_any /default0.
@@ -79,8 +79,7 @@ Section PickAny.
 
 End PickAny.
 
-(* Next, we show that any property P of (pick_min n p) can be proven by showing that
-   P holds for the smallest number < n that satisfies p. *)
+(** Lemmas about pick_min *)
 Section PickMin.
 
   Variable n: nat.
@@ -88,40 +87,73 @@ Section PickMin.
 
   Variable P: nat -> Prop.
 
+  (* Assume that there is some number < n that satisfies p. *)
   Hypothesis EX: exists x:'I_n, p x.
 
-  Hypothesis MIN:
-    forall x,
-      p x ->
-      (forall y, p y -> x <= y) ->
-      P x.
+  Section Bound.
+
+    (* First, we show that (pick_min n p) < n. *)
+    Lemma pick_min_ltn: pick_min n p < n.
+    Proof.
+      rewrite /pick_min /odflt /oapp.
+      case: pickP.
+      {
+        move => x /andP [PRED /forallP ALL].
+          by rewrite /default0.
+      }
+      {
+        intros NONE; red in NONE; exfalso.
+        move: EX => [x PRED]; clear EX.
+        set argmin := arg_min x p id.
+        specialize (NONE argmin).
+        suff ARGMIN: (pred_min_nat n p) argmin by rewrite ARGMIN in NONE.
+        rewrite /argmin; case: arg_minP; first by done.
+        intros y Py MINy.
+        apply/andP; split; first by done.
+        by apply/forallP; intros y0; apply/implyP; intros Py0; apply MINy.
+      }
+    Qed.
+
+  End Bound.
+
+  Section Minimum.
+    
+    Hypothesis MIN:
+      forall x,
+        p x ->
+        x < n ->
+        (forall y, p y -> x <= y) ->
+        P x.
+    
+    (* Next, we show that any property P of (pick_min n p) can be proven by showing
+       that P holds for the smallest number < n that satisfies p. *)
+    Lemma pick_min_holds: P (pick_min n p).
+    Proof.
+      rewrite /pick_min /odflt /oapp.
+      case: pickP.
+      {
+        move => x /andP [PRED /forallP ALL].
+        apply MIN; try (by done).
+          by intros y Py; specialize (ALL y); move: ALL => /implyP ALL; apply ALL.
+      }
+      {
+        intros NONE; red in NONE; exfalso.
+        move: EX => [x PRED]; clear EX.
+        set argmin := arg_min x p id.
+        specialize (NONE argmin).
+        suff ARGMIN: (pred_min_nat n p) argmin by rewrite ARGMIN in NONE.
+        rewrite /argmin; case: arg_minP; first by done.
+        intros y Py MINy.
+        apply/andP; split; first by done.
+          by apply/forallP; intros y0; apply/implyP; intros Py0; apply MINy.
+      }
+    Qed.
+
+  End Minimum.
   
-  Lemma pick_min_holds: P (pick_min n p).
-  Proof.
-    rewrite /pick_min /odflt /oapp.
-    case: pickP.
-    {
-      move => x /andP [PRED /forallP ALL].
-      apply MIN; first by done.
-      by intros y Py; specialize (ALL y); move: ALL => /implyP ALL; apply ALL.
-    }
-    {
-      intros NONE; red in NONE; exfalso.
-      move: EX => [x PRED]; clear EX.
-      set argmin := arg_min x p id.
-      specialize (NONE argmin).
-      suff ARGMIN: (pred_min_nat n p) argmin by rewrite ARGMIN in NONE.
-      rewrite /argmin; case: arg_minP; first by done.
-      intros y Py MINy.
-      apply/andP; split; first by done.
-      by apply/forallP; intros y0; apply/implyP; intros Py0; apply MINy.
-    }
-  Qed.
-
 End PickMin.
 
-(* Next, we show that any property P of (pick_max n p) can be proven by showing that
-   P holds for the largest number < n that satisfies p. *)
+(** Lemmas about pick_max *)
 Section PickMax.
 
   Variable n: nat.
@@ -129,34 +161,68 @@ Section PickMax.
 
   Variable P: nat -> Prop.
 
+  (* Assume that there is some number < n that satisfies p. *)
   Hypothesis EX: exists x:'I_n, p x.
 
-  Hypothesis MAX:
-    forall x,
-      p x ->
-      (forall y, p y -> x >= y) ->
-      P x.
+  Section Bound.
+    
+    (* First, we show that (pick_max n p) < n. *)
+    Lemma pick_max_ltn: pick_max n p < n.
+    Proof.
+      rewrite /pick_max /odflt /oapp.
+      case: pickP.
+      {
+        move => x /andP [PRED /forallP ALL].
+          by rewrite /default0.
+      }
+      {
+        intros NONE; red in NONE; exfalso.
+        move: EX => [x PRED]; clear EX.
+        set argmax := arg_max x p id.
+        specialize (NONE argmax).
+        suff ARGMAX: (pred_max_nat n p) argmax by rewrite ARGMAX in NONE.
+        rewrite /argmax; case: arg_maxP; first by done.
+        intros y Py MAXy.
+        apply/andP; split; first by done.
+          by apply/forallP; intros y0; apply/implyP; intros Py0; apply MAXy.
+      }
+    Qed.
+
+  End Bound.
+
+  Section Maximum.
+    
+    Hypothesis MAX:
+      forall x,
+        p x ->
+        x < n ->
+        (forall y, p y -> x >= y) ->
+        P x.
+    
+    (* Next, we show that any property P of (pick_max n p) can be proven by showing that
+       P holds for the largest number < n that satisfies p. *)
+    Lemma pick_max_holds: P (pick_max n p).
+    Proof.
+      rewrite /pick_max /odflt /oapp.
+      case: pickP.
+      {
+        move => x /andP [PRED /forallP ALL].
+        apply MAX; try (by done).
+          by intros y Py; specialize (ALL y); move: ALL => /implyP ALL; apply ALL.
+      }
+      {
+        intros NONE; red in NONE; exfalso.
+        move: EX => [x PRED]; clear EX.
+        set argmax := arg_max x p id.
+        specialize (NONE argmax).
+        suff ARGMAX: (pred_max_nat n p) argmax by rewrite ARGMAX in NONE.
+        rewrite /argmax; case: arg_maxP; first by done.
+        intros y Py MAXy.
+        apply/andP; split; first by done.
+          by apply/forallP; intros y0; apply/implyP; intros Py0; apply MAXy.
+      }
+    Qed.
+
+  End Maximum.
   
-  Lemma pick_max_holds: P (pick_max n p).
-  Proof.
-    rewrite /pick_max /odflt /oapp.
-    case: pickP.
-    {
-      move => x /andP [PRED /forallP ALL].
-      apply MAX; first by done.
-      by intros y Py; specialize (ALL y); move: ALL => /implyP ALL; apply ALL.
-    }
-    {
-      intros NONE; red in NONE; exfalso.
-      move: EX => [x PRED]; clear EX.
-      set argmax := arg_max x p id.
-      specialize (NONE argmax).
-      suff ARGMAX: (pred_max_nat n p) argmax by rewrite ARGMAX in NONE.
-      rewrite /argmax; case: arg_maxP; first by done.
-      intros y Py MAXy.
-      apply/andP; split; first by done.
-      by apply/forallP; intros y0; apply/implyP; intros Py0; apply MAXy.
-    }
-  Qed.
-
 End PickMax.
\ No newline at end of file