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
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(*i $Id: Zabs.v 10302 2007-11-08 09:54:31Z letouzey $ i*)
(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
Require Import Arith_base.
Require Import BinPos.
Require Import BinInt.
Require Import Zorder.
Require Import Zmax.
Require Import Znat.
Require Import ZArith_dec.
Open Local Scope Z_scope.
(**********************************************************************)
(** * Properties of absolute value *)
Lemma Zabs_eq : forall n:Z, 0 <= n -> Zabs n = n.
Proof.
intro x; destruct x; auto with arith.
compute in |- *; intros; absurd (Gt = Gt); trivial with arith.
Qed.
Lemma Zabs_non_eq : forall n:Z, n <= 0 -> Zabs n = - n.
Proof.
intro x; destruct x; auto with arith.
compute in |- *; intros; absurd (Gt = Gt); trivial with arith.
Qed.
Theorem Zabs_Zopp : forall n:Z, Zabs (- n) = Zabs n.
Proof.
intros z; case z; simpl in |- *; auto.
Qed.
(** * Proving a property of the absolute value by cases *)
Lemma Zabs_ind :
forall (P:Z -> Prop) (n:Z),
(n >= 0 -> P n) -> (n <= 0 -> P (- n)) -> P (Zabs n).
Proof.
intros P x H H0; elim (Z_lt_ge_dec x 0); intro.
assert (x <= 0). apply Zlt_le_weak; assumption.
rewrite Zabs_non_eq. apply H0. assumption. assumption.
rewrite Zabs_eq. apply H; assumption. apply Zge_le. assumption.
Qed.
Theorem Zabs_intro : forall P (n:Z), P (- n) -> P n -> P (Zabs n).
Proof.
intros P z; case z; simpl in |- *; auto.
Qed.
Definition Zabs_dec : forall x:Z, {x = Zabs x} + {x = - Zabs x}.
Proof.
intro x; destruct x; auto with arith.
Defined.
Lemma Zabs_pos : forall n:Z, 0 <= Zabs n.
intro x; destruct x; auto with arith; compute in |- *; intros H; inversion H.
Qed.
Lemma Zabs_involutive : forall x:Z, Zabs (Zabs x) = Zabs x.
Proof.
intros; apply Zabs_eq; apply Zabs_pos.
Qed.
Theorem Zabs_eq_case : forall n m:Z, Zabs n = Zabs m -> n = m \/ n = - m.
Proof.
intros z1 z2; case z1; case z2; simpl in |- *; auto;
try (intros; discriminate); intros p1 p2 H1; injection H1;
(intros H2; rewrite H2); auto.
Qed.
Lemma Zabs_spec : forall x:Z,
0 <= x /\ Zabs x = x \/
0 > x /\ Zabs x = -x.
Proof.
intros; unfold Zabs, Zle, Zgt; destruct x; simpl; intuition discriminate.
Qed.
(** * Triangular inequality *)
Hint Local Resolve Zle_neg_pos: zarith.
Theorem Zabs_triangle : forall n m:Z, Zabs (n + m) <= Zabs n + Zabs m.
Proof.
intros z1 z2; case z1; case z2; try (simpl in |- *; auto with zarith; fail).
intros p1 p2;
apply Zabs_intro with (P := fun x => x <= Zabs (Zpos p2) + Zabs (Zneg p1));
try rewrite Zopp_plus_distr; auto with zarith.
apply Zplus_le_compat; simpl in |- *; auto with zarith.
apply Zplus_le_compat; simpl in |- *; auto with zarith.
intros p1 p2;
apply Zabs_intro with (P := fun x => x <= Zabs (Zpos p2) + Zabs (Zneg p1));
try rewrite Zopp_plus_distr; auto with zarith.
apply Zplus_le_compat; simpl in |- *; auto with zarith.
apply Zplus_le_compat; simpl in |- *; auto with zarith.
Qed.
(** * Absolute value and multiplication *)
Lemma Zsgn_Zabs : forall n:Z, n * Zsgn n = Zabs n.
Proof.
intro x; destruct x; rewrite Zmult_comm; auto with arith.
Qed.
Lemma Zabs_Zsgn : forall n:Z, Zabs n * Zsgn n = n.
Proof.
intro x; destruct x; rewrite Zmult_comm; auto with arith.
Qed.
Theorem Zabs_Zmult : forall n m:Z, Zabs (n * m) = Zabs n * Zabs m.
Proof.
intros z1 z2; case z1; case z2; simpl in |- *; auto.
Qed.
Theorem Zabs_square : forall a, Zabs a * Zabs a = a * a.
Proof.
destruct a; simpl; auto.
Qed.
(** * Results about absolute value in nat. *)
Theorem inj_Zabs_nat : forall z:Z, Z_of_nat (Zabs_nat z) = Zabs z.
Proof.
destruct z; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P.
Qed.
Theorem Zabs_nat_Z_of_nat: forall n, Zabs_nat (Z_of_nat n) = n.
Proof.
destruct n; simpl; auto.
apply nat_of_P_o_P_of_succ_nat_eq_succ.
Qed.
Lemma Zabs_nat_mult: forall n m:Z, Zabs_nat (n*m) = (Zabs_nat n * Zabs_nat m)%nat.
Proof.
intros; apply inj_eq_rev.
rewrite inj_mult; repeat rewrite inj_Zabs_nat; apply Zabs_Zmult.
Qed.
Lemma Zabs_nat_Zsucc:
forall p, 0 <= p -> Zabs_nat (Zsucc p) = S (Zabs_nat p).
Proof.
intros; apply inj_eq_rev.
rewrite inj_S; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith.
Qed.
Lemma Zabs_nat_Zplus:
forall x y, 0<=x -> 0<=y -> Zabs_nat (x+y) = (Zabs_nat x + Zabs_nat y)%nat.
Proof.
intros; apply inj_eq_rev.
rewrite inj_plus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith.
apply Zplus_le_0_compat; auto.
Qed.
Lemma Zabs_nat_Zminus:
forall x y, 0 <= x <= y -> Zabs_nat (y - x) = (Zabs_nat y - Zabs_nat x)%nat.
Proof.
intros x y (H,H').
assert (0 <= y) by (apply Zle_trans with x; auto).
assert (0 <= y-x) by (apply Zle_minus_le_0; auto).
apply inj_eq_rev.
rewrite inj_minus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto.
rewrite Zmax_right; auto.
Qed.
Lemma Zabs_nat_le :
forall n m:Z, 0 <= n <= m -> (Zabs_nat n <= Zabs_nat m)%nat.
Proof.
intros n m (H,H'); apply inj_le_rev.
repeat rewrite inj_Zabs_nat, Zabs_eq; auto.
apply Zle_trans with n; auto.
Qed.
Lemma Zabs_nat_lt :
forall n m:Z, 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat.
Proof.
intros n m (H,H'); apply inj_lt_rev.
repeat rewrite inj_Zabs_nat, Zabs_eq; auto.
apply Zlt_le_weak; apply Zle_lt_trans with n; auto.
Qed.
(** * Some results about the sign function. *)
Lemma Zsgn_Zmult : forall a b, Zsgn (a*b) = Zsgn a * Zsgn b.
Proof.
destruct a; destruct b; simpl; auto.
Qed.
Lemma Zsgn_Zopp : forall a, Zsgn (-a) = - Zsgn a.
Proof.
destruct a; simpl; auto.
Qed.
(** A characterization of the sign function: *)
Lemma Zsgn_spec : forall x:Z,
0 < x /\ Zsgn x = 1 \/
0 = x /\ Zsgn x = 0 \/
0 > x /\ Zsgn x = -1.
Proof.
intros; unfold Zsgn, Zle, Zgt; destruct x; compute; intuition.
Qed.
Lemma Zsgn_pos : forall x:Z, Zsgn x = 1 <-> 0 < x.
Proof.
destruct x; now intuition.
Qed.
Lemma Zsgn_neg : forall x:Z, Zsgn x = -1 <-> x < 0.
Proof.
destruct x; now intuition.
Qed.
Lemma Zsgn_null : forall x:Z, Zsgn x = 0 <-> x = 0.
Proof.
destruct x; now intuition.
Qed.
|
