diff --git a/util/pick.v b/util/pick.v index f8d98d57bec0c969af80eb746c7fbb9898890406..3cc3a0929681483d452087a3b431809df3c7c141 100644 --- a/util/pick.v +++ b/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