From 3a2bf991910971c4744b096ce062ac8b66c10ca9 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Wed, 29 Mar 2017 18:16:32 +0200
Subject: [PATCH] Add pick-any, pick-min, pick-max
---
util/all.v | 1 +
util/pick.v | 162 ++++++++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 163 insertions(+)
create mode 100644 util/pick.v
diff --git a/util/all.v b/util/all.v
index ce5d41b3f..267ef0e11 100644
--- a/util/all.v
+++ b/util/all.v
@@ -16,3 +16,4 @@ Require Export rt.util.sum.
Require Export rt.util.minmax.
Require Export rt.util.seqset.
Require Export rt.util.step_function.
+Require Export rt.util.pick.
\ No newline at end of file
diff --git a/util/pick.v b/util/pick.v
new file mode 100644
index 000000000..f8d98d57b
--- /dev/null
+++ b/util/pick.v
@@ -0,0 +1,162 @@
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype.
+
+(* In this file, we define functions for picking numbers in an interval [0, n). *)
+
+(** Auxiliary Functions *)
+
+Definition default0 {n} (x: option 'I_n) : nat := if x is Some y then y else 0.
+
+Definition arg_pred_nat n (P: pred 'I_n) ord :=
+ [pred i | P i & [forall j: 'I_n, P j ==> ord i j]].
+
+Definition pred_min_nat n (P: pred 'I_n) := arg_pred_nat n P leq.
+Definition pred_max_nat n (P: pred 'I_n) := arg_pred_nat n P (fun x y => geq x y).
+
+(** Defining Pick functions *)
+
+(* (pick_any n P) returns some number < n that satisfies P, or 0 if it cannot be found. *)
+Definition pick_any n (P: pred 'I_n) := default0 (pick P).
+
+(* (pick_min n P) returns the smallest number < n that satisfies P, or 0 if it cannot be found. *)
+Definition pick_min n (P: pred 'I_n) := default0 (pick (pred_min_nat n P)).
+
+(* (pick_max n P) returns the largest number < n that satisfies P, or 0 if it cannot be found. *)
+Definition pick_max n (P: pred 'I_n) := default0 (pick (pred_max_nat n P)).
+
+(** Improved notation *)
+
+(* Next we provide the following notation for the variations of pick:
+ [pick-any x <= N | P], [pick-any x < N | P]
+ [pick-min x <= N | P], [pick-min x < N | P]
+ [pick-max x <= N | P], [pick-max x < N | P]. *)
+Notation "[ 'pick-any' x <= N | P ]" :=
+ (pick_any N.+1 (fun x : 'I_N.+1 => P%B))
+ (at level 0, x ident, only parsing) : form_scope.
+
+Notation "[ 'pick-any' x < N | P ]" :=
+ (pick_any N (fun x : 'I_N => P%B))
+ (at level 0, x ident, only parsing) : form_scope.
+
+Notation "[ 'pick-min' x <= N | P ]" :=
+ (pick_min N.+1 (fun x : 'I_N.+1 => P%B))
+ (at level 0, x ident, only parsing) : form_scope.
+
+Notation "[ 'pick-min' x < N | P ]" :=
+ (pick_min N (fun x : 'I_N => P%B))
+ (at level 0, x ident, only parsing) : form_scope.
+
+Notation "[ 'pick-max' x <= N | P ]" :=
+ (pick_max N.+1 (fun x : 'I_N.+1 => P%B))
+ (at level 0, x ident, only parsing) : form_scope.
+
+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 *)
+
+(* 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.
+ Variable p: pred 'I_n.
+
+ Variable P: nat -> Prop.
+
+ Hypothesis EX: exists x:'I_n, p x.
+
+ Hypothesis HOLDS: forall x, p x -> P x.
+
+ Lemma pick_any_holds: P (pick_any n p).
+ Proof.
+ rewrite /pick_any /default0.
+ case: pickP; first by intros x PRED; apply HOLDS.
+ intros NONE; red in NONE; exfalso.
+ move: EX => [x PRED].
+ by specialize (NONE x); rewrite PRED in NONE.
+ Qed.
+
+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. *)
+Section PickMin.
+
+ Variable n: nat.
+ Variable p: pred 'I_n.
+
+ Variable P: nat -> Prop.
+
+ Hypothesis EX: exists x:'I_n, p x.
+
+ Hypothesis MIN:
+ forall x,
+ p x ->
+ (forall y, p y -> x <= y) ->
+ P x.
+
+ 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. *)
+Section PickMax.
+
+ Variable n: nat.
+ Variable p: pred 'I_n.
+
+ Variable P: nat -> Prop.
+
+ Hypothesis EX: exists x:'I_n, p x.
+
+ Hypothesis MAX:
+ forall x,
+ p x ->
+ (forall y, p y -> x >= y) ->
+ P x.
+
+ 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
--
GitLab