diff options
| -rw-r--r-- | theories/Arith/MinMax.v | 138 | ||||
| -rw-r--r-- | theories/NArith/Nminmax.v | 188 | ||||
| -rw-r--r-- | theories/NArith/Pminmax.v | 189 | ||||
| -rw-r--r-- | theories/QArith/Qminmax.v | 91 | ||||
| -rw-r--r-- | theories/Reals/Rminmax.v | 189 | ||||
| -rw-r--r-- | theories/Structures/GenericMinMax.v | 456 | ||||
| -rw-r--r-- | theories/ZArith/ZOdiv.v | 4 | ||||
| -rw-r--r-- | theories/ZArith/Zmax.v | 38 | ||||
| -rw-r--r-- | theories/ZArith/Zmin.v | 38 | ||||
| -rw-r--r-- | theories/ZArith/Zminmax.v | 236 |
10 files changed, 585 insertions, 982 deletions
diff --git a/theories/Arith/MinMax.v b/theories/Arith/MinMax.v index caf860af8..32afba489 100644 --- a/theories/Arith/MinMax.v +++ b/theories/Arith/MinMax.v @@ -26,138 +26,40 @@ Fixpoint min n m : nat := (** These functions implement indeed a maximum and a minimum *) -Lemma max_spec : forall x y, - (x<y /\ max x y = y) \/ (y<=x /\ max x y = x). +Lemma max_l : forall x y, y<=x -> max x y = x. Proof. induction x; destruct y; simpl; auto with arith. - destruct (IHx y); intuition. Qed. -Lemma min_spec : forall x y, - (x<y /\ min x y = x) \/ (y<=x /\ min x y = y). +Lemma max_r : forall x y, x<=y -> max x y = y. Proof. induction x; destruct y; simpl; auto with arith. - destruct (IHx y); intuition. Qed. -Module NatHasMinMax <: HasMinMax Nat_as_OT. - Definition max := max. - Definition min := min. - Definition max_spec := max_spec. - Definition min_spec := min_spec. -End NatHasMinMax. - -(** We obtain hence all the generic properties of max and min. *) - -Module Import NatMinMaxProps := MinMaxProperties Nat_as_OT NatHasMinMax. - -(** For some generic properties, we can have nicer statements here, - since underlying equality is Leibniz. *) - -Lemma max_case_strong : forall n m (P:nat -> Type), - (m<=n -> P n) -> (n<=m -> P m) -> P (max n m). -Proof. intros; apply max_case_strong; auto. congruence. Defined. - -Lemma max_case : forall n m (P:nat -> Type), - P n -> P m -> P (max n m). -Proof. intros. apply max_case_strong; auto. Defined. - -Lemma max_monotone: forall f, - (Proper (le ==> le) f) -> - forall x y, max (f x) (f y) = f (max x y). -Proof. intros; apply max_monotone; auto. congruence. Qed. - -Lemma min_case_strong : forall n m (P:nat -> Type), - (n<=m -> P n) -> (m<=n -> P m) -> P (min n m). -Proof. intros; apply min_case_strong; auto. congruence. Defined. - -Lemma min_case : forall n m (P:nat -> Type), - P n -> P m -> P (min n m). -Proof. intros. apply min_case_strong; auto. Defined. - -Lemma min_monotone: forall f, - (Proper (le ==> le) f) -> - forall x y, min (f x) (f y) = f (min x y). -Proof. intros; apply min_monotone; auto. congruence. Qed. - -Lemma max_min_antimonotone : forall f, - Proper (le==>ge) f -> - forall x y, max (f x) (f y) == f (min x y). +Lemma min_l : forall x y, x<=y -> min x y = x. Proof. - intros. apply max_min_antimonotone. congruence. - intros z z' Hz; red; unfold ge in *; auto. + induction x; destruct y; simpl; auto with arith. Qed. -Lemma min_max_antimonotone : forall f, - Proper (le==>ge) f -> - forall x y, min (f x) (f y) == f (max x y). +Lemma min_r : forall x y, y<=x -> min x y = y. Proof. - intros. apply min_max_antimonotone. congruence. - intros z z' Hz; red; unfold ge in *; auto. + induction x; destruct y; simpl; auto with arith. Qed. -(** For the other generic properties, we make aliases, - since otherwise SearchAbout misses some of them - (bad interaction with an Include). - See GenericMinMax (or SearchAbout) for the statements. *) - -Definition max_spec_le := max_spec_le. -Definition max_dec := max_dec. -Definition max_unicity := max_unicity. -Definition max_unicity_ext := max_unicity_ext. -Definition max_id := max_id. -Notation max_idempotent := max_id (only parsing). -Definition max_assoc := max_assoc. -Definition max_comm := max_comm. -Definition max_l := max_l. -Definition max_r := max_r. -Definition le_max_l := le_max_l. -Definition le_max_r := le_max_r. -Definition max_le := max_le. -Definition max_le_iff := max_le_iff. -Definition max_lt_iff := max_lt_iff. -Definition max_lub_l := max_lub_l. -Definition max_lub_r := max_lub_r. -Definition max_lub := max_lub. -Definition max_lub_iff := max_lub_iff. -Definition max_lub_lt := max_lub_lt. -Definition max_lub_lt_iff := max_lub_lt_iff. -Definition max_le_compat_l := max_le_compat_l. -Definition max_le_compat_r := max_le_compat_r. -Definition max_le_compat := max_le_compat. - -Definition min_spec_le := min_spec_le. -Definition min_dec := min_dec. -Definition min_unicity := min_unicity. -Definition min_unicity_ext := min_unicity_ext. -Definition min_id := min_id. -Notation min_idempotent := min_id (only parsing). -Definition min_assoc := min_assoc. -Definition min_comm := min_comm. -Definition min_l := min_l. -Definition min_r := min_r. -Definition le_min_l := le_min_l. -Definition le_min_r := le_min_r. -Definition min_le := min_le. -Definition min_le_iff := min_le_iff. -Definition min_lt_iff := min_lt_iff. -Definition min_glb_l := min_glb_l. -Definition min_glb_r := min_glb_r. -Definition min_glb := min_glb. -Definition min_glb_iff := min_glb_iff. -Definition min_glb_lt := min_glb_lt. -Definition min_glb_lt_iff := min_glb_lt_iff. -Definition min_le_compat_l := min_le_compat_l. -Definition min_le_compat_r := min_le_compat_r. -Definition min_le_compat := min_le_compat. - -Definition min_max_absorption := min_max_absorption. -Definition max_min_absorption := max_min_absorption. -Definition max_min_distr := max_min_distr. -Definition min_max_distr := min_max_distr. -Definition max_min_modular := max_min_modular. -Definition min_max_modular := min_max_modular. -Definition max_min_disassoc := max_min_disassoc. + +Module NatHasMinMax <: HasMinMax Nat_as_OT. + Definition max := max. + Definition min := min. + Definition max_l := max_l. + Definition max_r := max_r. + Definition min_l := min_l. + Definition min_r := min_r. +End NatHasMinMax. + +(** We obtain hence all the generic properties of [max] and [min], + see file [GenericMinMax] or use SearchAbout. *) + +Module Export MMP := UsualMinMaxProperties Nat_as_OT NatHasMinMax. (** * Properties specific to the [nat] domain *) diff --git a/theories/NArith/Nminmax.v b/theories/NArith/Nminmax.v index c2fee9c7e..625fcce23 100644 --- a/theories/NArith/Nminmax.v +++ b/theories/NArith/Nminmax.v @@ -15,212 +15,112 @@ Local Open Scope N_scope. (** The functions [Nmax] and [Nmin] implement indeed a maximum and a minimum *) -Lemma Nmax_spec : forall x y, - (x<y /\ Nmax x y = y) \/ (y<=x /\ Nmax x y = x). +Lemma Nmax_l : forall x y, y<=x -> Nmax x y = x. Proof. - unfold Nlt, Nle, Nmax. intros. - generalize (Ncompare_eq_correct x y). - rewrite <- (Ncompare_antisym x y). - destruct (x ?= y); simpl; auto; right; intuition; discriminate. + unfold Nle, Nmax. intros x y. + generalize (Ncompare_eq_correct x y). rewrite <- (Ncompare_antisym x y). + destruct (x ?= y); intuition. Qed. -Lemma Nmin_spec : forall x y, - (x<y /\ Nmin x y = x) \/ (y<=x /\ Nmin x y = y). +Lemma Nmax_r : forall x y, x<=y -> Nmax x y = y. Proof. - unfold Nlt, Nle, Nmin. intros. - generalize (Ncompare_eq_correct x y). - rewrite <- (Ncompare_antisym x y). - destruct (x ?= y); simpl; auto; right; intuition; discriminate. + unfold Nle, Nmax. intros x y. destruct (x ?= y); intuition. Qed. -Module NHasMinMax <: HasMinMax N_as_OT. - Definition max := Nmax. - Definition min := Nmin. - Definition max_spec := Nmax_spec. - Definition min_spec := Nmin_spec. -End NHasMinMax. - -(** We obtain hence all the generic properties of max and min. *) - -Module Import NMinMaxProps := MinMaxProperties N_as_OT NHasMinMax. - -(** For some generic properties, we can have nicer statements here, - since underlying equality is Leibniz. *) - -Lemma Nmax_case_strong : forall n m (P:N -> Type), - (m<=n -> P n) -> (n<=m -> P m) -> P (Nmax n m). -Proof. intros; apply max_case_strong; auto. congruence. Defined. - -Lemma Nmax_case : forall n m (P:N -> Type), - P n -> P m -> P (Nmax n m). -Proof. intros. apply Nmax_case_strong; auto. Defined. - -Lemma Nmax_monotone: forall f, - (Proper (Nle ==> Nle) f) -> - forall x y, Nmax (f x) (f y) = f (Nmax x y). -Proof. intros; apply max_monotone; auto. congruence. Qed. - -Lemma Nmin_case_strong : forall n m (P:N -> Type), - (n<=m -> P n) -> (m<=n -> P m) -> P (Nmin n m). -Proof. intros; apply min_case_strong; auto. congruence. Defined. - -Lemma Nmin_case : forall n m (P:N -> Type), - P n -> P m -> P (Nmin n m). -Proof. intros. apply Nmin_case_strong; auto. Defined. - -Lemma Nmin_monotone: forall f, - (Proper (Nle ==> Nle) f) -> - forall x y, Nmin (f x) (f y) = f (Nmin x y). -Proof. intros; apply min_monotone; auto. congruence. Qed. - -Lemma Nmax_min_antimonotone : forall f, - Proper (Nle==>Nge) f -> - forall x y, Nmax (f x) (f y) == f (Nmin x y). +Lemma Nmin_l : forall x y, x<=y -> Nmin x y = x. Proof. - intros f H. apply max_min_antimonotone. congruence. - intros x x' Hx. red. specialize (H _ _ Hx). clear Hx. - unfold Nle, Nge in *; contradict H. rewrite <- Ncompare_antisym, H; auto. + unfold Nle, Nmin. intros x y. destruct (x ?= y); intuition. Qed. -Lemma Nmin_max_antimonotone : forall f, - Proper (Nle==>Nge) f -> - forall x y, Nmin (f x) (f y) == f (Nmax x y). +Lemma Nmin_r : forall x y, y<=x -> Nmin x y = y. Proof. - intros f H. apply min_max_antimonotone. congruence. - intros z z' Hz; red. specialize (H _ _ Hz). clear Hz. - unfold Nle, Nge in *. contradict H. rewrite <- Ncompare_antisym, H; auto. + unfold Nle, Nmin. intros x y. + generalize (Ncompare_eq_correct x y). rewrite <- (Ncompare_antisym x y). + destruct (x ?= y); intuition. Qed. -(** For the other generic properties, we make aliases, - since otherwise SearchAbout misses some of them - (bad interaction with an Include). - See GenericMinMax (or SearchAbout) for the statements. *) - -Definition Nmax_spec_le := max_spec_le. -Definition Nmax_dec := max_dec. -Definition Nmax_unicity := max_unicity. -Definition Nmax_unicity_ext := max_unicity_ext. -Definition Nmax_id := max_id. -Notation Nmax_idempotent := Nmax_id (only parsing). -Definition Nmax_assoc := max_assoc. -Definition Nmax_comm := max_comm. -Definition Nmax_l := max_l. -Definition Nmax_r := max_r. -Definition Nle_max_l := le_max_l. -Definition Nle_max_r := le_max_r. -Definition Nmax_le := max_le. -Definition Nmax_le_iff := max_le_iff. -Definition Nmax_lt_iff := max_lt_iff. -Definition Nmax_lub_l := max_lub_l. -Definition Nmax_lub_r := max_lub_r. -Definition Nmax_lub := max_lub. -Definition Nmax_lub_iff := max_lub_iff. -Definition Nmax_lub_lt := max_lub_lt. -Definition Nmax_lub_lt_iff := max_lub_lt_iff. -Definition Nmax_le_compat_l := max_le_compat_l. -Definition Nmax_le_compat_r := max_le_compat_r. -Definition Nmax_le_compat := max_le_compat. - -Definition Nmin_spec_le := min_spec_le. -Definition Nmin_dec := min_dec. -Definition Nmin_unicity := min_unicity. -Definition Nmin_unicity_ext := min_unicity_ext. -Definition Nmin_id := min_id. -Notation Nmin_idempotent := Nmin_id (only parsing). -Definition Nmin_assoc := min_assoc. -Definition Nmin_comm := min_comm. -Definition Nmin_l := min_l. -Definition Nmin_r := min_r. -Definition Nle_min_l := le_min_l. -Definition Nle_min_r := le_min_r. -Definition Nmin_le := min_le. -Definition Nmin_le_iff := min_le_iff. -Definition Nmin_lt_iff := min_lt_iff. -Definition Nmin_glb_l := min_glb_l. -Definition Nmin_glb_r := min_glb_r. -Definition Nmin_glb := min_glb. -Definition Nmin_glb_iff := min_glb_iff. -Definition Nmin_glb_lt := min_glb_lt. -Definition Nmin_glb_lt_iff := min_glb_lt_iff. -Definition Nmin_le_compat_l := min_le_compat_l. -Definition Nmin_le_compat_r := min_le_compat_r. -Definition Nmin_le_compat := min_le_compat. - -Definition Nmin_max_absorption := min_max_absorption. -Definition Nmax_min_absorption := max_min_absorption. -Definition Nmax_min_distr := max_min_distr. -Definition Nmin_max_distr := min_max_distr. -Definition Nmax_min_modular := max_min_modular. -Definition Nmin_max_modular := min_max_modular. -Definition Nmax_min_disassoc := max_min_disassoc. +Module NHasMinMax <: HasMinMax N_as_OT. + Definition max := Nmax. + Definition min := Nmin. + Definition max_l := Nmax_l. + Definition max_r := Nmax_r. + Definition min_l := Nmin_l. + Definition min_r := Nmin_r. +End NHasMinMax. +Module N. +(** We obtain hence all the generic properties of max and min. *) + +Include UsualMinMaxProperties N_as_OT NHasMinMax. (** * Properties specific to the [positive] domain *) (** Simplifications *) -Lemma Nmax_0_l : forall n, Nmax 0 n = n. +Lemma max_0_l : forall n, Nmax 0 n = n. Proof. intros. unfold Nmax. rewrite <- Ncompare_antisym. generalize (Ncompare_0 n). destruct (n ?= 0); intuition. Qed. -Lemma Nmax_0_r : forall n, Nmax n 0 = n. -Proof. intros. rewrite max_comm. apply Nmax_0_l. Qed. +Lemma max_0_r : forall n, Nmax n 0 = n. +Proof. intros. rewrite N.max_comm. apply max_0_l. Qed. -Lemma Nmin_0_l : forall n, Nmin 0 n = 0. +Lemma min_0_l : forall n, Nmin 0 n = 0. Proof. intros. unfold Nmin. rewrite <- Ncompare_antisym. generalize (Ncompare_0 n). destruct (n ?= 0); intuition. Qed. -Lemma Nmin_0_r : forall n, Nmin n 0 = 0. -Proof. intros. rewrite min_comm. apply Nmin_0_l. Qed. +Lemma min_0_r : forall n, Nmin n 0 = 0. +Proof. intros. rewrite N.min_comm. apply min_0_l. Qed. (** Compatibilities (consequences of monotonicity) *) -Lemma Nsucc_max_distr : +Lemma succ_max_distr : forall n m, Nsucc (Nmax n m) = Nmax (Nsucc n) (Nsucc m). Proof. - intros. symmetry. apply Nmax_monotone. + intros. symmetry. apply max_monotone. intros x x'. unfold Nle. rewrite 2 nat_of_Ncompare, 2 nat_of_Nsucc. simpl; auto. Qed. -Lemma Nsucc_min_distr : forall n m, Nsucc (Nmin n m) = Nmin (Nsucc n) (Nsucc m). +Lemma succ_min_distr : forall n m, Nsucc (Nmin n m) = Nmin (Nsucc n) (Nsucc m). Proof. - intros. symmetry. apply Nmin_monotone. + intros. symmetry. apply min_monotone. intros x x'. unfold Nle. rewrite 2 nat_of_Ncompare, 2 nat_of_Nsucc. simpl; auto. Qed. -Lemma Nplus_max_distr_l : forall n m p, Nmax (p + n) (p + m) = p + Nmax n m. +Lemma plus_max_distr_l : forall n m p, Nmax (p + n) (p + m) = p + Nmax n m. Proof. - intros. apply Nmax_monotone. + intros. apply max_monotone. intros x x'. unfold Nle. rewrite 2 nat_of_Ncompare, 2 nat_of_Nplus. rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. Qed. -Lemma Nplus_max_distr_r : forall n m p, Nmax (n + p) (m + p) = Nmax n m + p. +Lemma plus_max_distr_r : forall n m p, Nmax (n + p) (m + p) = Nmax n m + p. Proof. intros. rewrite (Nplus_comm n p), (Nplus_comm m p), (Nplus_comm _ p). - apply Nplus_max_distr_l. + apply plus_max_distr_l. Qed. -Lemma Nplus_min_distr_l : forall n m p, Nmin (p + n) (p + m) = p + Nmin n m. +Lemma plus_min_distr_l : forall n m p, Nmin (p + n) (p + m) = p + Nmin n m. Proof. - intros. apply Nmin_monotone. + intros. apply min_monotone. intros x x'. unfold Nle. rewrite 2 nat_of_Ncompare, 2 nat_of_Nplus. rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. Qed. -Lemma Nplus_min_distr_r : forall n m p, Nmin (n + p) (m + p) = Nmin n m + p. +Lemma plus_min_distr_r : forall n m p, Nmin (n + p) (m + p) = Nmin n m + p. Proof. intros. rewrite (Nplus_comm n p), (Nplus_comm m p), (Nplus_comm _ p). - apply Nplus_min_distr_l. + apply plus_min_distr_l. Qed. + +End N.
\ No newline at end of file diff --git a/theories/NArith/Pminmax.v b/theories/NArith/Pminmax.v index afae63f5a..3b3c58841 100644 --- a/theories/NArith/Pminmax.v +++ b/theories/NArith/Pminmax.v @@ -15,211 +15,112 @@ Local Open Scope positive_scope. (** The functions [Pmax] and [Pmin] implement indeed a maximum and a minimum *) -Lemma Pmax_spec : forall x y, - (x<y /\ Pmax x y = y) \/ (y<=x /\ Pmax x y = x). +Lemma Pmax_l : forall x y, y<=x -> Pmax x y = x. Proof. - unfold Plt, Ple, Pmax. intros. - generalize (Pcompare_eq_iff x y). rewrite (ZC4 y x). - destruct ((x ?= y) Eq); simpl; auto; right; intuition; discriminate. + unfold Ple, Pmax. intros x y. + rewrite (ZC4 y x). generalize (Pcompare_eq_iff x y). + destruct ((x ?= y) Eq); intuition. Qed. -Lemma Pmin_spec : forall x y, - (x<y /\ Pmin x y = x) \/ (y<=x /\ Pmin x y = y). +Lemma Pmax_r : forall x y, x<=y -> Pmax x y = y. Proof. - unfold Plt, Ple, Pmin. intros. - generalize (Pcompare_eq_iff x y). rewrite (ZC4 y x). - destruct ((x ?= y) Eq); simpl; auto; right; intuition; discriminate. + unfold Ple, Pmax. intros x y. destruct ((x ?= y) Eq); intuition. Qed. -Module PositiveHasMinMax <: HasMinMax Positive_as_OT. - Definition max := Pmax. - Definition min := Pmin. - Definition max_spec := Pmax_spec. - Definition min_spec := Pmin_spec. -End PositiveHasMinMax. - -(** We obtain hence all the generic properties of max and min. *) - -Module Import NatMinMaxProps := - MinMaxProperties Positive_as_OT PositiveHasMinMax. - - -(** For some generic properties, we can have nicer statements here, - since underlying equality is Leibniz. *) - -Lemma Pmax_case_strong : forall n m (P:positive -> Type), - (m<=n -> P n) -> (n<=m -> P m) -> P (Pmax n m). -Proof. intros; apply max_case_strong; auto. congruence. Defined. - -Lemma Pmax_case : forall n m (P:positive -> Type), - P n -> P m -> P (Pmax n m). -Proof. intros. apply Pmax_case_strong; auto. Defined. - -Lemma Pmax_monotone: forall f, - (Proper (Ple ==> Ple) f) -> - forall x y, Pmax (f x) (f y) = f (Pmax x y). -Proof. intros; apply max_monotone; auto. congruence. Qed. - -Lemma Pmin_case_strong : forall n m (P:positive -> Type), - (n<=m -> P n) -> (m<=n -> P m) -> P (Pmin n m). -Proof. intros; apply min_case_strong; auto. congruence. Defined. - -Lemma Pmin_case : forall n m (P:positive -> Type), - P n -> P m -> P (Pmin n m). -Proof. intros. apply Pmin_case_strong; auto. Defined. - -Lemma Pmin_monotone: forall f, - (Proper (Ple ==> Ple) f) -> - forall x y, Pmin (f x) (f y) = f (Pmin x y). -Proof. intros; apply min_monotone; auto. congruence. Qed. - -Lemma Pmax_min_antimonotone : forall f, - Proper (Ple==>Pge) f -> - forall x y, Pmax (f x) (f y) == f (Pmin x y). +Lemma Pmin_l : forall x y, x<=y -> Pmin x y = x. Proof. - intros f H. apply max_min_antimonotone. congruence. - intros z z' Hz; red. specialize (H _ _ Hz). clear Hz. - unfold Ple, Pge in *. contradict H. rewrite ZC4, H; auto. + unfold Ple, Pmin. intros x y. destruct ((x ?= y) Eq); intuition. Qed. -Lemma Pmin_max_antimonotone : forall f, - Proper (Ple==>Pge) f -> - forall x y, Pmin (f x) (f y) == f (Pmax x y). +Lemma Pmin_r : forall x y, y<=x -> Pmin x y = y. Proof. - intros f H. apply min_max_antimonotone. congruence. - intros z z' Hz; red. specialize (H _ _ Hz). clear Hz. - unfold Ple, Pge in *. contradict H. rewrite ZC4, H; auto. + unfold Ple, Pmin. intros x y. + rewrite (ZC4 y x). generalize (Pcompare_eq_iff x y). + destruct ((x ?= y) Eq); intuition. Qed. -(** For the other generic properties, we make aliases, - since otherwise SearchAbout misses some of them - (bad interaction with an Include). - See GenericMinMax (or SearchAbout) for the statements. *) - -Definition Pmax_spec_le := max_spec_le. -Definition Pmax_dec := max_dec. -Definition Pmax_unicity := max_unicity. -Definition Pmax_unicity_ext := max_unicity_ext. -Definition Pmax_id := max_id. -Notation Pmax_idempotent := Pmax_id (only parsing). -Definition Pmax_assoc := max_assoc. -Definition Pmax_comm := max_comm. -Definition Pmax_l := max_l. -Definition Pmax_r := max_r. -Definition Ple_max_l := le_max_l. -Definition Ple_max_r := le_max_r. -Definition Pmax_le := max_le. -Definition Pmax_le_iff := max_le_iff. -Definition Pmax_lt_iff := max_lt_iff. -Definition Pmax_lub_l := max_lub_l. -Definition Pmax_lub_r := max_lub_r. -Definition Pmax_lub := max_lub. -Definition Pmax_lub_iff := max_lub_iff. -Definition Pmax_lub_lt := max_lub_lt. -Definition Pmax_lub_lt_iff := max_lub_lt_iff. -Definition Pmax_le_compat_l := max_le_compat_l. -Definition Pmax_le_compat_r := max_le_compat_r. -Definition Pmax_le_compat := max_le_compat. - -Definition Pmin_spec_le := min_spec_le. -Definition Pmin_dec := min_dec. -Definition Pmin_unicity := min_unicity. -Definition Pmin_unicity_ext := min_unicity_ext. -Definition Pmin_id := min_id. -Notation Pmin_idempotent := Pmin_id (only parsing). -Definition Pmin_assoc := min_assoc. -Definition Pmin_comm := min_comm. -Definition Pmin_l := min_l. -Definition Pmin_r := min_r. -Definition Ple_min_l := le_min_l. -Definition Ple_min_r := le_min_r. -Definition Pmin_le := min_le. -Definition Pmin_le_iff := min_le_iff. -Definition Pmin_lt_iff := min_lt_iff. -Definition Pmin_glb_l := min_glb_l. -Definition Pmin_glb_r := min_glb_r. -Definition Pmin_glb := min_glb. -Definition Pmin_glb_iff := min_glb_iff. -Definition Pmin_glb_lt := min_glb_lt. -Definition Pmin_glb_lt_iff := min_glb_lt_iff. -Definition Pmin_le_compat_l := min_le_compat_l. -Definition Pmin_le_compat_r := min_le_compat_r. -Definition Pmin_le_compat := min_le_compat. - -Definition Pmin_max_absorption := min_max_absorption. -Definition Pmax_min_absorption := max_min_absorption. -Definition Pmax_min_distr := max_min_distr. -Definition Pmin_max_distr := min_max_distr. -Definition Pmax_min_modular := max_min_modular. -Definition Pmin_max_modular := min_max_modular. -Definition Pmax_min_disassoc := max_min_disassoc. +Module PositiveHasMinMax <: HasMinMax Positive_as_OT. + Definition max := Pmax. + Definition min := Pmin. + Definition max_l := Pmax_l. + Definition max_r := Pmax_r. + Definition min_l := Pmin_l. + Definition min_r := Pmin_r. +End PositiveHasMinMax. + +Module P. +(** We obtain hence all the generic properties of max and min. *) + +Include UsualMinMaxProperties Positive_as_OT PositiveHasMinMax. (** * Properties specific to the [positive] domain *) (** Simplifications *) -Lemma Pmax_1_l : forall n, Pmax 1 n = n. +Lemma max_1_l : forall n, Pmax 1 n = n. Proof. intros. unfold Pmax. rewrite ZC4. generalize (Pcompare_1 n). destruct (n ?= 1); intuition. Qed. -Lemma Pmax_1_r : forall n, Pmax n 1 = n. -Proof. intros. rewrite max_comm. apply Pmax_1_l. Qed. +Lemma max_1_r : forall n, Pmax n 1 = n. +Proof. intros. rewrite P.max_comm. apply max_1_l. Qed. -Lemma Pmin_1_l : forall n, Pmin 1 n = 1. +Lemma min_1_l : forall n, Pmin 1 n = 1. Proof. intros. unfold Pmin. rewrite ZC4. generalize (Pcompare_1 n). destruct (n ?= 1); intuition. Qed. -Lemma Pmin_1_r : forall n, Pmin n 1 = 1. -Proof. intros. rewrite min_comm. apply Pmin_1_l. Qed. +Lemma min_1_r : forall n, Pmin n 1 = 1. +Proof. intros. rewrite P.min_comm. apply min_1_l. Qed. (** Compatibilities (consequences of monotonicity) *) -Lemma Psucc_max_distr : +Lemma succ_max_distr : forall n m, Psucc (Pmax n m) = Pmax (Psucc n) (Psucc m). Proof. - intros. symmetry. apply Pmax_monotone. + intros. symmetry. apply max_monotone. intros x x'. unfold Ple. rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism. simpl; auto. Qed. -Lemma Psucc_min_distr : forall n m, Psucc (Pmin n m) = Pmin (Psucc n) (Psucc m). +Lemma succ_min_distr : forall n m, Psucc (Pmin n m) = Pmin (Psucc n) (Psucc m). Proof. - intros. symmetry. apply Pmin_monotone. + intros. symmetry. apply min_monotone. intros x x'. unfold Ple. rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism. simpl; auto. Qed. -Lemma Pplus_max_distr_l : forall n m p, Pmax (p + n) (p + m) = p + Pmax n m. +Lemma plus_max_distr_l : forall n m p, Pmax (p + n) (p + m) = p + Pmax n m. Proof. - intros. apply Pmax_monotone. + intros. apply max_monotone. intros x x'. unfold Ple. rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism. rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. Qed. -Lemma Pplus_max_distr_r : forall n m p, Pmax (n + p) (m + p) = Pmax n m + p. +Lemma plus_max_distr_r : forall n m p, Pmax (n + p) (m + p) = Pmax n m + p. Proof. intros. rewrite (Pplus_comm n p), (Pplus_comm m p), (Pplus_comm _ p). - apply Pplus_max_distr_l. + apply plus_max_distr_l. Qed. -Lemma Pplus_min_distr_l : forall n m p, Pmin (p + n) (p + m) = p + Pmin n m. +Lemma plus_min_distr_l : forall n m p, Pmin (p + n) (p + m) = p + Pmin n m. Proof. - intros. apply Pmin_monotone. + intros. apply min_monotone. intros x x'. unfold Ple. rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism. rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. Qed. -Lemma Pplus_min_distr_r : forall n m p, Pmin (n + p) (m + p) = Pmin n m + p. +Lemma plus_min_distr_r : forall n m p, Pmin (n + p) (m + p) = Pmin n m + p. Proof. intros. rewrite (Pplus_comm n p), (Pplus_comm m p), (Pplus_comm _ p). - apply Pplus_min_distr_l. + apply plus_min_distr_l. Qed. + +End P.
\ No newline at end of file diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v index e9d2f79ab..ae9cc4605 100644 --- a/theories/QArith/Qminmax.v +++ b/theories/QArith/Qminmax.v @@ -25,106 +25,41 @@ Module QHasMinMax <: HasMinMax Q_as_OT. Definition min_spec := QMM.min_spec. End QHasMinMax. -(** We obtain hence all the generic properties of max and min. *) +Module Q. -Module Import QMinMaxProps := MinMaxProperties Q_as_OT QHasMinMax. - -Definition Qmax_case_strong := max_case_strong. -Definition Qmax_case := max_case. -Definition Qmax_monotone := max_monotone. -Definition Qmax_spec := max_spec. -Definition Qmax_spec_le := max_spec_le. -Definition Qmax_dec := max_dec. -Definition Qmax_unicity := max_unicity. -Definition Qmax_unicity_ext := max_unicity_ext. -Definition Qmax_id := max_id. -Notation Qmax_idempotent := Qmax_id (only parsing). -Definition Qmax_assoc := max_assoc. -Definition Qmax_comm := max_comm. -Definition Qmax_l := max_l. -Definition Qmax_r := max_r. -Definition Nle_max_l := le_max_l. -Definition Nle_max_r := le_max_r. -Definition Qmax_le := max_le. -Definition Qmax_le_iff := max_le_iff. -Definition Qmax_lt_iff := max_lt_iff. -Definition Qmax_lub_l := max_lub_l. -Definition Qmax_lub_r := max_lub_r. -Definition Qmax_lub := max_lub. -Definition Qmax_lub_iff := max_lub_iff. -Definition Qmax_lub_lt := max_lub_lt. -Definition Qmax_lub_lt_iff := max_lub_lt_iff. -Definition Qmax_le_compat_l := max_le_compat_l. -Definition Qmax_le_compat_r := max_le_compat_r. -Definition Qmax_le_compat := max_le_compat. - -Definition Qmin_case_strong := min_case_strong. -Definition Qmin_case := min_case. -Definition Qmin_monotone := min_monotone. -Definition Qmin_spec := min_spec. -Definition Qmin_spec_le := min_spec_le. -Definition Qmin_dec := min_dec. -Definition Qmin_unicity := min_unicity. -Definition Qmin_unicity_ext := min_unicity_ext. -Definition Qmin_id := min_id. -Notation Qmin_idempotent := Qmin_id (only parsing). -Definition Qmin_assoc := min_assoc. -Definition Qmin_comm := min_comm. -Definition Qmin_l := min_l. -Definition Qmin_r := min_r. -Definition Nle_min_l := le_min_l. -Definition Nle_min_r := le_min_r. -Definition Qmin_le := min_le. -Definition Qmin_le_iff := min_le_iff. -Definition Qmin_lt_iff := min_lt_iff. -Definition Qmin_glb_l := min_glb_l. -Definition Qmin_glb_r := min_glb_r. -Definition Qmin_glb := min_glb. -Definition Qmin_glb_iff := min_glb_iff. -Definition Qmin_glb_lt := min_glb_lt. -Definition Qmin_glb_lt_iff := min_glb_lt_iff. -Definition Qmin_le_compat_l := min_le_compat_l. -Definition Qmin_le_compat_r := min_le_compat_r. -Definition Qmin_le_compat := min_le_compat. - -Definition Qmin_max_absorption := min_max_absorption. -Definition Qmax_min_absorption := max_min_absorption. -Definition Qmax_min_distr := max_min_distr. -Definition Qmin_max_distr := min_max_distr. -Definition Qmax_min_modular := max_min_modular. -Definition Qmin_max_modular := min_max_modular. -Definition Qmax_min_disassoc := max_min_disassoc. -Definition Qmax_min_antimonotone := max_min_antimonotone. -Definition Qmin_max_antimonotone := min_max_antimonotone. +(** We obtain hence all the generic properties of max and min. *) +Include MinMaxProperties Q_as_OT QHasMinMax. (** * Properties specific to the [Q] domain *) (** Compatibilities (consequences of monotonicity) *) -Lemma Qplus_max_distr_l : forall n m p, Qmax (p + n) (p + m) == p + Qmax n m. +Lemma plus_max_distr_l : forall n m p, Qmax (p + n) (p + m) == p + Qmax n m. Proof. - intros. apply Qmax_monotone. + intros. apply max_monotone. intros x x' Hx; rewrite Hx; auto with qarith. intros x x' Hx. apply Qplus_le_compat; q_order. Qed. -Lemma Qplus_max_distr_r : forall n m p, Qmax (n + p) (m + p) == Qmax n m + p. +Lemma plus_max_distr_r : forall n m p, Qmax (n + p) (m + p) == Qmax n m + p. Proof. intros. rewrite (Qplus_comm n p), (Qplus_comm m p), (Qplus_comm _ p). - apply Qplus_max_distr_l. + apply plus_max_distr_l. Qed. -Lemma Qplus_min_distr_l : forall n m p, Qmin (p + n) (p + m) == p + Qmin n m. +Lemma plus_min_distr_l : forall n m p, Qmin (p + n) (p + m) == p + Qmin n m. Proof. - intros. apply Qmin_monotone. + intros. apply min_monotone. intros x x' Hx; rewrite Hx; auto with qarith. intros x x' Hx. apply Qplus_le_compat; q_order. Qed. -Lemma Qplus_min_distr_r : forall n m p, Qmin (n + p) (m + p) == Qmin n m + p. +Lemma plus_min_distr_r : forall n m p, Qmin (n + p) (m + p) == Qmin n m + p. Proof. intros. rewrite (Qplus_comm n p), (Qplus_comm m p), (Qplus_comm _ p). - apply Qplus_min_distr_l. + apply plus_min_distr_l. Qed. + +End Q.
\ No newline at end of file diff --git a/theories/Reals/Rminmax.v b/theories/Reals/Rminmax.v index e78e89542..79343ee45 100644 --- a/theories/Reals/Rminmax.v +++ b/theories/Reals/Rminmax.v @@ -15,200 +15,109 @@ Local Open Scope R_scope. (** The functions [Rmax] and [Rmin] implement indeed a maximum and a minimum *) -Lemma Rmax_spec : forall x y, - (x<y /\ Rmax x y = y) \/ (y<=x /\ Rmax x y = x). +Lemma Rmax_l : forall x y, y<=x -> Rmax x y = x. Proof. unfold Rmax. intros. - destruct Rle_dec as [H|H]; [| apply Rnot_le_lt in H ]; + destruct Rle_dec as [H'|H']; [| apply Rnot_le_lt in H' ]; unfold Rle in *; intuition. Qed. -Lemma Rmin_spec : forall x y, - (x<y /\ Rmin x y = x) \/ (y<=x /\ Rmin x y = y). +Lemma Rmax_r : forall x y, x<=y -> Rmax x y = y. +Proof. + unfold Rmax. intros. + destruct Rle_dec as [H'|H']; [| apply Rnot_le_lt in H' ]; + unfold Rle in *; intuition. +Qed. + +Lemma Rmin_l : forall x y, x<=y -> Rmin x y = x. +Proof. + unfold Rmin. intros. + destruct Rle_dec as [H'|H']; [| apply Rnot_le_lt in H' ]; + unfold Rle in *; intuition. +Qed. + +Lemma Rmin_r : forall x y, y<=x -> Rmin x y = y. Proof. unfold Rmin. intros. - destruct Rle_dec as [H|H]; [| apply Rnot_le_lt in H ]; + destruct Rle_dec as [H'|H']; [| apply Rnot_le_lt in H' ]; unfold Rle in *; intuition. Qed. Module RHasMinMax <: HasMinMax R_as_OT. Definition max := Rmax. Definition min := Rmin. - Definition max_spec := Rmax_spec. - Definition min_spec := Rmin_spec. + Definition max_l := Rmax_l. + Definition max_r := Rmax_r. + Definition min_l := Rmin_l. + Definition min_r := Rmin_r. End RHasMinMax. -(** We obtain hence all the generic properties of max and min. *) - -Module Import RMinMaxProps := MinMaxProperties R_as_OT RHasMinMax. - -(** For some generic properties, we can have nicer statements here, - since underlying equality is Leibniz. *) - -Lemma Rmax_case_strong : forall n m (P:R -> Type), - (m<=n -> P n) -> (n<=m -> P m) -> P (Rmax n m). -Proof. intros; apply max_case_strong; auto. congruence. Defined. +Module R. -Lemma Rmax_case : forall n m (P:R -> Type), - P n -> P m -> P (Rmax n m). -Proof. intros. apply Rmax_case_strong; auto. Defined. - -Lemma Rmax_monotone: forall f, - (Proper (Rle ==> Rle) f) -> - forall x y, Rmax (f x) (f y) = f (Rmax x y). -Proof. intros; apply max_monotone; auto. congruence. Qed. - -Lemma Rmin_case_strong : forall n m (P:R -> Type), - (n<=m -> P n) -> (m<=n -> P m) -> P (Rmin n m). -Proof. intros; apply min_case_strong; auto. congruence. Defined. - -Lemma Rmin_case : forall n m (P:R -> Type), - P n -> P m -> P (Rmin n m). -Proof. intros. apply Rmin_case_strong; auto. Defined. - -Lemma Rmin_monotone: forall f, - (Proper (Rle ==> Rle) f) -> - forall x y, Rmin (f x) (f y) = f (Rmin x y). -Proof. intros; apply min_monotone; auto. congruence. Qed. - -Lemma Rmax_min_antimonotone : forall f, - Proper (Rle==>Rge) f -> - forall x y, Rmax (f x) (f y) == f (Rmin x y). -Proof. - intros. apply max_min_antimonotone. congruence. - intros z z' Hz; red; apply Rge_le; auto. -Qed. - -Lemma Rmin_max_antimonotone : forall f, - Proper (Rle==>Rge) f -> - forall x y, Rmin (f x) (f y) == f (Rmax x y). -Proof. - intros. apply min_max_antimonotone. congruence. - intros z z' Hz; red. apply Rge_le. auto. -Qed. - -(** For the other generic properties, we make aliases, - since otherwise SearchAbout misses some of them - (bad interaction with an Include). - See GenericMinMax (or SearchAbout) for the statements. *) - -Definition Rmax_spec_le := max_spec_le. -Definition Rmax_dec := max_dec. -Definition Rmax_unicity := max_unicity. -Definition Rmax_unicity_ext := max_unicity_ext. -Definition Rmax_id := max_id. -Notation Rmax_idempotent := Rmax_id (only parsing). -Definition Rmax_assoc := max_assoc. -Definition Rmax_comm := max_comm. -Definition Rmax_l := max_l. -Definition Rmax_r := max_r. -Definition Zle_max_l := le_max_l. -Definition Zle_max_r := le_max_r. -Definition Rmax_le := max_le. -Definition Rmax_le_iff := max_le_iff. -Definition Rmax_lt_iff := max_lt_iff. -Definition Rmax_lub_l := max_lub_l. -Definition Rmax_lub_r := max_lub_r. -Definition Rmax_lub := max_lub. -Definition Rmax_lub_iff := max_lub_iff. -Definition Rmax_lub_lt := max_lub_lt. -Definition Rmax_lub_lt_iff := max_lub_lt_iff. -Definition Rmax_le_compat_l := max_le_compat_l. -Definition Rmax_le_compat_r := max_le_compat_r. -Definition Rmax_le_compat := max_le_compat. - -Definition Rmin_spec_le := min_spec_le. -Definition Rmin_dec := min_dec. -Definition Rmin_unicity := min_unicity. -Definition Rmin_unicity_ext := min_unicity_ext. -Definition Rmin_id := min_id. -Notation Rmin_idempotent := Rmin_id (only parsing). -Definition Rmin_assoc := min_assoc. -Definition Rmin_comm := min_comm. -Definition Rmin_l := min_l. -Definition Rmin_r := min_r. -Definition Zle_min_l := le_min_l. -Definition Zle_min_r := le_min_r. -Definition Rmin_le := min_le. -Definition Rmin_le_iff := min_le_iff. -Definition Rmin_lt_iff := min_lt_iff. -Definition Rmin_glb_l := min_glb_l. -Definition Rmin_glb_r := min_glb_r. -Definition Rmin_glb := min_glb. -Definition Rmin_glb_iff := min_glb_iff. -Definition Rmin_glb_lt := min_glb_lt. -Definition Rmin_glb_lt_iff := min_glb_lt_iff. -Definition Rmin_le_compat_l := min_le_compat_l. -Definition Rmin_le_compat_r := min_le_compat_r. -Definition Rmin_le_compat := min_le_compat. - -Definition Rmin_max_absorption := min_max_absorption. -Definition Rmax_min_absorption := max_min_absorption. -Definition Rmax_min_distr := max_min_distr. -Definition Rmin_max_distr := min_max_distr. -Definition Rmax_min_modular := max_min_modular. -Definition Rmin_max_modular := min_max_modular. -Definition Rmax_min_disassoc := max_min_disassoc. +(** We obtain hence all the generic properties of max and min. *) +Include UsualMinMaxProperties R_as_OT RHasMinMax. (** * Properties specific to the [R] domain *) (** Compatibilities (consequences of monotonicity) *) -Lemma Rplus_max_distr_l : forall n m p, Rmax (p + n) (p + m) = p + Rmax n m. +Lemma plus_max_distr_l : forall n m p, Rmax (p + n) (p + m) = p + Rmax n m. Proof. - intros. apply Rmax_monotone. + intros. apply max_monotone. intros x y. apply Rplus_le_compat_l. Qed. -Lemma Rplus_max_distr_r : forall n m p, Rmax (n + p) (m + p) = Rmax n m + p. +Lemma plus_max_distr_r : forall n m p, Rmax (n + p) (m + p) = Rmax n m + p. Proof. intros. rewrite (Rplus_comm n p), (Rplus_comm m p), (Rplus_comm _ p). - apply Rplus_max_distr_l. + apply plus_max_distr_l. Qed. -Lemma Rplus_min_distr_l : forall n m p, Rmin (p + n) (p + m) = p + Rmin n m. +Lemma plus_min_distr_l : forall n m p, Rmin (p + n) (p + m) = p + Rmin n m. Proof. - intros. apply Rmin_monotone. + intros. apply min_monotone. intros x y. apply Rplus_le_compat_l. Qed. -Lemma Rplus_min_distr_r : forall n m p, Rmin (n + p) (m + p) = Rmin n m + p. +Lemma plus_min_distr_r : forall n m p, Rmin (n + p) (m + p) = Rmin n m + p. Proof. intros. rewrite (Rplus_comm n p), (Rplus_comm m p), (Rplus_comm _ p). - apply Rplus_min_distr_l. + apply plus_min_distr_l. Qed. (** Anti-monotonicity swaps the role of [min] and [max] *) -Lemma Ropp_max_distr : forall n m : R, -(Rmax n m) = Rmin (- n) (- m). +Lemma opp_max_distr : forall n m : R, -(Rmax n m) = Rmin (- n) (- m). Proof. - intros. symmetry. apply Rmin_max_antimonotone. - exact Ropp_le_ge_contravar. + intros. symmetry. apply min_max_antimonotone. + do 3 red. intros; apply Rge_le. apply Ropp_le_ge_contravar; auto. Qed. -Lemma Ropp_min_distr : forall n m : R, - (Rmin n m) = Rmax (- n) (- m). +Lemma opp_min_distr : forall n m : R, - (Rmin n m) = Rmax (- n) (- m). Proof. - intros. symmetry. apply Rmax_min_antimonotone. - exact Ropp_le_ge_contravar. + intros. symmetry. apply max_min_antimonotone. + do 3 red. intros; apply Rge_le. apply Ropp_le_ge_contravar; auto. Qed. -Lemma Rminus_max_distr_l : forall n m p, Rmax (p - n) (p - m) = p - Rmin n m. +Lemma minus_max_distr_l : forall n m p, Rmax (p - n) (p - m) = p - Rmin n m. Proof. - unfold Rminus. intros. rewrite Ropp_min_distr. apply Rplus_max_distr_l. + unfold Rminus. intros. rewrite opp_min_distr. apply plus_max_distr_l. Qed. -Lemma Rminus_max_distr_r : forall n m p, Rmax (n - p) (m - p) = Rmax n m - p. +Lemma minus_max_distr_r : forall n m p, Rmax (n - p) (m - p) = Rmax n m - p. Proof. - unfold Rminus. intros. apply Rplus_max_distr_r. + unfold Rminus. intros. apply plus_max_distr_r. Qed. -Lemma Rminus_min_distr_l : forall n m p, Rmin (p - n) (p - m) = p - Rmax n m. +Lemma minus_min_distr_l : forall n m p, Rmin (p - n) (p - m) = p - Rmax n m. Proof. - unfold Rminus. intros. rewrite Ropp_max_distr. apply Rplus_min_distr_l. + unfold Rminus. intros. rewrite opp_max_distr. apply plus_min_distr_l. Qed. -Lemma Rminus_min_distr_r : forall n m p, Rmin (n - p) (m - p) = Rmin n m - p. +Lemma minus_min_distr_r : forall n m p, Rmin (n - p) (m - p) = Rmin n m - p. Proof. - unfold Rminus. intros. apply Rplus_min_distr_r. + unfold Rminus. intros. apply plus_min_distr_r. Qed. + +End R. diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index f5ff27888..f45e43b44 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -6,28 +6,25 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -Require Import OrderedType2 OrderedType2Facts Setoid Morphisms Basics. +Require Import OrderTac OrderedType2 OrderedType2Facts Setoid Morphisms Basics. -(** * A Generic construction of min and max based on OrderedType *) +(** * A Generic construction of min and max *) (** ** First, an interface for types with [max] and/or [min] *) -Module Type HasMax (Import O:OrderedTypeFull). +Module Type HasMax (Import E:EqLe'). Parameter Inline max : t -> t -> t. - Parameter max_spec : forall x y, - (lt x y /\ eq (max x y) y) \/ (le y x /\ eq (max x y) x). + Parameter max_l : forall x y, y<=x -> max x y == x. + Parameter max_r : forall x y, x<=y -> max x y == y. End HasMax. -Module Type HasMin (Import O:OrderedTypeFull). +Module Type HasMin (Import E:EqLe'). Parameter Inline min : t -> t -> t. - Parameter min_spec : forall x y, - (lt x y /\ eq (min x y) x) \/ (le y x /\ eq (min x y) y). + Parameter min_l : forall x y, x<=y -> min x y == x. + Parameter min_r : forall x y, y<=x -> min x y == y. End HasMin. -Module Type HasMinMax (Import O:OrderedTypeFull). - Include Type HasMax O. - Include Type HasMin O. -End HasMinMax. +Module Type HasMinMax (E:EqLe) := HasMax E <+ HasMin E. (** ** Any [OrderedTypeFull] can be equipped by [max] and [min] @@ -38,23 +35,42 @@ Definition gmax {A} (cmp : A->A->comparison) x y := Definition gmin {A} (cmp : A->A->comparison) x y := match cmp x y with Gt => y | _ => x end. -Module GenericMinMax (Import O:OrderedTypeFull) <: HasMinMax O. +Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O. Definition max := gmax O.compare. Definition min := gmin O.compare. - Lemma max_spec : forall x y, - (lt x y /\ eq (max x y) y) \/ (le y x /\ eq (max x y) x). + Lemma ge_not_lt : forall x y, y<=x -> x<y -> False. Proof. - intros. rewrite le_lteq. unfold max, gmax. - destruct (compare_spec x y); auto with relations. + intros x y H H'. + apply (StrictOrder_Irreflexive x). + rewrite le_lteq in *; destruct H as [H|H]. + transitivity y; auto. + rewrite H in H'; auto. Qed. - Lemma min_spec : forall x y, - (lt x y /\ eq (min x y) x) \/ (le y x /\ eq (min x y) y). + Lemma max_l : forall x y, y<=x -> max x y == x. Proof. - intros. rewrite le_lteq. unfold min, gmin. - destruct (compare_spec x y); auto with relations. + intros. unfold max, gmax. destruct (compare_spec x y); auto with relations. + elim (ge_not_lt x y); auto. + Qed. + + Lemma max_r : forall x y, x<=y -> max x y == y. + Proof. + intros. unfold max, gmax. destruct (compare_spec x y); auto with relations. + elim (ge_not_lt y x); auto. + Qed. + + Lemma min_l : forall x y, x<=y -> min x y == x. + Proof. + intros. unfold min, gmin. destruct (compare_spec x y); auto with relations. + elim (ge_not_lt y x); auto. + Qed. + + Lemma min_r : forall x y, y<=x -> min x y == y. + Proof. + intros. unfold min, gmin. destruct (compare_spec x y); auto with relations. + elim (ge_not_lt x y); auto. Qed. End GenericMinMax. @@ -62,26 +78,21 @@ End GenericMinMax. (** ** Consequences of the minimalist interface: facts about [max]. *) -Module MaxProperties (Import O:OrderedTypeFull)(Import M:HasMax O). - Module Import OF := OrderedTypeFullFacts O. - Infix "<" := lt. - Infix "==" := eq (at level 70). - Infix "<=" := le. - -Instance max_compat : Proper (eq==>eq==>eq) max. -Proof. -intros x x' Hx y y' Hy. -assert (H1 := max_spec x y). assert (H2 := max_spec x' y'). -set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'. -rewrite <- Hx, <- Hy in *. -destruct (compare_spec x y); intuition; order. -Qed. +Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O). + Module Import T := MakeOrderTac O. -(** An alias to the [max_spec] of the interface. *) +(** An alternative caracterisation of [max], equivalent to + [max_l /\ max_r] *) Lemma max_spec : forall n m, (n < m /\ max n m == m) \/ (m <= n /\ max n m == n). -Proof. exact max_spec. Qed. +Proof. + intros n m. + destruct (lt_total n m); [left|right]. + split; auto. apply max_r. rewrite le_lteq; auto. + assert (m <= n) by (rewrite le_lteq; intuition). + split; auto. apply max_l; auto. +Qed. (** A more symmetric version of [max_spec], based only on [le]. Beware that left and right alternatives overlap. *) @@ -92,13 +103,26 @@ Proof. intros. destruct (max_spec n m); [left|right]; intuition; order. Qed. -(** Another function satisfying the same specification is equal to [max]. *) +Instance : Proper (eq==>eq==>iff) le. +Proof. repeat red. intuition order. Qed. + +Instance max_compat : Proper (eq==>eq==>eq) max. +Proof. +intros x x' Hx y y' Hy. +assert (H1 := max_spec x y). assert (H2 := max_spec x' y'). +set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'. +rewrite <- Hx, <- Hy in *. +destruct (lt_total x y); intuition order. +Qed. + + +(** A function satisfying the same specification is equal to [max]. *) Lemma max_unicity : forall n m p, ((n < m /\ p == m) \/ (m <= n /\ p == n)) -> p == max n m. Proof. intros. assert (Hm := max_spec n m). - destruct (compare_spec n m); intuition; order. + destruct (lt_total n m); intuition; order. Qed. Lemma max_unicity_ext : forall f, @@ -108,45 +132,16 @@ Proof. intros. apply max_unicity; auto. Qed. -(** Induction principles for [max]. *) - -Lemma max_case_strong : forall n m (P:t -> Type), - (forall x y, x==y -> P x -> P y) -> - (m<=n -> P n) -> (n<=m -> P m) -> P (max n m). -Proof. -intros n m P Compat Hl Hr. -assert (H:=compare_spec n m). assert (H':=max_spec n m). -destruct (compare n m). -apply (Compat m), Hr; inversion_clear H; intuition; order. -apply (Compat m), Hr; inversion_clear H; intuition; order. -apply (Compat n), Hl; inversion_clear H; intuition; order. -Qed. - -Lemma max_case : forall n m (P:t -> Type), - (forall x y, x == y -> P x -> P y) -> - P n -> P m -> P (max n m). -Proof. - intros. apply max_case_strong; auto. -Defined. - -(** [max] returns one of its arguments. *) - -Lemma max_dec : forall n m, {max n m == n} + {max n m == m}. -Proof. - intros n m. apply max_case; auto with relations. - intros x y H [E|E]; [left|right]; order. -Defined. - (** [max] commutes with monotone functions. *) -Lemma max_monotone: forall f, +Lemma max_mono: forall f, (Proper (eq ==> eq) f) -> (Proper (le ==> le) f) -> forall x y, max (f x) (f y) == f (max x y). Proof. intros f Eqf Lef x y. - destruct (M.max_spec x y) as [(H,E)|(H,E)]; rewrite E; - destruct (M.max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. + destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E; + destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. assert (f x <= f y) by (apply Lef; order). order. assert (f y <= f x) by (apply Lef; order). order. Qed. @@ -155,101 +150,106 @@ Qed. Lemma max_id : forall n, max n n == n. Proof. - intros. destruct (M.max_spec n n); intuition. + intros. destruct (max_spec n n); intuition. Qed. +Notation max_idempotent := max_id (only parsing). + Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p. Proof. intros. - destruct (M.max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq. - destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. + destruct (max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq. + destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. destruct (max_spec m p); intuition; order. order. - destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. order. + destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. order. destruct (max_spec m p); intuition; order. Qed. Lemma max_comm : forall n m, max n m == max m n. Proof. intros. - destruct (M.max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq. - destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order. - destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order. + destruct (max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq. + destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order. + destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order. Qed. (** *** Least-upper bound properties of [max] *) -Lemma max_l : forall n m, m <= n -> max n m == n. +Definition max_l := max_l. +Definition max_r := max_r. + +Lemma le_max_l : forall n m, n <= max n m. Proof. - intros. destruct (M.max_spec n m); intuition; order. + intros; destruct (max_spec n m); intuition; order. Qed. -Lemma max_r : forall n m, n <= m -> max n m == m. +Lemma le_max_r : forall n m, m <= max n m. Proof. - intros. destruct (M.max_spec n m); intuition; order. + intros; destruct (max_spec n m); intuition; order. Qed. -Lemma le_max_l : forall n m, n <= max n m. +Lemma max_l_iff : forall n m, max n m == n <-> m <= n. Proof. - intros; destruct (M.max_spec n m); intuition; order. + split. intro H; rewrite <- H. apply le_max_r. apply max_l. Qed. -Lemma le_max_r : forall n m, m <= max n m. +Lemma max_r_iff : forall n m, max n m == m <-> n <= m. Proof. - intros; destruct (M.max_spec n m); intuition; order. + split. intro H; rewrite <- H. apply le_max_l. apply max_r. Qed. Lemma max_le : forall n m p, p <= max n m -> p <= n \/ p <= m. Proof. - intros n m p H; destruct (M.max_spec n m); + intros n m p H; destruct (max_spec n m); [right|left]; intuition; order. Qed. Lemma max_le_iff : forall n m p, p <= max n m <-> p <= n \/ p <= m. Proof. intros. split. apply max_le. - destruct (M.max_spec n m); intuition; order. + destruct (max_spec n m); intuition; order. Qed. Lemma max_lt_iff : forall n m p, p < max n m <-> p < n \/ p < m. Proof. - intros. destruct (M.max_spec n m); intuition; + intros. destruct (max_spec n m); intuition; order || (right; order) || (left; order). Qed. Lemma max_lub_l : forall n m p, max n m <= p -> n <= p. Proof. - intros; destruct (M.max_spec n m); intuition; order. + intros; destruct (max_spec n m); intuition; order. Qed. Lemma max_lub_r : forall n m p, max n m <= p -> m <= p. Proof. - intros; destruct (M.max_spec n m); intuition; order. + intros; destruct (max_spec n m); intuition; order. Qed. Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p. Proof. - intros; destruct (M.max_spec n m); intuition; order. + intros; destruct (max_spec n m); intuition; order. Qed. Lemma max_lub_iff : forall n m p, max n m <= p <-> n <= p /\ m <= p. Proof. - intros; destruct (M.max_spec n m); intuition; order. + intros; destruct (max_spec n m); intuition; order. Qed. Lemma max_lub_lt : forall n m p, n < p -> m < p -> max n m < p. Proof. - intros; destruct (M.max_spec n m); intuition; order. + intros; destruct (max_spec n m); intuition; order. Qed. Lemma max_lub_lt_iff : forall n m p, max n m < p <-> n < p /\ m < p. Proof. - intros; destruct (M.max_spec n m); intuition; order. + intros; destruct (max_spec n m); intuition; order. Qed. Lemma max_le_compat_l : forall n m p, n <= m -> max p n <= max p m. Proof. intros. - destruct (M.max_spec p n) as [(LT,E)|(LE,E)]; rewrite E. + destruct (max_spec p n) as [(LT,E)|(LE,E)]; rewrite E. assert (LE' := le_max_r p m). order. apply le_max_l. Qed. @@ -269,57 +269,44 @@ Proof. order. Qed. -End MaxProperties. +End MaxLogicalProperties. (** ** Properties concernant [min], then both [min] and [max]. - To avoid duplication of code, we exploit that [min] can be + To avoid too much code duplication, we exploit that [min] can be seen as a [max] of the reversed order. *) -Module MinMaxProperties (Import O:OrderedTypeFull)(Import M:HasMinMax O). - Include MaxProperties O M. +Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O). + Include MaxLogicalProperties O M. + Import T. - Module ORev := OrderedTypeRev O. + Module ORev := TotalOrderRev O. Module MRev <: HasMax ORev. Definition max x y := M.min y x. - Definition max_spec x y := M.min_spec y x. + Definition max_l x y := M.min_r y x. + Definition max_r x y := M.min_l y x. End MRev. - Module MPRev := MaxProperties ORev MRev. + Module MPRev := MaxLogicalProperties ORev MRev. Instance min_compat : Proper (eq==>eq==>eq) min. Proof. intros x x' Hx y y' Hy. apply MPRev.max_compat; assumption. Qed. Lemma min_spec : forall n m, (n < m /\ min n m == n) \/ (m <= n /\ min n m == m). -Proof. exact min_spec. Qed. +Proof. intros. exact (MPRev.max_spec m n). Qed. Lemma min_spec_le : forall n m, (n <= m /\ min n m == n) \/ (m <= n /\ min n m == m). Proof. intros. exact (MPRev.max_spec_le m n). Qed. -Lemma min_case_strong : forall n m (P:O.t -> Type), - (forall x y, x == y -> P x -> P y) -> - (n<=m -> P n) -> (m<=n -> P m) -> P (min n m). -Proof. intros. apply (MPRev.max_case_strong m n P); auto. Qed. - -Lemma min_case : forall n m (P:O.t -> Type), - (forall x y, x == y -> P x -> P y) -> - P n -> P m -> P (min n m). -Proof. intros. apply min_case_strong; auto. Defined. - -Lemma min_dec : forall n m, {min n m == n} + {min n m == m}. -Proof. - intros. destruct (MPRev.max_dec m n); [right|left]; assumption. -Defined. - -Lemma min_monotone: forall f, +Lemma min_mono: forall f, (Proper (eq ==> eq) f) -> (Proper (le ==> le) f) -> forall x y, min (f x) (f y) == f (min x y). Proof. - intros. apply MPRev.max_monotone; auto. compute in *; eauto. + intros. apply MPRev.max_mono; auto. compute in *; eauto. Qed. Lemma min_unicity : forall n m p, @@ -334,17 +321,16 @@ Proof. intros f H n m. apply MPRev.max_unicity, H; auto. Qed. Lemma min_id : forall n, min n n == n. Proof. intros. exact (MPRev.max_id n). Qed. +Notation min_idempotent := min_id (only parsing). + Lemma min_assoc : forall m n p, min m (min n p) == min (min m n) p. Proof. intros. symmetry; apply MPRev.max_assoc. Qed. Lemma min_comm : forall n m, min n m == min m n. Proof. intros. exact (MPRev.max_comm m n). Qed. -Lemma min_l : forall n m, n <= m -> min n m == n. -Proof. intros n m. exact (MPRev.max_r m n). Qed. - -Lemma min_r : forall n m, m <= n -> min n m == m. -Proof. intros n m. exact (MPRev.max_l m n). Qed. +Definition min_l := min_l. +Definition min_r := min_r. Lemma le_min_r : forall n m, min n m <= m. Proof. intros. exact (MPRev.le_max_l m n). Qed. @@ -352,6 +338,12 @@ Proof. intros. exact (MPRev.le_max_l m n). Qed. Lemma le_min_l : forall n m, min n m <= n. Proof. intros. exact (MPRev.le_max_r m n). Qed. +Lemma min_l_iff : forall n m, min n m == n <-> n <= m. +Proof. intros n m. exact (MPRev.max_r_iff m n). Qed. + +Lemma min_r_iff : forall n m, min n m == m <-> m <= n. +Proof. intros n m. exact (MPRev.max_l_iff m n). Qed. + Lemma min_le : forall n m p, min n m <= p -> n <= p \/ m <= p. Proof. intros n m p H. destruct (MPRev.max_le _ _ _ H); auto. Qed. @@ -395,17 +387,17 @@ Proof. intros. apply MPRev.max_le_compat; auto. Qed. Lemma min_max_absorption : forall n m, max n (min n m) == n. Proof. intros. - destruct (M.min_spec n m) as [(C,E)|(C,E)]; rewrite E. - apply max_l. OF.order. - destruct (M.max_spec n m); intuition; OF.order. + destruct (min_spec n m) as [(C,E)|(C,E)]; rewrite E. + apply max_l. order. + destruct (max_spec n m); intuition; order. Qed. Lemma max_min_absorption : forall n m, min n (max n m) == n. Proof. intros. - destruct (M.max_spec n m) as [(C,E)|(C,E)]; rewrite E. - destruct (M.min_spec n m) as [(C',E')|(C',E')]; auto. OF.order. - apply min_l; auto. OF.order. + destruct (max_spec n m) as [(C,E)|(C,E)]; rewrite E. + destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order. + apply min_l; auto. order. Qed. (** Distributivity *) @@ -413,7 +405,7 @@ Qed. Lemma max_min_distr : forall n m p, max n (min m p) == min (max n m) (max n p). Proof. - intros. symmetry. apply min_monotone. + intros. symmetry. apply min_mono. eauto with *. repeat red; intros. apply max_le_compat_l; auto. Qed. @@ -421,7 +413,7 @@ Qed. Lemma min_max_distr : forall n m p, min n (max m p) == max (min n m) (min n p). Proof. - intros. symmetry. apply max_monotone. + intros. symmetry. apply max_mono. eauto with *. repeat red; intros. apply min_le_compat_l; auto. Qed. @@ -432,20 +424,20 @@ Lemma max_min_modular : forall n m p, max n (min m (max n p)) == min (max n m) (max n p). Proof. intros. rewrite <- max_min_distr. - destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E. reflexivity. + destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *. destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'. - rewrite 2 max_l; try OF.order. rewrite min_le_iff; auto. - rewrite 2 max_l; try OF.order. rewrite min_le_iff; auto. + rewrite 2 max_l; try order. rewrite min_le_iff; auto. + rewrite 2 max_l; try order. rewrite min_le_iff; auto. Qed. Lemma min_max_modular : forall n m p, min n (max m (min n p)) == max (min n m) (min n p). Proof. intros. rewrite <- min_max_distr. - destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E. + destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *. destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'. - rewrite 2 min_l; try OF.order. rewrite max_le_iff; right; OF.order. - rewrite 2 min_l; try OF.order. rewrite max_le_iff; auto. reflexivity. + rewrite 2 min_l; try order. rewrite max_le_iff; right; order. + rewrite 2 min_l; try order. rewrite max_le_iff; auto. Qed. (** Disassociativity *) @@ -459,34 +451,196 @@ Qed. (** Anti-monotonicity swaps the role of [min] and [max] *) -Lemma max_min_antimonotone : forall f, +Lemma max_min_antimono : forall f, Proper (eq==>eq) f -> Proper (le==>inverse le) f -> forall x y, max (f x) (f y) == f (min x y). Proof. intros f Eqf Lef x y. - destruct (M.min_spec x y) as [(H,E)|(H,E)]; rewrite E; - destruct (M.max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f y <= f x) by (apply Lef; OF.order). OF.order. - assert (f x <= f y) by (apply Lef; OF.order). OF.order. + destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E; + destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. + assert (f y <= f x) by (apply Lef; order). order. + assert (f x <= f y) by (apply Lef; order). order. Qed. - -Lemma min_max_antimonotone : forall f, +Lemma min_max_antimono : forall f, Proper (eq==>eq) f -> Proper (le==>inverse le) f -> forall x y, min (f x) (f y) == f (max x y). Proof. intros f Eqf Lef x y. - destruct (M.max_spec x y) as [(H,E)|(H,E)]; rewrite E; - destruct (M.min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f y <= f x) by (apply Lef; OF.order). OF.order. - assert (f x <= f y) by (apply Lef; OF.order). OF.order. + destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E; + destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. + assert (f y <= f x) by (apply Lef; order). order. + assert (f x <= f y) by (apply Lef; order). order. Qed. +End MinMaxLogicalProperties. + + +(** ** Properties requiring a decidable order *) + +Module MinMaxDecProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O). + +(** Induction principles for [max]. *) + +Lemma max_case_strong : forall n m (P:t -> Type), + (forall x y, x==y -> P x -> P y) -> + (m<=n -> P n) -> (n<=m -> P m) -> P (max n m). +Proof. +intros n m P Compat Hl Hr. +assert (H:=compare_spec n m). destruct (compare n m). +assert (n<=m) by (inversion H; rewrite le_lteq; auto). +apply (Compat m), Hr; auto. symmetry; apply max_r; auto. +assert (n<=m) by (inversion H; rewrite le_lteq; auto). +apply (Compat m), Hr; auto. symmetry; apply max_r; auto. +assert (m<=n) by (inversion H; rewrite le_lteq; auto). +apply (Compat n), Hl; auto. symmetry; apply max_l; auto. +Defined. + +Lemma max_case : forall n m (P:t -> Type), + (forall x y, x == y -> P x -> P y) -> + P n -> P m -> P (max n m). +Proof. intros. apply max_case_strong; auto. Defined. + +(** [max] returns one of its arguments. *) + +Lemma max_dec : forall n m, {max n m == n} + {max n m == m}. +Proof. + intros n m. apply max_case; auto with relations. + intros x y H [E|E]; [left|right]; rewrite <-H; auto. +Defined. + +(** Idem for [min] *) + +Lemma min_case_strong : forall n m (P:O.t -> Type), + (forall x y, x == y -> P x -> P y) -> + (n<=m -> P n) -> (m<=n -> P m) -> P (min n m). +Proof. +intros n m P Compat Hl Hr. +assert (H:=compare_spec n m). destruct (compare n m). +assert (n<=m) by (inversion H; rewrite le_lteq; auto). +apply (Compat n), Hl; auto. symmetry; apply min_l; auto. +assert (n<=m) by (inversion H; rewrite le_lteq; auto). +apply (Compat n), Hl; auto. symmetry; apply min_l; auto. +assert (m<=n) by (inversion H; rewrite le_lteq; auto). +apply (Compat m), Hr; auto. symmetry; apply min_r; auto. +Defined. + +Lemma min_case : forall n m (P:O.t -> Type), + (forall x y, x == y -> P x -> P y) -> + P n -> P m -> P (min n m). +Proof. intros. apply min_case_strong; auto. Defined. + +Lemma min_dec : forall n m, {min n m == n} + {min n m == m}. +Proof. + intros. apply min_case; auto with relations. + intros x y H [E|E]; [left|right]; rewrite <- E; auto with relations. +Defined. + +End MinMaxDecProperties. + +Module MinMaxProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O). + Module OT := OTF_to_TotalOrder O. + Include MinMaxLogicalProperties OT M. + Include MinMaxDecProperties O M. + Notation max_monotone := max_mono. + Notation min_monotone := min_mono. + Notation max_min_antimonotone := max_min_antimono. + Notation min_max_antimonotone := min_max_antimono. End MinMaxProperties. +(** ** When the equality is Leibniz, we can skip a few [Proper] precondition. *) + +Module UsualMinMaxLogicalProperties + (Import O:UsualTotalOrder')(Import M:HasMinMax O). + + Include MinMaxLogicalProperties O M. + + Lemma max_monotone : forall f, Proper (le ==> le) f -> + forall x y, max (f x) (f y) = f (max x y). + Proof. intros; apply max_mono; auto. congruence. Qed. + + Lemma min_monotone : forall f, Proper (le ==> le) f -> + forall x y, min (f x) (f y) = f (min x y). + Proof. intros; apply min_mono; auto. congruence. Qed. + + Lemma min_max_antimonotone : forall f, Proper (le ==> inverse le) f -> + forall x y, min (f x) (f y) = f (max x y). + Proof. intros; apply min_max_antimono; auto. congruence. Qed. + + Lemma max_min_antimonotone : forall f, Proper (le ==> inverse le) f -> + forall x y, max (f x) (f y) = f (min x y). + Proof. intros; apply max_min_antimono; auto. congruence. Qed. + +End UsualMinMaxLogicalProperties. + + +Module UsualMinMaxDecProperties + (Import O:UsualOrderedTypeFull')(Import M:HasMinMax O). + + Module P := MinMaxDecProperties O M. + + Lemma max_case_strong : forall n m (P:t -> Type), + (m<=n -> P n) -> (n<=m -> P m) -> P (max n m). + Proof. intros; apply P.max_case_strong; auto. congruence. Defined. + + Lemma max_case : forall n m (P:t -> Type), + P n -> P m -> P (max n m). + Proof. intros; apply max_case_strong; auto. Defined. + + Lemma max_dec : forall n m, {max n m = n} + {max n m = m}. + Proof. exact P.max_dec. Defined. + + Lemma min_case_strong : forall n m (P:O.t -> Type), + (m<=n -> P m) -> (n<=m -> P n) -> P (min n m). + Proof. intros; apply P.min_case_strong; auto. congruence. Defined. + + Lemma min_case : forall n m (P:O.t -> Type), + P n -> P m -> P (min n m). + Proof. intros. apply min_case_strong; auto. Defined. + + Lemma min_dec : forall n m, {min n m = n} + {min n m = m}. + Proof. exact P.min_dec. Defined. + +End UsualMinMaxDecProperties. + +Module UsualMinMaxProperties + (Import O:UsualOrderedTypeFull')(Import M:HasMinMax O). + Module OT := OTF_to_TotalOrder O. + Include UsualMinMaxLogicalProperties OT M. + Include UsualMinMaxDecProperties O M. +End UsualMinMaxProperties. + + +(** From [TotalOrder] and [HasMax] and [HasEqDec], we can prove + that the order is decidable and build an [OrderedTypeFull]. *) + +Module TOMaxEqDec_to_Compare + (Import O:TotalOrder')(Import M:HasMax O)(Import E:HasEqDec O) <: HasCompare O. + + Definition compare x y := + if eq_dec x y then Eq + else if eq_dec (M.max x y) y then Lt else Gt. + + Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). + Proof. + intros; unfold compare; repeat destruct eq_dec; auto; constructor. + destruct (lt_total x y); auto. + absurd (x==y); auto. transitivity (max x y); auto. + symmetry. apply max_l. rewrite le_lteq; intuition. + destruct (lt_total y x); auto. + absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition. + Qed. + +End TOMaxEqDec_to_Compare. + +Module TOMaxEqDec_to_OTF (O:TotalOrder)(M:HasMax O)(E:HasEqDec O) + <: OrderedTypeFull + := O <+ E <+ TOMaxEqDec_to_Compare O M E. + + (** TODO: Some Remaining questions... diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v index a7dcb63de..59784553a 100644 --- a/theories/ZArith/ZOdiv.v +++ b/theories/ZArith/ZOdiv.v @@ -262,9 +262,7 @@ Module ZODivMod := ZBinary.ZBinAxiomsMod <+ ZODiv. (** We hence benefit from generic results about this abstract division. *) -Module Z. - Include ZDivTrunc.ZDivPropFunct ZODivMod ZBinary.ZBinPropMod. -End Z. +Module Z := ZDivTrunc.ZDivPropFunct ZODivMod ZBinary.ZBinPropMod. (** * Unicity results *) diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index e6582a775..53c40ae7d 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -20,13 +20,13 @@ Open Local Scope Z_scope. (** * Characterization of maximum on binary integer numbers *) -Definition Zmax_case := Zmax_case. -Definition Zmax_case_strong := Zmax_case_strong. +Definition Zmax_case := Z.max_case. +Definition Zmax_case_strong := Z.max_case_strong. Lemma Zmax_spec : forall x y, x >= y /\ Zmax x y = x \/ x < y /\ Zmax x y = y. Proof. - intros x y. rewrite Zge_iff_le. destruct (Zmax_spec x y); auto. + intros x y. rewrite Zge_iff_le. destruct (Z.max_spec x y); auto. Qed. Lemma Zmax_left : forall n m, n>=m -> Zmax n m = n. @@ -36,60 +36,60 @@ Definition Zmax_right : forall n m, n<=m -> Zmax n m = m := Zmax_r. (** * Least upper bound properties of max *) -Definition Zle_max_l : forall n m, n <= Zmax n m := Zle_max_l. -Definition Zle_max_r : forall n m, m <= Zmax n m := Zle_max_r. +Definition Zle_max_l : forall n m, n <= Zmax n m := Z.le_max_l. +Definition Zle_max_r : forall n m, m <= Zmax n m := Z.le_max_r. Definition Zmax_lub : forall n m p, n <= p -> m <= p -> Zmax n m <= p - := Zmax_lub. + := Z.max_lub. Definition Zmax_lub_lt : forall n m p:Z, n < p -> m < p -> Zmax n m < p - := Zmax_lub_lt. + := Z.max_lub_lt. (** * Compatibility with order *) Definition Zle_max_compat_r : forall n m p, n <= m -> Zmax n p <= Zmax m p - := Zmax_le_compat_r. + := Z.max_le_compat_r. Definition Zle_max_compat_l : forall n m p, n <= m -> Zmax p n <= Zmax p m - := Zmax_le_compat_l. + := Z.max_le_compat_l. (** * Semi-lattice properties of max *) -Definition Zmax_idempotent : forall n, Zmax n n = n := Zmax_id. -Definition Zmax_comm : forall n m, Zmax n m = Zmax m n := Zmax_comm. +Definition Zmax_idempotent : forall n, Zmax n n = n := Z.max_id. +Definition Zmax_comm : forall n m, Zmax n m = Zmax m n := Z.max_comm. Definition Zmax_assoc : forall n m p, Zmax n (Zmax m p) = Zmax (Zmax n m) p - := Zmax_assoc. + := Z.max_assoc. (** * Additional properties of max *) Lemma Zmax_irreducible_dec : forall n m, {Zmax n m = n} + {Zmax n m = m}. -Proof. exact Zmax_dec. Qed. +Proof. exact Z.max_dec. Qed. Definition Zmax_le_prime : forall n m p, p <= Zmax n m -> p <= n \/ p <= m - := Zmax_le. + := Z.max_le. (** * Operations preserving max *) Definition Zsucc_max_distr : forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m) - := Zsucc_max_distr. + := Z.succ_max_distr. Definition Zplus_max_distr_l : forall n m p:Z, Zmax (p + n) (p + m) = p + Zmax n m - := Zplus_max_distr_l. + := Z.plus_max_distr_l. Definition Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p - := Zplus_max_distr_r. + := Z.plus_max_distr_r. (** * Maximum and Zpos *) Definition Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q) - := Zpos_max. + := Z.pos_max. Definition Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p - := Zpos_max_1. + := Z.pos_max_1. (** * Characterization of Pminus in term of Zminus and Zmax *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 0278b604b..5dd26fa38 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -20,47 +20,47 @@ Open Local Scope Z_scope. (** * Characterization of the minimum on binary integer numbers *) -Definition Zmin_case := Zmin_case. -Definition Zmin_case_strong := Zmin_case_strong. +Definition Zmin_case := Z.min_case. +Definition Zmin_case_strong := Z.min_case_strong. Lemma Zmin_spec : forall x y, x <= y /\ Zmin x y = x \/ x > y /\ Zmin x y = y. Proof. - intros x y. rewrite Zgt_iff_lt, Zmin_comm. destruct (Zmin_spec y x); auto. + intros x y. rewrite Zgt_iff_lt, Z.min_comm. destruct (Z.min_spec y x); auto. Qed. (** * Greatest lower bound properties of min *) -Definition Zle_min_l : forall n m, Zmin n m <= n := Zle_min_l. -Definition Zle_min_r : forall n m, Zmin n m <= m := Zle_min_r. +Definition Zle_min_l : forall n m, Zmin n m <= n := Z.le_min_l. +Definition Zle_min_r : forall n m, Zmin n m <= m := Z.le_min_r. Definition Zmin_glb : forall n m p, p <= n -> p <= m -> p <= Zmin n m - := Zmin_glb. + := Z.min_glb. Definition Zmin_glb_lt : forall n m p, p < n -> p < m -> p < Zmin n m - := Zmin_glb_lt. + := Z.min_glb_lt. (** * Compatibility with order *) Definition Zle_min_compat_r : forall n m p, n <= m -> Zmin n p <= Zmin m p - := Zmin_le_compat_r. + := Z.min_le_compat_r. Definition Zle_min_compat_l : forall n m p, n <= m -> Zmin p n <= Zmin p m - := Zmin_le_compat_l. + := Z.min_le_compat_l. (** * Semi-lattice properties of min *) -Definition Zmin_idempotent : forall n, Zmin n n = n := Zmin_id. +Definition Zmin_idempotent : forall n, Zmin n n = n := Z.min_id. Notation Zmin_n_n := Zmin_idempotent (only parsing). -Definition Zmin_comm : forall n m, Zmin n m = Zmin m n := Zmin_comm. +Definition Zmin_comm : forall n m, Zmin n m = Zmin m n := Z.min_comm. Definition Zmin_assoc : forall n m p, Zmin n (Zmin m p) = Zmin (Zmin n m) p - := Zmin_assoc. + := Z.min_assoc. (** * Additional properties of min *) Lemma Zmin_irreducible_inf : forall n m, {Zmin n m = n} + {Zmin n m = m}. -Proof. exact Zmin_dec. Qed. +Proof. exact Z.min_dec. Qed. Lemma Zmin_irreducible : forall n m, Zmin n m = n \/ Zmin n m = m. -Proof. intros; destruct (Zmin_dec n m); auto. Qed. +Proof. intros; destruct (Z.min_dec n m); auto. Qed. Notation Zmin_or := Zmin_irreducible (only parsing). @@ -71,20 +71,20 @@ Proof. intros n m p; apply Zmin_case; auto. Qed. Definition Zsucc_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m) - := Zsucc_min_distr. + := Z.succ_min_distr. -Notation Zmin_SS := Zsucc_min_distr (only parsing). +Notation Zmin_SS := Z.succ_min_distr (only parsing). Definition Zplus_min_distr_r : forall n m p, Zmin (n + p) (m + p) = Zmin n m + p - := Zplus_min_distr_r. + := Z.plus_min_distr_r. -Notation Zmin_plus := Zplus_min_distr_r (only parsing). +Notation Zmin_plus := Z.plus_min_distr_r (only parsing). (** * Minimum and Zpos *) Definition Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q) - := Zpos_min. + := Z.pos_min. diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v index e4d290ab2..108e74bea 100644 --- a/theories/ZArith/Zminmax.v +++ b/theories/ZArith/Zminmax.v @@ -28,251 +28,155 @@ Unboxed Definition Zmin (n m:Z) := (** The functions [Zmax] and [Zmin] implement indeed a maximum and a minimum *) -Lemma Zmax_spec : forall x y, - (x<y /\ Zmax x y = y) \/ (y<=x /\ Zmax x y = x). +Lemma Zmax_l : forall x y, y<=x -> Zmax x y = x. Proof. - unfold Zlt, Zle, Zmax. intros. - generalize (Zcompare_Eq_eq x y). - rewrite <- (Zcompare_antisym x y). - destruct (x ?= y); simpl; auto; right; intuition; discriminate. + unfold Zle, Zmax. intros x y. rewrite <- (Zcompare_antisym x y). + destruct (x ?= y); intuition. Qed. -Lemma Zmin_spec : forall x y, - (x<y /\ Zmin x y = x) \/ (y<=x /\ Zmin x y = y). +Lemma Zmax_r : forall x y, x<=y -> Zmax x y = y. Proof. - unfold Zlt, Zle, Zmin. intros. - generalize (Zcompare_Eq_eq x y). - rewrite <- (Zcompare_antisym x y). - destruct (x ?= y); simpl; auto; right; intuition; discriminate. + unfold Zle, Zmax. intros x y. generalize (Zcompare_Eq_eq x y). + destruct (x ?= y); intuition. Qed. -Module ZHasMinMax <: HasMinMax Z_as_OT. - Definition max := Zmax. - Definition min := Zmin. - Definition max_spec := Zmax_spec. - Definition min_spec := Zmin_spec. -End ZHasMinMax. - -(** We obtain hence all the generic properties of max and min. *) - -Module Import ZMinMaxProps := MinMaxProperties Z_as_OT ZHasMinMax. - -(** For some generic properties, we can have nicer statements here, - since underlying equality is Leibniz. *) - -Lemma Zmax_case_strong : forall n m (P:Z -> Type), - (m<=n -> P n) -> (n<=m -> P m) -> P (Zmax n m). -Proof. intros; apply max_case_strong; auto. congruence. Defined. - -Lemma Zmax_case : forall n m (P:Z -> Type), - P n -> P m -> P (Zmax n m). -Proof. intros. apply Zmax_case_strong; auto. Defined. - -Lemma Zmax_monotone: forall f, - (Proper (Zle ==> Zle) f) -> - forall x y, Zmax (f x) (f y) = f (Zmax x y). -Proof. intros; apply max_monotone; auto. congruence. Qed. - -Lemma Zmin_case_strong : forall n m (P:Z -> Type), - (n<=m -> P n) -> (m<=n -> P m) -> P (Zmin n m). -Proof. intros; apply min_case_strong; auto. congruence. Defined. - -Lemma Zmin_case : forall n m (P:Z -> Type), - P n -> P m -> P (Zmin n m). -Proof. intros. apply Zmin_case_strong; auto. Defined. - -Lemma Zmin_monotone: forall f, - (Proper (Zle ==> Zle) f) -> - forall x y, Zmin (f x) (f y) = f (Zmin x y). -Proof. intros; apply min_monotone; auto. congruence. Qed. - -Lemma Zmax_min_antimonotone : forall f, - Proper (Zle==>Zge) f -> - forall x y, Zmax (f x) (f y) == f (Zmin x y). +Lemma Zmin_l : forall x y, x<=y -> Zmin x y = x. Proof. - intros. apply max_min_antimonotone. congruence. - intros z z' Hz; red. apply Zge_le. auto. + unfold Zle, Zmin. intros x y. generalize (Zcompare_Eq_eq x y). + destruct (x ?= y); intuition. Qed. -Lemma Zmin_max_antimonotone : forall f, - Proper (Zle==>Zge) f -> - forall x y, Zmin (f x) (f y) == f (Zmax x y). +Lemma Zmin_r : forall x y, y<=x -> Zmin x y = y. Proof. - intros. apply min_max_antimonotone. congruence. - intros z z' Hz; red. apply Zge_le. auto. + unfold Zle, Zmin. intros x y. + rewrite <- (Zcompare_antisym x y). generalize (Zcompare_Eq_eq x y). + destruct (x ?= y); intuition. Qed. -(** For the other generic properties, we make aliases, - since otherwise SearchAbout misses some of them - (bad interaction with an Include). - See GenericMinMax (or SearchAbout) for the statements. *) - -Definition Zmax_spec_le := max_spec_le. -Definition Zmax_dec := max_dec. -Definition Zmax_unicity := max_unicity. -Definition Zmax_unicity_ext := max_unicity_ext. -Definition Zmax_id := max_id. -Notation Zmax_idempotent := Zmax_id (only parsing). -Definition Zmax_assoc := max_assoc. -Definition Zmax_comm := max_comm. -Definition Zmax_l := max_l. -Definition Zmax_r := max_r. -Definition Zle_max_l := le_max_l. -Definition Zle_max_r := le_max_r. -Definition Zmax_le := max_le. -Definition Zmax_le_iff := max_le_iff. -Definition Zmax_lt_iff := max_lt_iff. -Definition Zmax_lub_l := max_lub_l. -Definition Zmax_lub_r := max_lub_r. -Definition Zmax_lub := max_lub. -Definition Zmax_lub_iff := max_lub_iff. -Definition Zmax_lub_lt := max_lub_lt. -Definition Zmax_lub_lt_iff := max_lub_lt_iff. -Definition Zmax_le_compat_l := max_le_compat_l. -Definition Zmax_le_compat_r := max_le_compat_r. -Definition Zmax_le_compat := max_le_compat. - -Definition Zmin_spec_le := min_spec_le. -Definition Zmin_dec := min_dec. -Definition Zmin_unicity := min_unicity. -Definition Zmin_unicity_ext := min_unicity_ext. -Definition Zmin_id := min_id. -Notation Zmin_idempotent := Zmin_id (only parsing). -Definition Zmin_assoc := min_assoc. -Definition Zmin_comm := min_comm. -Definition Zmin_l := min_l. -Definition Zmin_r := min_r. -Definition Zle_min_l := le_min_l. -Definition Zle_min_r := le_min_r. -Definition Zmin_le := min_le. -Definition Zmin_le_iff := min_le_iff. -Definition Zmin_lt_iff := min_lt_iff. -Definition Zmin_glb_l := min_glb_l. -Definition Zmin_glb_r := min_glb_r. -Definition Zmin_glb := min_glb. -Definition Zmin_glb_iff := min_glb_iff. -Definition Zmin_glb_lt := min_glb_lt. -Definition Zmin_glb_lt_iff := min_glb_lt_iff. -Definition Zmin_le_compat_l := min_le_compat_l. -Definition Zmin_le_compat_r := min_le_compat_r. -Definition Zmin_le_compat := min_le_compat. - -Definition Zmin_max_absorption := min_max_absorption. -Definition Zmax_min_absorption := max_min_absorption. -Definition Zmax_min_distr := max_min_distr. -Definition Zmin_max_distr := min_max_distr. -Definition Zmax_min_modular := max_min_modular. -Definition Zmin_max_modular := min_max_modular. -Definition Zmax_min_disassoc := max_min_disassoc. +Module ZHasMinMax <: HasMinMax Z_as_OT. + Definition max := Zmax. + Definition min := Zmin. + Definition max_l := Zmax_l. + Definition max_r := Zmax_r. + Definition min_l := Zmin_l. + Definition min_r := Zmin_r. +End ZHasMinMax. + +Module Z. +(** We obtain hence all the generic properties of max and min. *) + +Include UsualMinMaxProperties Z_as_OT ZHasMinMax. (** * Properties specific to the [Z] domain *) (** Compatibilities (consequences of monotonicity) *) -Lemma Zplus_max_distr_l : forall n m p, Zmax (p + n) (p + m) = p + Zmax n m. +Lemma plus_max_distr_l : forall n m p, Zmax (p + n) (p + m) = p + Zmax n m. Proof. - intros. apply Zmax_monotone. + intros. apply max_monotone. intros x y. apply Zplus_le_compat_l. Qed. -Lemma Zplus_max_distr_r : forall n m p, Zmax (n + p) (m + p) = Zmax n m + p. +Lemma plus_max_distr_r : forall n m p, Zmax (n + p) (m + p) = Zmax n m + p. Proof. intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p). - apply Zplus_max_distr_l. + apply plus_max_distr_l. Qed. -Lemma Zplus_min_distr_l : forall n m p, Zmin (p + n) (p + m) = p + Zmin n m. +Lemma plus_min_distr_l : forall n m p, Zmin (p + n) (p + m) = p + Zmin n m. Proof. - intros. apply Zmin_monotone. + intros. apply Z.min_monotone. intros x y. apply Zplus_le_compat_l. Qed. -Lemma Zplus_min_distr_r : forall n m p, Zmin (n + p) (m + p) = Zmin n m + p. +Lemma plus_min_distr_r : forall n m p, Zmin (n + p) (m + p) = Zmin n m + p. Proof. intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p). - apply Zplus_min_distr_l. + apply plus_min_distr_l. Qed. -Lemma Zsucc_max_distr : forall n m, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m). +Lemma succ_max_distr : forall n m, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m). Proof. - unfold Zsucc. intros. symmetry. apply Zplus_max_distr_r. + unfold Zsucc. intros. symmetry. apply plus_max_distr_r. Qed. -Lemma Zsucc_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). +Lemma succ_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). Proof. - unfold Zsucc. intros. symmetry. apply Zplus_min_distr_r. + unfold Zsucc. intros. symmetry. apply plus_min_distr_r. Qed. -Lemma Zpred_max_distr : forall n m, Zpred (Zmax n m) = Zmax (Zpred n) (Zpred m). +Lemma pred_max_distr : forall n m, Zpred (Zmax n m) = Zmax (Zpred n) (Zpred m). Proof. - unfold Zpred. intros. symmetry. apply Zplus_max_distr_r. + unfold Zpred. intros. symmetry. apply plus_max_distr_r. Qed. -Lemma Zpred_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). +Lemma pred_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). Proof. - unfold Zpred. intros. symmetry. apply Zplus_min_distr_r. + unfold Zpred. intros. symmetry. apply plus_min_distr_r. Qed. (** Anti-monotonicity swaps the role of [min] and [max] *) -Lemma Zopp_max_distr : forall n m : Z, -(Zmax n m) = Zmin (- n) (- m). +Lemma opp_max_distr : forall n m : Z, -(Zmax n m) = Zmin (- n) (- m). Proof. - intros. symmetry. apply Zmin_max_antimonotone. - intros x x'. rewrite Zge_iff_le; red; rewrite <- Zcompare_opp; auto. + intros. symmetry. apply min_max_antimonotone. + intros x x'. red. red. rewrite <- Zcompare_opp; auto. Qed. -Lemma Zopp_min_distr : forall n m : Z, - (Zmin n m) = Zmax (- n) (- m). +Lemma opp_min_distr : forall n m : Z, - (Zmin n m) = Zmax (- n) (- m). Proof. - intros. symmetry. apply Zmax_min_antimonotone. - intros x x'. rewrite Zge_iff_le; red; rewrite <- Zcompare_opp; auto. + intros. symmetry. apply max_min_antimonotone. + intros x x'. red. red. rewrite <- Zcompare_opp; auto. Qed. -Lemma Zminus_max_distr_l : forall n m p, Zmax (p - n) (p - m) = p - Zmin n m. +Lemma minus_max_distr_l : forall n m p, Zmax (p - n) (p - m) = p - Zmin n m. Proof. - unfold Zminus. intros. rewrite Zopp_min_distr. apply Zplus_max_distr_l. + unfold Zminus. intros. rewrite opp_min_distr. apply plus_max_distr_l. Qed. -Lemma Zminus_max_distr_r : forall n m p, Zmax (n - p) (m - p) = Zmax n m - p. +Lemma minus_max_distr_r : forall n m p, Zmax (n - p) (m - p) = Zmax n m - p. Proof. - unfold Zminus. intros. apply Zplus_max_distr_r. + unfold Zminus. intros. apply plus_max_distr_r. Qed. -Lemma Zminus_min_distr_l : forall n m p, Zmin (p - n) (p - m) = p - Zmax n m. +Lemma minus_min_distr_l : forall n m p, Zmin (p - n) (p - m) = p - Zmax n m. Proof. - unfold Zminus. intros. rewrite Zopp_max_distr. apply Zplus_min_distr_l. + unfold Zminus. intros. rewrite opp_max_distr. apply plus_min_distr_l. Qed. -Lemma Zminus_min_distr_r : forall n m p, Zmin (n - p) (m - p) = Zmin n m - p. +Lemma minus_min_distr_r : forall n m p, Zmin (n - p) (m - p) = Zmin n m - p. Proof. - unfold Zminus. intros. apply Zplus_min_distr_r. + unfold Zminus. intros. apply plus_min_distr_r. Qed. (** Compatibility with [Zpos] *) -Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q). +Lemma pos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q). Proof. intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q). destruct Pcompare; auto. intro H; rewrite H; auto. Qed. -Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q). +Lemma pos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q). Proof. intros; unfold Zmin, Pmin; simpl; generalize (Pcompare_Eq_eq p q). destruct Pcompare; auto. Qed. -Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p. +Lemma pos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p. Proof. intros; unfold Zmax; simpl; destruct p; simpl; auto. Qed. -Lemma Zpos_min_1 : forall p, Zmin 1 (Zpos p) = 1. +Lemma pos_min_1 : forall p, Zmin 1 (Zpos p) = 1. Proof. intros; unfold Zmax; simpl; destruct p; simpl; auto. Qed. +End Z. + (** * Characterization of Pminus in term of Zminus and Zmax *) @@ -282,17 +186,17 @@ Proof. rewrite (Pcompare_Eq_eq _ _ H). unfold Pminus; rewrite Pminus_mask_diag; reflexivity. rewrite Pminus_Lt; auto. - symmetry. apply Zpos_max_1. + symmetry. apply Z.pos_max_1. Qed. (*begin hide*) (* Compatibility with names of the old Zminmax file *) -Notation Zmin_max_absorption_r_r := Zmin_max_absorption (only parsing). -Notation Zmax_min_absorption_r_r := Zmax_min_absorption (only parsing). -Notation Zmax_min_distr_r := Zmax_min_distr (only parsing). -Notation Zmin_max_distr_r := Zmin_max_distr (only parsing). -Notation Zmax_min_modular_r := Zmax_min_modular (only parsing). -Notation Zmin_max_modular_r := Zmin_max_modular (only parsing). -Notation max_min_disassoc := Zmax_min_disassoc (only parsing). +Notation Zmin_max_absorption_r_r := Z.min_max_absorption (only parsing). +Notation Zmax_min_absorption_r_r := Z.max_min_absorption (only parsing). +Notation Zmax_min_distr_r := Z.max_min_distr (only parsing). +Notation Zmin_max_distr_r := Z.min_max_distr (only parsing). +Notation Zmax_min_modular_r := Z.max_min_modular (only parsing). +Notation Zmin_max_modular_r := Z.min_max_modular (only parsing). +Notation max_min_disassoc := Z.max_min_disassoc (only parsing). (*end hide*)
\ No newline at end of file |