blob: 6910717b4ad4ad7876a082d906d4881988ace5f8 (
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
|
(* $Id$ *)
Require fast_integer.
Require zarith_aux.
Require auxiliary.
Require Zsyntax.
(* Our purpose is to write an induction shema for {0,1,2,...}
similar to the nat schema (Theorem [Natlike_rec]). For that the
following implications will be used :
\begin{verbatim}
(n:nat)(Q n)==(n:nat)(P (inject_nat n)) ===> (x:Z)`x > 0) -> (P x)
/\
||
||
(Q O) (n:nat)(Q n)->(Q (S n)) <=== (P 0) (x:Z) (P x) -> (P (Zs x))
<=== (inject_nat (S n))=(Zs (inject_nat n))
<=== inject_nat_complete
Then the diagram will be closed and the theorem proved.
\end{verbatim}
*)
Lemma inject_nat_complete :
(x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)).
Destruct x; Intros;
[ Exists O; Auto with arith
| Specialize (ZL4 p); Intros Hp; Elim Hp; Intros;
Exists (S x0); Intros; Simpl;
Specialize (bij1 x0); Intro Hx0;
Rewrite <- H0 in Hx0;
Apply f_equal with f:=POS;
Apply convert_intro; Auto with arith
| Absurd `0 <= (NEG p)`;
[ Unfold Zle; Simpl; Do 2 (Unfold not); Auto with arith
| Assumption]
].
Save.
Lemma ZL4_inf: (y:positive) { h:nat | (convert y)=(S h) }.
Induction y; [
Intros p H;Elim H; Intros x H1; Exists (plus (S x) (S x));
Unfold convert ;Simpl; Rewrite ZL0; Rewrite ZL2; Unfold convert in H1;
Rewrite H1; Auto with arith
| Intros p H1;Elim H1;Intros x H2; Exists (plus x (S x)); Unfold convert;
Simpl; Rewrite ZL0; Rewrite ZL2;Unfold convert in H2; Rewrite H2; Auto with arith
| Exists O ;Auto with arith].
Save.
Lemma inject_nat_complete_inf :
(x:Z)`0 <= x` -> { n:nat | (x=(inject_nat n)) }.
Destruct x; Intros;
[ Exists O; Auto with arith
| Specialize (ZL4_inf p); Intros Hp; Elim Hp; Intros x0 H0;
Exists (S x0); Intros; Simpl;
Specialize (bij1 x0); Intro Hx0;
Rewrite <- H0 in Hx0;
Apply f_equal with f:=POS;
Apply convert_intro; Auto with arith
| Absurd `0 <= (NEG p)`;
[ Unfold Zle; Simpl; Do 2 (Unfold not); Auto with arith
| Assumption]
].
Save.
Lemma inject_nat_prop :
(P:Z->Prop)((n:nat)(P (inject_nat n))) ->
(x:Z) `0 <= x` -> (P x).
Intros.
Specialize (inject_nat_complete x H0).
Intros Hn; Elim Hn; Intros.
Rewrite -> H1; Apply H.
Save.
Lemma ZERO_le_inj :
(n:nat) `0 <= (inject_nat n)`.
Induction n; Simpl; Intros;
[ Apply Zle_n
| Unfold Zle; Simpl; Discriminate].
Save.
Lemma natlike_ind : (P:Z->Prop) (P `0`) ->
((x:Z)(`0 <= x` -> (P x) -> (P (Zs x)))) ->
(x:Z) `0 <= x` -> (P x).
Intros; Apply inject_nat_prop;
[ Induction n;
[ Simpl; Assumption
| Intros; Rewrite -> (inj_S n0);
Exact (H0 (inject_nat n0) (ZERO_le_inj n0) H2) ]
| Assumption].
Save.
Lemma Z_lt_induction :
(P:Z->Prop)
((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x))
-> (x:Z)`0 <= x`->(P x).
Proof.
Intros P H x Hx.
Cut (x:Z)`0 <= x`->(y:Z)`0 <= y < x`->(P y).
Intro.
Apply (H0 (Zs x)).
Auto with zarith.
Split; [ Assumption | Exact (Zlt_n_Sn x) ].
Intros x0 Hx0; Generalize Hx0; Pattern x0; Apply natlike_ind.
Intros.
Absurd `0 <= 0`; Try Assumption.
Apply Zgt_not_le.
Apply Zgt_le_trans with m:=y.
Apply Zlt_gt.
Intuition. Intuition.
Intros. Apply H. Intros.
Apply (H1 H0).
Split; [ Intuition | Idtac ].
Apply Zlt_le_trans with y. Intuition.
Apply Zgt_S_le. Apply Zlt_gt. Intuition.
Assumption.
Save.
|
