aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Wf_Z.v
blob: 65571855e1185c197b71818e6158f555c45d1618 (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
(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(*i $Id$ i*)

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)).
NewDestruct x; Intros;
[ Exists  O; Auto with arith
| Specialize (ZL4 p); Intros Hp; Elim Hp; Intros;
  Exists (S x); Intros; Simpl;
  Specialize (bij1 x); 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)) }.
NewDestruct 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.