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
|
(************************************************************************)
(* 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 9302 2006-10-27 21:21:17Z barras $ i*)
(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
Require Import Arith_base.
Require Import BinPos.
Require Import BinInt.
Require Import Zorder.
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.
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.
(** * 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.
(** * Absolute value in nat is compatible with order *)
Lemma Zabs_nat_lt :
forall n m:Z, 0 <= n /\ n < m -> (Zabs_nat n < Zabs_nat m)%nat.
Proof.
intros x y. case x; simpl in |- *. case y; simpl in |- *.
intro. absurd (0 < 0). compute in |- *. intro H0. discriminate H0. intuition.
intros. elim (ZL4 p). intros. rewrite H0. auto with arith.
intros. elim (ZL4 p). intros. rewrite H0. auto with arith.
case y; simpl in |- *.
intros. absurd (Zpos p < 0). compute in |- *. intro H0. discriminate H0. intuition.
intros. change (nat_of_P p > nat_of_P p0)%nat in |- *.
apply nat_of_P_gt_Gt_compare_morphism.
elim H; auto with arith. intro. exact (ZC2 p0 p).
intros. absurd (Zpos p0 < Zneg p).
compute in |- *. intro H0. discriminate H0. intuition.
intros. absurd (0 <= Zneg p). compute in |- *. auto with arith. intuition.
Qed.
|
