1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import Orders BinInt Zcompare Zorder ZBinary.
(** * Maximum and Minimum of two [Z] numbers *)
Local Open Scope Z_scope.
(* All generic properties about max and min are already in [ZBinary.Z].
We prove here in addition some results specific to Z.
*)
Module Z.
Include ZBinary.Z.
(** Compatibilities (consequences of monotonicity) *)
Lemma plus_max_distr_l : forall n m p, Zmax (p + n) (p + m) = p + Zmax n m.
Proof.
intros. apply max_monotone.
intros x y. apply Zplus_le_compat_l.
Qed.
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 plus_max_distr_l.
Qed.
Lemma plus_min_distr_l : forall n m p, Zmin (p + n) (p + m) = p + Zmin n m.
Proof.
intros. apply Z.min_monotone.
intros x y. apply Zplus_le_compat_l.
Qed.
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 plus_min_distr_l.
Qed.
Lemma succ_max_distr : forall n m, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m).
Proof.
unfold Zsucc. intros. symmetry. apply plus_max_distr_r.
Qed.
Lemma succ_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
Proof.
unfold Zsucc. intros. symmetry. apply plus_min_distr_r.
Qed.
Lemma pred_max_distr : forall n m, Zpred (Zmax n m) = Zmax (Zpred n) (Zpred m).
Proof.
unfold Zpred. intros. symmetry. apply plus_max_distr_r.
Qed.
Lemma pred_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
Proof.
unfold Zpred. intros. symmetry. apply plus_min_distr_r.
Qed.
(** Anti-monotonicity swaps the role of [min] and [max] *)
Lemma opp_max_distr : forall n m : Z, -(Zmax n m) = Zmin (- n) (- m).
Proof.
intros. symmetry. apply min_max_antimonotone.
intros x x'. red. red. rewrite <- Zcompare_opp; auto.
Qed.
Lemma opp_min_distr : forall n m : Z, - (Zmin n m) = Zmax (- n) (- m).
Proof.
intros. symmetry. apply max_min_antimonotone.
intros x x'. red. red. rewrite <- Zcompare_opp; auto.
Qed.
Lemma minus_max_distr_l : forall n m p, Zmax (p - n) (p - m) = p - Zmin n m.
Proof.
unfold Zminus. intros. rewrite opp_min_distr. apply plus_max_distr_l.
Qed.
Lemma minus_max_distr_r : forall n m p, Zmax (n - p) (m - p) = Zmax n m - p.
Proof.
unfold Zminus. intros. apply plus_max_distr_r.
Qed.
Lemma minus_min_distr_l : forall n m p, Zmin (p - n) (p - m) = p - Zmax n m.
Proof.
unfold Zminus. intros. rewrite opp_max_distr. apply plus_min_distr_l.
Qed.
Lemma minus_min_distr_r : forall n m p, Zmin (n - p) (m - p) = Zmin n m - p.
Proof.
unfold Zminus. intros. apply plus_min_distr_r.
Qed.
(** Compatibility with [Zpos] *)
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 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 pos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
Proof.
intros; unfold Zmax; simpl; destruct p; simpl; auto.
Qed.
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 *)
Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
Proof.
intros; simpl. destruct (Pcompare p q Eq) as [ ]_eqn:H.
rewrite (Pcompare_Eq_eq _ _ H).
unfold Pminus; rewrite Pminus_mask_diag; reflexivity.
rewrite Pminus_Lt; auto.
symmetry. apply Z.pos_max_1.
Qed.
(*begin hide*)
(* Compatibility with names of the old Zminmax file *)
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*)
|
