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
226
227
228
229
230
231
232
233
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
Require Import ZAxioms ZProperties.
Require Import BinInt Zcompare Zorder ZArith_dec Zbool Zeven.
Local Open Scope Z_scope.
(** An alternative Zpow *)
(** The Zpow is extensionnaly equal to Zpower in ZArith, but not
convertible with it. This Zpow uses a logarithmic number of
multiplications instead of a linear one. We should try someday to
replace Zpower with this Zpow.
*)
Definition Zpow n m :=
match m with
| Z0 => 1
| Zpos p => Piter_op Zmult p n
| Zneg p => 0
end.
Lemma Zpow_0_r : forall n, Zpow n 0 = 1.
Proof. reflexivity. Qed.
Lemma Zpow_succ_r : forall a b, 0<=b -> Zpow a (Zsucc b) = a * Zpow a b.
Proof.
intros a [|b|b] Hb; [ | |now elim Hb]; simpl.
now rewrite Zmult_1_r.
rewrite <- Pplus_one_succ_r. apply Piter_op_succ. apply Zmult_assoc.
Qed.
Lemma Zpow_neg : forall a b, b<0 -> Zpow a b = 0.
Proof.
now destruct b.
Qed.
Theorem Z_bi_induction :
forall A : Z -> Prop, Proper (eq ==> iff) A ->
A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n.
Proof.
intros A A_wd A0 AS n; apply Zind; clear n.
assumption.
intros; rewrite <- Zsucc_succ'. now apply -> AS.
intros n H. rewrite <- Zpred_pred'. rewrite Zsucc_pred in H. now apply <- AS.
Qed.
(** * Implementation of [ZAxiomsMiniSig] by [BinInt.Z] *)
Module Z
<: ZAxiomsSig <: UsualOrderedTypeFull <: TotalOrder
<: UsualDecidableTypeFull.
Definition t := Z.
Definition eqb := Zeq_bool.
Definition zero := 0.
Definition one := 1.
Definition two := 2.
Definition succ := Zsucc.
Definition pred := Zpred.
Definition add := Zplus.
Definition sub := Zminus.
Definition mul := Zmult.
Definition lt := Zlt.
Definition le := Zle.
Definition compare := Zcompare.
Definition min := Zmin.
Definition max := Zmax.
Definition opp := Zopp.
Definition abs := Zabs.
Definition sgn := Zsgn.
Definition eq_dec := Z_eq_dec.
Definition bi_induction := Z_bi_induction.
(** Basic operations. *)
Definition eq_equiv : Equivalence (@eq Z) := eq_equivalence.
Local Obligation Tactic := simpl_relation.
Program Instance succ_wd : Proper (eq==>eq) Zsucc.
Program Instance pred_wd : Proper (eq==>eq) Zpred.
Program Instance add_wd : Proper (eq==>eq==>eq) Zplus.
Program Instance sub_wd : Proper (eq==>eq==>eq) Zminus.
Program Instance mul_wd : Proper (eq==>eq==>eq) Zmult.
Definition pred_succ n := eq_sym (Zpred_succ n).
Definition add_0_l := Zplus_0_l.
Definition add_succ_l := Zplus_succ_l.
Definition sub_0_r := Zminus_0_r.
Definition sub_succ_r := Zminus_succ_r.
Definition mul_0_l := Zmult_0_l.
Definition mul_succ_l := Zmult_succ_l.
Lemma one_succ : 1 = Zsucc 0.
Proof.
reflexivity.
Qed.
Lemma two_succ : 2 = Zsucc 1.
Proof.
reflexivity.
Qed.
(** Boolean Equality *)
Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y).
(** Order *)
Program Instance lt_wd : Proper (eq==>eq==>iff) Zlt.
Definition lt_eq_cases := Zle_lt_or_eq_iff.
Definition lt_irrefl := Zlt_irrefl.
Definition lt_succ_r := Zlt_succ_r.
(** Comparison *)
Definition compare_spec := Zcompare_spec.
(** Minimum and maximum *)
Definition min_l := Zmin_l.
Definition min_r := Zmin_r.
Definition max_l := Zmax_l.
Definition max_r := Zmax_r.
(** Properties specific to integers, not natural numbers. *)
Program Instance opp_wd : Proper (eq==>eq) Zopp.
Definition succ_pred n := eq_sym (Zsucc_pred n).
Definition opp_0 := Zopp_0.
Definition opp_succ := Zopp_succ.
(** Absolute value and sign *)
Definition abs_eq := Zabs_eq.
Definition abs_neq := Zabs_non_eq.
Definition sgn_null := Zsgn_0.
Definition sgn_pos := Zsgn_1.
Definition sgn_neg := Zsgn_m1.
(** Even and Odd *)
Definition Even n := exists m, n=2*m.
Definition Odd n := exists m, n=2*m+1.
Lemma even_spec n : Zeven_bool n = true <-> Even n.
Proof. rewrite Zeven_bool_iff. exact (Zeven_ex_iff n). Qed.
Lemma odd_spec n : Zodd_bool n = true <-> Odd n.
Proof. rewrite Zodd_bool_iff. exact (Zodd_ex_iff n). Qed.
Definition even := Zeven_bool.
Definition odd := Zodd_bool.
(** Power *)
Program Instance pow_wd : Proper (eq==>eq==>eq) Zpow.
Definition pow_0_r := Zpow_0_r.
Definition pow_succ_r := Zpow_succ_r.
Definition pow_neg := Zpow_neg.
Definition pow := Zpow.
(** We define [eq] only here to avoid refering to this [eq] above. *)
Definition eq := (@eq Z).
(** Now the generic properties. *)
Include ZProp
<+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
End Z.
(** * An [order] tactic for integers *)
Ltac z_order := Z.order.
(** Note that [z_order] is domain-agnostic: it will not prove
[1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
Section TestOrder.
Let test : forall x y, x<=y -> y<=x -> x=y.
Proof.
z_order.
Qed.
End TestOrder.
(** Z forms a ring *)
(*Lemma Zring : ring_theory 0 1 NZadd NZmul NZsub Zopp NZeq.
Proof.
constructor.
exact Zadd_0_l.
exact Zadd_comm.
exact Zadd_assoc.
exact Zmul_1_l.
exact Zmul_comm.
exact Zmul_assoc.
exact Zmul_add_distr_r.
intros; now rewrite Zadd_opp_minus.
exact Zadd_opp_r.
Qed.
Add Ring ZR : Zring.*)
(*
Theorem eq_equiv_e : forall x y : Z, E x y <-> e x y.
Proof.
intros x y; unfold E, e, Zeq_bool; split; intro H.
rewrite H; now rewrite Zcompare_refl.
rewrite eq_true_unfold_pos in H.
assert (H1 : (x ?= y) = Eq).
case_eq (x ?= y); intro H1; rewrite H1 in H; simpl in H;
[reflexivity | discriminate H | discriminate H].
now apply Zcompare_Eq_eq.
Qed.
*)
|
