1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: Znat.v 10726 2008-03-28 18:15:23Z notin $ i*)
11
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
13
Require Export Arith_base.
14
Require Import BinPos.
15
Require Import BinInt.
16
Require Import Zcompare.
17
Require Import Zorder.
18
Require Import Decidable.
19
Require Import Peano_dec.
20
Require Import Min Max Zmin Zmax.
21
Require Export Compare_dec.
23
Open Local Scope Z_scope.
25
Definition neq (x y:nat) := x <> y.
27
(************************************************)
28
(** Properties of the injection from nat into Z *)
30
(** Injection and successor *)
32
Theorem inj_0 : Z_of_nat 0 = 0%Z.
37
Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n).
39
intro y; induction y as [| n H];
40
[ unfold Zsucc in |- *; simpl in |- *; trivial with arith
41
| change (Zpos (Psucc (P_of_succ_nat n)) = Zsucc (Z_of_nat (S n))) in |- *;
42
rewrite Zpos_succ_morphism; trivial with arith ].
45
(** Injection and equality. *)
47
Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
49
intros x y H; rewrite H; trivial with arith.
52
Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m).
54
unfold neq, Zne, not in |- *; intros x y H1 H2; apply H1; generalize H2;
55
case x; case y; intros;
59
| simpl in H0; injection H0;
60
do 2 rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ;
61
intros E; rewrite E; auto with arith ].
64
Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m.
67
destruct (eq_nat_dec x y) as [H'|H']; auto.
69
exact (inj_neq _ _ H' H).
72
Theorem inj_eq_iff : forall n m:nat, n=m <-> Z_of_nat n = Z_of_nat m.
74
split; [apply inj_eq | apply inj_eq_rev].
78
(** Injection and order relations: *)
82
Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m.
84
intros x y; intros H; elim H;
85
[ unfold Zle in |- *; elim (Zcompare_Eq_iff_eq (Z_of_nat x) (Z_of_nat x));
86
intros H1 H2; rewrite H2; [ discriminate | trivial with arith ]
87
| intros m H1 H2; apply Zle_trans with (Z_of_nat m);
88
[ assumption | rewrite inj_S; apply Zle_succ ] ].
91
Theorem inj_lt : forall n m:nat, (n < m)%nat -> Z_of_nat n < Z_of_nat m.
93
intros x y H; apply Zgt_lt; apply Zlt_succ_gt; rewrite <- inj_S; apply inj_le;
97
Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
99
intros x y H; apply Zle_ge; apply inj_le; apply H.
102
Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m.
104
intros x y H; apply Zlt_gt; apply inj_lt; exact H.
107
(** The other way ... *)
109
Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat.
112
destruct (le_lt_dec x y) as [H0|H0]; auto.
114
assert (H1:=inj_lt _ _ H0).
116
rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
119
Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
122
destruct (le_lt_dec y x) as [H0|H0]; auto.
124
assert (H1:=inj_le _ _ H0).
126
rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
129
Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat.
132
destruct (le_lt_dec y x) as [H0|H0]; auto.
134
assert (H1:=inj_gt _ _ H0).
136
rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
139
Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat.
142
destruct (le_lt_dec x y) as [H0|H0]; auto.
144
assert (H1:=inj_ge _ _ H0).
146
rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
151
Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m.
153
split; [apply inj_le | apply inj_le_rev].
156
Theorem inj_lt_iff : forall n m:nat, (n<m)%nat <-> Z_of_nat n < Z_of_nat m.
158
split; [apply inj_lt | apply inj_lt_rev].
161
Theorem inj_ge_iff : forall n m:nat, (n>=m)%nat <-> Z_of_nat n >= Z_of_nat m.
163
split; [apply inj_ge | apply inj_ge_rev].
166
Theorem inj_gt_iff : forall n m:nat, (n>m)%nat <-> Z_of_nat n > Z_of_nat m.
168
split; [apply inj_gt | apply inj_gt_rev].
171
(** Injection and usual operations *)
173
Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
175
intro x; induction x as [| n H]; intro y; destruct y as [| m];
176
[ simpl in |- *; trivial with arith
177
| simpl in |- *; trivial with arith
178
| simpl in |- *; rewrite <- plus_n_O; trivial with arith
179
| change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *;
180
rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l;
181
trivial with arith ].
184
Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
186
intro x; induction x as [| n H];
187
[ simpl in |- *; trivial with arith
188
| intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H;
189
rewrite <- inj_plus; simpl in |- *; rewrite plus_comm;
190
trivial with arith ].
194
forall n m:nat, (m <= n)%nat -> Z_of_nat (n - m) = Z_of_nat n - Z_of_nat m.
196
intros x y H; apply (Zplus_reg_l (Z_of_nat y)); unfold Zminus in |- *;
197
rewrite Zplus_permute; rewrite Zplus_opp_r; rewrite <- inj_plus;
198
rewrite <- (le_plus_minus y x H); rewrite Zplus_0_r;
202
Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z_of_nat (n - m) = 0.
204
intros x y H; rewrite not_le_minus_0;
205
[ trivial with arith | apply gt_not_le; assumption ].
208
Theorem inj_minus : forall n m:nat,
209
Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m).
214
destruct (le_lt_dec m n) as [H|H].
216
rewrite (inj_minus1 _ _ H).
217
assert (H':=Zle_minus_le_0 _ _ (inj_le _ _ H)).
219
rewrite <- Zcompare_antisym in H'.
220
destruct Zcompare; simpl in *; intuition.
222
rewrite (inj_minus2 _ _ H).
223
assert (H':=Zplus_lt_compat_r _ _ (- Z_of_nat m) (inj_lt _ _ H)).
224
rewrite Zplus_opp_r in H'.
225
unfold Zminus; rewrite H'; auto.
228
Theorem inj_min : forall n m:nat,
229
Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m).
231
induction n; destruct m; try (compute; auto; fail).
234
rewrite <- Zsucc_min_distr; f_equal; auto.
237
Theorem inj_max : forall n m:nat,
238
Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m).
240
induction n; destruct m; try (compute; auto; fail).
243
rewrite <- Zsucc_max_distr; f_equal; auto.
246
(** Composition of injections **)
248
Theorem Zpos_eq_Z_of_nat_o_nat_of_P :
249
forall p:positive, Zpos p = Z_of_nat (nat_of_P p).
251
intros x; elim x; simpl in |- *; auto.
252
intros p H; rewrite ZL6.
253
apply f_equal with (f := Zpos).
255
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; unfold nat_of_P in |- *;
258
intros p H; unfold nat_of_P in |- *; simpl in |- *.
259
rewrite ZL6; simpl in |- *.
260
rewrite inj_plus; repeat rewrite <- H.
261
rewrite Zpos_xO; simpl in |- *; rewrite Pplus_diag; reflexivity.
267
forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
269
intros x; exists (Z_of_nat x); split;
271
| rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r;
272
unfold Zle in |- *; elim x; intros; simpl in |- *;
276
Lemma Zpos_P_of_succ_nat : forall n:nat,
277
Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n).
283
simpl (P_of_succ_nat (S n)).
284
apply Zpos_succ_morphism.