blob: 57778caecad6badd19310cdeeae556b64f2ab2ce (
plain)
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
|
(************************************************************************)
(* 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,v 1.1.2.1 2004/07/16 19:31:42 herbelin Exp $ i*)
(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
Require Arith.
Require BinPos.
Require BinInt.
Require Zorder.
Require Zsyntax.
Require ZArith_dec.
V7only [Import nat_scope.].
Open Local Scope Z_scope.
(**********************************************************************)
(** Properties of absolute value *)
Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x.
Intro x; NewDestruct x; Auto with arith.
Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
Qed.
Lemma Zabs_non_eq : (x:Z) (Zle x ZERO) -> (Zabs x)=(Zopp x).
Proof.
Intro x; NewDestruct x; Auto with arith.
Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
Qed.
V7only [ (* From Zdivides *) ].
Theorem Zabs_Zopp: (z : Z) (Zabs (Zopp z)) = (Zabs z).
Proof.
Intros z; Case z; Simpl; Auto.
Qed.
(** Proving a property of the absolute value by cases *)
Lemma Zabs_ind :
(P:Z->Prop)(x:Z)(`x >= 0` -> (P x)) -> (`x <= 0` -> (P `-x`)) ->
(P `|x|`).
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.
Save.
V7only [ (* From Zdivides *) ].
Theorem Zabs_intro: (P : ?) (z : Z) (P (Zopp z)) -> (P z) -> (P (Zabs z)).
Intros P z; Case z; Simpl; Auto.
Qed.
Definition Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}.
Proof.
Intro x; NewDestruct x;Auto with arith.
Defined.
Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)).
Intro x; NewDestruct x;Auto with arith; Compute; Intros H;Inversion H.
Qed.
V7only [ (* From Zdivides *) ].
Theorem Zabs_eq_case:
(z1, z2 : Z) (Zabs z1) = (Zabs z2) -> z1 = z2 \/ z1 = (Zopp z2).
Proof.
Intros z1 z2; Case z1; Case z2; Simpl; Auto; Try (Intros; Discriminate);
Intros p1 p2 H1; Injection H1; (Intros H2; Rewrite H2); Auto.
Qed.
(** Triangular inequality *)
Hints Local Resolve Zle_NEG_POS :zarith.
V7only [ (* From Zdivides *) ].
Theorem Zabs_triangle:
(z1, z2 : Z) (Zle (Zabs (Zplus z1 z2)) (Zplus (Zabs z1) (Zabs z2))).
Proof.
Intros z1 z2; Case z1; Case z2; Try (Simpl; Auto with zarith; Fail).
Intros p1 p2;
Apply Zabs_intro
with P := [x : ?] (Zle x (Zplus (Zabs (POS p2)) (Zabs (NEG p1))));
Try Rewrite Zopp_Zplus; Auto with zarith.
Apply Zle_plus_plus; Simpl; Auto with zarith.
Apply Zle_plus_plus; Simpl; Auto with zarith.
Intros p1 p2;
Apply Zabs_intro
with P := [x : ?] (Zle x (Zplus (Zabs (POS p2)) (Zabs (NEG p1))));
Try Rewrite Zopp_Zplus; Auto with zarith.
Apply Zle_plus_plus; Simpl; Auto with zarith.
Apply Zle_plus_plus; Simpl; Auto with zarith.
Qed.
(** Absolute value and multiplication *)
Lemma Zsgn_Zabs: (x:Z)(Zmult x (Zsgn x))=(Zabs x).
Proof.
Intro x; NewDestruct x; Rewrite Zmult_sym; Auto with arith.
Qed.
Lemma Zabs_Zsgn: (x:Z)(Zmult (Zabs x) (Zsgn x))=x.
Proof.
Intro x; NewDestruct x; Rewrite Zmult_sym; Auto with arith.
Qed.
V7only [ (* From Zdivides *) ].
Theorem Zabs_Zmult:
(z1, z2 : Z) (Zabs (Zmult z1 z2)) = (Zmult (Zabs z1) (Zabs z2)).
Proof.
Intros z1 z2; Case z1; Case z2; Simpl; Auto.
Qed.
(** absolute value in nat is compatible with order *)
Lemma absolu_lt : (x,y:Z) (Zle ZERO x)/\(Zlt x y) -> (lt (absolu x) (absolu y)).
Proof.
Intros x y. Case x; Simpl. Case y; Simpl.
Intro. Absurd (Zlt ZERO ZERO). Compute. 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.
Intros. Absurd (Zlt (POS p) ZERO). Compute. Intro H0. Discriminate H0. Intuition.
Intros. Change (gt (convert p) (convert p0)).
Apply compare_convert_SUPERIEUR.
Elim H; Auto with arith. Intro. Exact (ZC2 p0 p).
Intros. Absurd (Zlt (POS p0) (NEG p)).
Compute. Intro H0. Discriminate H0. Intuition.
Intros. Absurd (Zle ZERO (NEG p)). Compute. Auto with arith. Intuition.
Qed.
|
