diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-07 15:32:34 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-07 15:32:34 +0000 |
commit | e1059385b30316f974d47558d8b95b1980a8f1f8 (patch) | |
tree | 431d038070717f22d23b5e3d648c96c363c22292 /theories/ZArith/Zminmax.v | |
parent | 50411a16e71008f9d4f951e82637d1f38b02a58d (diff) |
Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibniz part
Moreover, instantiation like MinMax are now made without redefining
generic properties (easier maintenance). We start using inner modules
for qualifying (e.g. Z.max_comm).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12638 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zminmax.v')
-rw-r--r-- | theories/ZArith/Zminmax.v | 236 |
1 files changed, 70 insertions, 166 deletions
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 |