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: Znat.v,v 1.1.2.1 2004/07/16 19:31:43 herbelin Exp $ i*)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
Require Export Arith.
Require BinPos.
Require BinInt.
Require Zcompare.
Require Zorder.
Require Decidable.
Require Peano_dec.
Require Export Compare_dec.
Open Local Scope Z_scope.
Definition neq := [x,y:nat] ~(x=y).
(**********************************************************************)
(** Properties of the injection from nat into Z *)
Theorem inj_S : (y:nat) (inject_nat (S y)) = (Zs (inject_nat y)).
Proof.
Intro y; NewInduction y as [|n H]; [
Unfold Zs ; Simpl; Trivial with arith
| Change (POS (add_un (anti_convert n)))=(Zs (inject_nat (S n)));
Rewrite add_un_Zs; Trivial with arith].
Qed.
Theorem inj_plus :
(x,y:nat) (inject_nat (plus x y)) = (Zplus (inject_nat x) (inject_nat y)).
Proof.
Intro x; NewInduction x as [|n H]; Intro y; NewDestruct y as [|m]; [
Simpl; Trivial with arith
| Simpl; Trivial with arith
| Simpl; Rewrite <- plus_n_O; Trivial with arith
| Change (inject_nat (S (plus n (S m))))=
(Zplus (inject_nat (S n)) (inject_nat (S m)));
Rewrite inj_S; Rewrite H; Do 2 Rewrite inj_S; Rewrite Zplus_S_n; Trivial with arith].
Qed.
Theorem inj_mult :
(x,y:nat) (inject_nat (mult x y)) = (Zmult (inject_nat x) (inject_nat y)).
Proof.
Intro x; NewInduction x as [|n H]; [
Simpl; Trivial with arith
| Intro y; Rewrite -> inj_S; Rewrite <- Zmult_Sm_n;
Rewrite <- H;Rewrite <- inj_plus; Simpl; Rewrite plus_sym; Trivial with arith].
Qed.
Theorem inj_neq:
(x,y:nat) (neq x y) -> (Zne (inject_nat x) (inject_nat y)).
Proof.
Unfold neq Zne not ; Intros x y H1 H2; Apply H1; Generalize H2;
Case x; Case y; Intros; [
Auto with arith
| Discriminate H0
| Discriminate H0
| Simpl in H0; Injection H0; Do 2 Rewrite <- bij1; Intros E; Rewrite E; Auto with arith].
Qed.
Theorem inj_le:
(x,y:nat) (le x y) -> (Zle (inject_nat x) (inject_nat y)).
Proof.
Intros x y; Intros H; Elim H; [
Unfold Zle ; Elim (Zcompare_EGAL (inject_nat x) (inject_nat x));
Intros H1 H2; Rewrite H2; [ Discriminate | Trivial with arith]
| Intros m H1 H2; Apply Zle_trans with (inject_nat m);
[Assumption | Rewrite inj_S; Apply Zle_n_Sn]].
Qed.
Theorem inj_lt: (x,y:nat) (lt x y) -> (Zlt (inject_nat x) (inject_nat y)).
Proof.
Intros x y H; Apply Zgt_lt; Apply Zle_S_gt; Rewrite <- inj_S; Apply inj_le;
Exact H.
Qed.
Theorem inj_gt: (x,y:nat) (gt x y) -> (Zgt (inject_nat x) (inject_nat y)).
Proof.
Intros x y H; Apply Zlt_gt; Apply inj_lt; Exact H.
Qed.
Theorem inj_ge: (x,y:nat) (ge x y) -> (Zge (inject_nat x) (inject_nat y)).
Proof.
Intros x y H; Apply Zle_ge; Apply inj_le; Apply H.
Qed.
Theorem inj_eq: (x,y:nat) x=y -> (inject_nat x) = (inject_nat y).
Proof.
Intros x y H; Rewrite H; Trivial with arith.
Qed.
Theorem intro_Z :
(x:nat) (EX y:Z | (inject_nat x)=y /\
(Zle ZERO (Zplus (Zmult y (POS xH)) ZERO))).
Proof.
Intros x; Exists (inject_nat x); Split; [
Trivial with arith
| Rewrite Zmult_sym; Rewrite Zmult_one; Rewrite Zero_right;
Unfold Zle ; Elim x; Intros;Simpl; Discriminate ].
Qed.
Theorem inj_minus1 :
(x,y:nat) (le y x) ->
(inject_nat (minus x y)) = (Zminus (inject_nat x) (inject_nat y)).
Proof.
Intros x y H; Apply (Zsimpl_plus_l (inject_nat y)); Unfold Zminus ;
Rewrite Zplus_permute; Rewrite Zplus_inverse_r; Rewrite <- inj_plus;
Rewrite <- (le_plus_minus y x H);Rewrite Zero_right; Trivial with arith.
Qed.
Theorem inj_minus2: (x,y:nat) (gt y x) -> (inject_nat (minus x y)) = ZERO.
Proof.
Intros x y H; Rewrite inj_minus_aux; [ Trivial with arith | Apply gt_not_le; Assumption].
Qed.
V7only [ (* From Zdivides *) ].
Theorem POS_inject: (x : positive) (POS x) = (inject_nat (convert x)).
Proof.
Intros x; Elim x; Simpl; Auto.
Intros p H; Rewrite ZL6.
Apply f_equal with f := POS.
Apply convert_intro.
Rewrite bij1; Unfold convert; Simpl.
Rewrite ZL6; Auto.
Intros p H; Unfold convert; Simpl.
Rewrite ZL6; Simpl.
Rewrite inj_plus; Repeat Rewrite <- H.
Rewrite POS_xO; Simpl; Rewrite add_x_x; Reflexivity.
Qed.
|
