diff --git a/util/all.v b/util/all.v index ce5d41b3f61817ef7d9ba0ebf36c1d7eb897111f..267ef0e11fc4c47b0cbf075059946c21cecc370e 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 0000000000000000000000000000000000000000..f8d98d57bec0c969af80eb746c7fbb9898890406 --- /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