]> matita.cs.unibo.it Git - helm.git/blob - matita/dama/reals.ma
New dependency over acic_procedural.
[helm.git] / matita / dama / reals.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/reals/".
16
17 include "ordered_fields_ch0.ma".
18
19 record is_real (F:ordered_field_ch0) : Type
20
21  { r_archimedean: ∀x:F. ∃n:nat. x ≤ (sum_field ? n);
22    r_complete: is_complete F  
23  }.
24
25 record real: Type \def
26  { r_ordered_field_ch0:> ordered_field_ch0;
27    r_real_properties: is_real r_ordered_field_ch0
28  }.
29
30 definition lim: ∀R:real.∀f:nat→R.is_cauchy_seq ? f → R.
31  intros;
32  elim (r_complete ? (r_real_properties R) ? H);
33  exact a.
34 qed.
35
36 definition max_seq: ∀R:real.∀x,y:R. nat → R.
37  intros (R x y);
38  elim (cos_cotransitive R 0 (inv ? (sum_field ? (S n)) ?) (x-y));
39   [ apply x
40   | apply not_eq_sum_field_zero ;
41     unfold;
42     auto new
43   | apply y
44   | apply lt_zero_to_le_inv_zero 
45   ].
46 qed.
47
48 axiom daemon: False.
49
50 theorem cauchy_max_seq: ∀R:real.∀x,y:R. is_cauchy_seq ? (max_seq ? x y).
51 elim daemon.
52 (*
53  intros;
54  unfold;
55  intros;
56  exists; [ exact m | ]; (* apply (ex_intro ? ? m); *)
57  intros;
58  unfold max_seq;
59  elim (of_cotransitive R 0
60 (inv R (sum_field R (S N))
61  (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))) (x-y)
62 (lt_zero_to_le_inv_zero R (S N)
63  (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))));
64   [ simplify;
65     elim (of_cotransitive R  0
66 (inv R (1+sum R (plus R) 0 1 m)
67  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
68 (lt_zero_to_le_inv_zero R (S m)
69  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
70     [ simplify;
71       rewrite > (plus_comm ? x (-x));
72       rewrite > opp_inverse;
73       split;
74        [ apply (le_zero_x_to_le_opp_x_zero R ?); 
75          apply lt_zero_to_le_inv_zero
76        | apply lt_zero_to_le_inv_zero
77        ]
78     | simplify;
79       split;
80        [ apply (or_transitive ? ? R ? 0);
81           [ apply (le_zero_x_to_le_opp_x_zero R ?)
82           | assumption
83           ]
84        | assumption
85        ]
86     ]
87   | simplify;
88     elim (of_cotransitive R 0
89 (inv R (1+sum R (plus R) 0 1 m)
90  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
91 (lt_zero_to_le_inv_zero R (S m)
92  (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
93      [ simplify;
94        split;
95        [ elim daemon
96        | generalize in match (le_zero_x_to_le_opp_x_zero R ? t1);
97          intro;
98          unfold minus in H1;
99          rewrite > eq_opp_plus_plus_opp_opp in H1;
100          rewrite > eq_opp_opp_x_x in H1;
101          rewrite > plus_comm in H1;
102          apply (or_transitive ? ? R ? 0);
103           [ assumption
104           | apply lt_zero_to_le_inv_zero
105           ]
106         ]
107      | simplify;
108        rewrite > (plus_comm ? y (-y));
109        rewrite > opp_inverse;
110        split;
111        [ elim daemon
112        | apply lt_zero_to_le_inv_zero
113        ]
114      ]
115   ].
116   elim daemon.*)
117 qed.
118
119 definition max: ∀R:real.R → R → R.
120  intros (R x y);
121  apply (lim R (max_seq R x y));
122  apply cauchy_max_seq.
123 qed.
124
125 definition abs \def λR:real.λx:R. max R x (-x).
126
127 lemma comparison:
128  ∀R:real.∀f,g:nat→R. is_cauchy_seq ? f → is_cauchy_seq ? g →
129   (∀n:nat.f n ≤ g n) → lim ? f ? ≤ lim ? g ?.
130  [ assumption
131  | assumption
132  | intros;
133    elim daemon
134  ].
135 qed.
136
137 definition to_zero ≝
138  λR:real.λn.
139   -(inv R (sum_field R (S n))
140    (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))).
141   
142 axiom is_cauchy_seq_to_zero: ∀R:real. is_cauchy_seq ? (to_zero R).
143
144 lemma technical1: ∀R:real.lim R (to_zero R) (is_cauchy_seq_to_zero R) = 0.
145  intros;
146  unfold lim;
147  elim daemon.
148 qed.
149  
150 lemma abs_x_ge_O: ∀R:real.∀x:R. 0 ≤ abs ? x.
151  intros;
152  unfold abs;
153  unfold max;
154  rewrite < technical1;
155  apply comparison;
156  intros;
157  unfold to_zero;
158  unfold max_seq;
159  elim
160      (cos_cotransitive R 0
161 (inv R (sum_field R (S n))
162  (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))) (x--x)
163 (lt_zero_to_le_inv_zero R (S n)
164  (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))));
165  [ simplify;
166    (* facile *)
167    elim daemon
168  | simplify;
169    (* facile *)
170    elim daemon
171  ].
172 qed.