From 0ed31f277fdffbd5e970ea1404059aec2a486f9a Mon Sep 17 00:00:00 2001 From: Felipe Cerqueira Date: Fri, 25 Nov 2016 13:47:12 +0100 Subject: [PATCH] Add more lemmas about min/max --- util/minmax.v | 525 +++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 429 insertions(+), 96 deletions(-) diff --git a/util/minmax.v b/util/minmax.v index edef8fe..9541ed6 100644 --- a/util/minmax.v +++ b/util/minmax.v @@ -1,160 +1,493 @@ -Require Import rt.util.tactics rt.util.notation rt.util.sorting rt.util.nat. +Require Import rt.util.tactics rt.util.notation rt.util.sorting rt.util.nat rt.util.list. From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop. Section MinMaxSeq. - Section Arg. - - Context {T: eqType}. + Section ArgGeneric. - Variable F: T -> nat. + Context {T1 T2: eqType}. + + Variable rel: T2 -> T2 -> bool. + Variable F: T1 -> T2. - Fixpoint seq_argmax (F: T -> nat) (l: seq T) := + Fixpoint seq_argmin (l: seq T1) := if l is x :: l' then - if seq_argmax F l' is Some y then - if F x >= F y then Some x else Some y + if seq_argmin l' is Some y then + if rel (F x) (F y) then Some x else Some y else Some x else None. - Fixpoint seq_argmin (F: T -> nat) (l: seq T) := + Fixpoint seq_argmax (l: seq T1) := if l is x :: l' then - if seq_argmin F l' is Some y then - if F x <= F y then Some x else Some y + if seq_argmax l' is Some y then + if rel (F y) (F x) then Some x else Some y else Some x else None. - + Section Lemmas. - Lemma seq_max_exists: + Lemma seq_argmin_exists: forall l x, x \in l -> - seq_argmax F l != None. + seq_argmin l != None. Proof. induction l; first by done. intros x; rewrite in_cons. move => /orP [/eqP EQ | IN] /=; - first by subst; destruct (seq_argmax F l); first by case: ifP. - by destruct (seq_argmax F l); first by case: ifP. + first by subst; destruct (seq_argmin l); first by case: ifP. + by destruct (seq_argmin l); first by case: ifP. Qed. - Lemma mem_seq_max: + Lemma seq_argmin_in_seq: forall l x, - seq_argmax F l = Some x -> + seq_argmin l = Some x -> x \in l. Proof. induction l; simpl; first by done. intros x ARG. - destruct (seq_argmax F l); + destruct (seq_argmin l); last by case: ARG => EQ; subst; rewrite in_cons eq_refl. - destruct (F s <= F a); + destruct (rel (F a) (F s)); first by case: ARG => EQ; subst; rewrite in_cons eq_refl. case: ARG => EQ; subst. by rewrite in_cons; apply/orP; right; apply IHl. Qed. - Lemma seq_max_computes_max: - forall l x y, - seq_argmax F l = Some x -> - y \in l -> - F x >= F y. - Proof. - induction l; first by done. - intros x y EQmax IN; simpl in EQmax. - rewrite in_cons in IN. - move: IN => /orP [/eqP EQ | IN]. - { - subst. - destruct (seq_argmax F l) eqn:ARG; - last by case: EQmax => EQ; subst. - destruct (leqP (F s) (F a)) as [LE | GT]; - first by case: EQmax => EQ; subst. - apply leq_trans with (n := F s); first by apply ltnW. - apply IHl; first by done. - by apply mem_seq_max. - } - { - destruct (seq_argmax F l) eqn:ARG. - { - destruct (leqP (F s) (F a)) as [LE | GT]; - last by case: EQmax => EQ; subst; apply IHl. - case: EQmax => EQ; subst. - by apply: (leq_trans _ LE); apply IHl. - } - { - case: EQmax => EQ; subst. - by apply seq_max_exists in IN; rewrite ARG in IN. - } - } - Qed. - - Lemma seq_min_exists: + Lemma seq_argmax_exists: forall l x, x \in l -> - seq_argmin F l != None. + seq_argmax l != None. Proof. induction l; first by done. intros x; rewrite in_cons. move => /orP [/eqP EQ | IN] /=; - first by subst; destruct (seq_argmin F l); first by case: ifP. - by destruct (seq_argmin F l); first by case: ifP. + first by subst; destruct (seq_argmax l); first by case: ifP. + by destruct (seq_argmax l); first by case: ifP. Qed. - Lemma mem_seq_min: + Lemma seq_argmax_in_seq: forall l x, - seq_argmin F l = Some x -> + seq_argmax l = Some x -> x \in l. Proof. induction l; simpl; first by done. intros x ARG. - destruct (seq_argmin F l); + destruct (seq_argmax l); last by case: ARG => EQ; subst; rewrite in_cons eq_refl. - destruct (F s >= F a); + destruct (rel (F s) (F a)); first by case: ARG => EQ; subst; rewrite in_cons eq_refl. case: ARG => EQ; subst. by rewrite in_cons; apply/orP; right; apply IHl. Qed. + + Section TotalOrder. - Lemma seq_min_computes_min: - forall l x y, - seq_argmin F l = Some x -> - y \in l -> - F x <= F y. - Proof. - induction l; first by done. - intros x y EQmin IN; simpl in EQmin. - rewrite in_cons in IN. - move: IN => /orP [/eqP EQ | IN]. - { - subst; destruct (seq_argmin F l) eqn:ARG; - last by case: EQmin => EQ; subst. - destruct (ltnP (F s) (F a)) as [LT | GE]; - last by case: EQmin => EQ; subst. - apply leq_trans with (n := F s); last by apply ltnW. - apply IHl; first by done. - by apply mem_seq_min. - } - { - destruct (seq_argmin F l) eqn:ARG. + Hypothesis H_transitive: transitive rel. + + Variable l: seq T1. + Hypothesis H_total_over_list: + forall x y, + x \in l -> + y \in l -> + rel (F x) (F y) || rel (F y) (F x). + + Lemma seq_argmin_computes_min: + forall x y, + seq_argmin l = Some x -> + y \in l -> + rel (F x) (F y). + Proof. + rename H_transitive into TRANS, H_total_over_list into TOT, l into l'. + induction l'; first by done. + intros x y EQmin IN; simpl in EQmin. + rewrite in_cons in IN. + move: IN => /orP [/eqP EQ | IN]. { - destruct (ltnP (F s) (F a)) as [LT | GE]; - first by case: EQmin => EQ; subst; apply IHl. - case: EQmin => EQ; subst. - by apply: (leq_trans GE); apply IHl. + subst; destruct (seq_argmin l') eqn:ARG; last first. + { + case: EQmin => EQ; subst. + by exploit (TOT x x); try (by rewrite in_cons eq_refl); rewrite orbb. + } + { + destruct (rel (F a) (F s)) eqn:REL; case: EQmin => EQ; subst; + first by exploit (TOT x x); try (by rewrite in_cons eq_refl); rewrite orbb. + exploit (TOT a x). + - by rewrite in_cons eq_refl. + - by rewrite in_cons; apply/orP; right; apply seq_argmin_in_seq. + - by rewrite REL /=. + } } + { + destruct (seq_argmin l') eqn:ARG. + { + destruct (rel (F a) (F s)) eqn:REL; case: EQmin => EQ; subst; last first. + { + apply IHl'; [| by done | by done]. + by intros x0 y0 INx INy; apply TOT; rewrite in_cons; apply/orP; right. + } + { + apply TRANS with (y := F s); first by done. + apply IHl'; [| by done | by done]. + by intros x0 y0 INx INy; apply TOT; rewrite in_cons; apply/orP; right. + } + } + { + case: EQmin => EQ; subst. + by apply seq_argmin_exists in IN; rewrite ARG in IN. + } + } + Qed. + + Lemma seq_argmax_computes_max: + forall x y, + seq_argmax l = Some x -> + y \in l -> + rel (F y) (F x). + Proof. + rename H_transitive into TRANS, H_total_over_list into TOT, l into l'. + induction l'; first by done. + intros x y EQmin IN; simpl in EQmin. + rewrite in_cons in IN. + move: IN => /orP [/eqP EQ | IN]. { - case: EQmin => EQ; subst. - by apply seq_min_exists in IN; rewrite ARG in IN. + subst; destruct (seq_argmax l') eqn:ARG; last first. + { + case: EQmin => EQ; subst. + by exploit (TOT x x); try (by rewrite in_cons eq_refl); rewrite orbb. + } + { + destruct (rel (F s) (F a)) eqn:REL; case: EQmin => EQ; subst; + first by exploit (TOT x x); try (by rewrite in_cons eq_refl); rewrite orbb. + exploit (TOT a x). + - by rewrite in_cons eq_refl. + - by rewrite in_cons; apply/orP; right; apply seq_argmax_in_seq. + - by rewrite REL orbF. + } } - } + { + destruct (seq_argmax l') eqn:ARG. + { + destruct (rel (F s) (F a)) eqn:REL; case: EQmin => EQ; subst; last first. + { + apply IHl'; [| by done | by done]. + by intros x0 y0 INx INy; apply TOT; rewrite in_cons; apply/orP; right. + } + { + apply TRANS with (y := F s); last by done. + apply IHl'; [| by done | by done]. + by intros x0 y0 INx INy; apply TOT; rewrite in_cons; apply/orP; right. + } + } + { + case: EQmin => EQ; subst. + by apply seq_argmax_exists in IN; rewrite ARG in IN. + } + } + Qed. + + End TotalOrder. + + End Lemmas. + + End ArgGeneric. + + Section MinGeneric. + + Context {T: eqType}. + Variable rel: rel T. + + Definition seq_min := seq_argmin rel id. + Definition seq_max := seq_argmax rel id. + + Section Lemmas. + + Lemma seq_min_exists: + forall l x, + x \in l -> + seq_min l != None. + Proof. + by apply seq_argmin_exists. + Qed. + + Lemma seq_min_in_seq: + forall l x, + seq_min l = Some x -> + x \in l. + Proof. + by apply seq_argmin_in_seq. + Qed. + + Lemma seq_max_exists: + forall l x, + x \in l -> + seq_max l != None. + Proof. + by apply seq_argmax_exists. + Qed. + + Lemma seq_max_in_seq: + forall l x, + seq_max l = Some x -> + x \in l. + Proof. + by apply seq_argmax_in_seq. Qed. + Section TotalOrder. + + Hypothesis H_transitive: transitive rel. + + Variable l: seq T. + Hypothesis H_total_over_list: + forall x y, + x \in l -> + y \in l -> + rel x y || rel y x. + + Lemma seq_min_computes_min: + forall x y, + seq_min l = Some x -> + y \in l -> + rel x y. + Proof. + by apply seq_argmin_computes_min. + Qed. + + Lemma seq_max_computes_max: + forall x y, + seq_max l = Some x -> + y \in l -> + rel y x. + Proof. + by apply seq_argmax_computes_max. + Qed. + + End TotalOrder. + End Lemmas. - - End Arg. - - Definition seq_max := seq_argmax id. - Definition seq_min := seq_argmin id. + + End MinGeneric. + + Section ArgNat. + + Context {T: eqType}. + + Variable F: T -> nat. + + Definition seq_argmin_nat := seq_argmin leq F. + Definition seq_argmax_nat := seq_argmax leq F. + + Section Lemmas. + + Lemma seq_argmin_nat_exists: + forall l x, + x \in l -> + seq_argmin_nat l != None. + Proof. + by apply seq_argmin_exists. + Qed. + + Lemma seq_argmin_nat_in_seq: + forall l x, + seq_argmin_nat l = Some x -> + x \in l. + Proof. + by apply seq_argmin_in_seq. + Qed. + + Lemma seq_argmax_nat_exists: + forall l x, + x \in l -> + seq_argmax_nat l != None. + Proof. + by apply seq_argmax_exists. + Qed. + + Lemma seq_argmax_nat_in_seq: + forall l x, + seq_argmax_nat l = Some x -> + x \in l. + Proof. + by apply seq_argmax_in_seq. + Qed. + + Section TotalOrder. + + Lemma seq_argmin_nat_computes_min: + forall l x y, + seq_argmin_nat l = Some x -> + y \in l -> + F x <= F y. + Proof. + intros l x y SOME IN. + apply seq_argmin_computes_min with (l0 := l); try (by done). + - by intros x1 x2 x3; apply leq_trans. + - by intros x1 x2 IN1 IN2; apply leq_total. + Qed. + + Lemma seq_argmax_nat_computes_max: + forall l x y, + seq_argmax_nat l = Some x -> + y \in l -> + F x >= F y. + Proof. + intros l x y SOME IN. + apply seq_argmax_computes_max with (l0 := l); try (by done). + - by intros x1 x2 x3; apply leq_trans. + - by intros x1 x2 IN1 IN2; apply leq_total. + Qed. + + End TotalOrder. + + End Lemmas. + + End ArgNat. + Section MinNat. + + Definition seq_min_nat := seq_argmin leq id. + Definition seq_max_nat := seq_argmax leq id. + + Section Lemmas. + + Lemma seq_min_nat_exists: + forall l x, + x \in l -> + seq_min_nat l != None. + Proof. + by apply seq_argmin_exists. + Qed. + + Lemma seq_min_nat_in_seq: + forall l x, + seq_min_nat l = Some x -> + x \in l. + Proof. + by apply seq_argmin_in_seq. + Qed. + + Lemma seq_max_nat_exists: + forall l x, + x \in l -> + seq_max_nat l != None. + Proof. + by apply seq_argmax_exists. + Qed. + + Lemma seq_max_nat_in_seq: + forall l x, + seq_max_nat l = Some x -> + x \in l. + Proof. + by apply seq_argmax_in_seq. + Qed. + + Section TotalOrder. + + Lemma seq_min_nat_computes_min: + forall l x y, + seq_min_nat l = Some x -> + y \in l -> + x <= y. + Proof. + intros l x y SOME IN. + apply seq_min_computes_min with (l0 := l); try (by done). + - by intros x1 x2 x3; apply leq_trans. + - by intros x1 x2 IN1 IN2; apply leq_total. + Qed. + + Lemma seq_max_nat_computes_max: + forall l x y, + seq_max_nat l = Some x -> + y \in l -> + x >= y. + Proof. + intros l x y SOME IN. + apply seq_max_computes_max with (l0 := l); try (by done). + - by intros x1 x2 x3; apply leq_trans. + - by intros x1 x2 IN1 IN2; apply leq_total. + Qed. + + End TotalOrder. + + End Lemmas. + + End MinNat. + + Section NatRange. + + Definition values_between (a b: nat) := + filter (fun x => x >= a) (map (@nat_of_ord _) (enum 'I_b)). + + Lemma mem_values_between a b: + forall x, x \in values_between a b = (a <= x < b). + Proof. + intros x; rewrite mem_filter. + apply/idP/idP. + { + move => /andP [GE IN]. + move: IN => /mapP [x' IN] EQ; subst. + rewrite mem_enum in IN. + by apply/andP; split. + } + { + move => /andP [GE LT]. + rewrite GE andTb. + apply/mapP; exists (Ordinal LT); last by done. + by rewrite mem_enum. + } + Qed. + + Definition min_nat_cond P (a b: nat) := + seq_min_nat (filter P (values_between a b)). + + Definition max_nat_cond P (a b: nat) := + seq_max_nat (filter P (values_between a b)). + + Lemma min_nat_cond_in_seq: + forall P a b x, + min_nat_cond P a b = Some x -> + a <= x < b /\ P x. + Proof. + intros P a b x SOME. + apply seq_min_nat_in_seq in SOME. + rewrite mem_filter in SOME; move: SOME => /andP [Px LE]. + by split; first by rewrite mem_values_between in LE. + Qed. + + Lemma min_nat_cond_computes_min: + forall P a b x, + min_nat_cond P a b = Some x -> + (forall y, a <= y < b -> P y -> x <= y). + Proof. + intros P a b x SOME y LE Py. + apply seq_min_nat_computes_min with (y := y) in SOME; first by done. + by rewrite mem_filter Py andTb mem_values_between. + Qed. + + Lemma max_nat_cond_in_seq: + forall P a b x, + max_nat_cond P a b = Some x -> + a <= x < b /\ P x. + Proof. + intros P a b x SOME. + apply seq_max_nat_in_seq in SOME. + rewrite mem_filter in SOME; move: SOME => /andP [Px LE]. + by split; first by rewrite mem_values_between in LE. + Qed. + + Lemma max_nat_cond_computes_max: + forall P a b x, + max_nat_cond P a b = Some x -> + (forall y, a <= y < b -> P y -> y <= x). + Proof. + intros P a b x SOME y LE Py. + apply seq_max_nat_computes_max with (y := y) in SOME; first by done. + by rewrite mem_filter Py andTb mem_values_between. + Qed. + + End NatRange. + End MinMaxSeq. (* Additional lemmas about max. *) -- GitLab