]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
more notation moved to core notation, unification of duplicated CProp connectives
[helm.git] / helm / software / matita / contribs / dama / dama / models / nat_dedekind_sigma_complete.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 include "models/nat_uniform.ma".
16 include "supremum.ma".
17 include "nat/le_arith.ma".
18 include "russell_support.ma".
19
20 alias symbol "pi1" = "exT \fst".
21 alias symbol "leq" = "natural 'less or equal to'".
22 lemma nat_dedekind_sigma_complete:
23   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → 
24     ∀x.x is_supremum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
25 intros 5; cases x (s Hs); clear x; letin X ≝ ≪s,Hs≫; 
26 fold normalize X; intros; cases H1; 
27 alias symbol "plus" = "natural plus".
28 alias symbol "N" = "Uniform space N".
29 alias symbol "and" = "logical and".
30 letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = \fst (a j)) ∨ (i < u ∧ s+i ≤ u + \fst (a j))); 
31 (* s - aj <= max 0 (u - i) *)  
32 letin m ≝ (hide ? (
33   let rec aux i ≝
34     match i with
35     [ O ⇒ O
36     | S m ⇒ 
37         let pred ≝ aux m in
38         let apred ≝ a pred in 
39         match cmp_nat s (\fst apred) with
40         [ cmp_le _ ⇒ pred
41         | cmp_gt nP ⇒ \fst (H3 apred ?)]]
42   in aux 
43    :
44    ∀i:nat.∃j:nat.spec i j));[whd; apply nP;] unfold spec in aux ⊢ %;
45 [3: unfold X in H2; clear H4 n aux spec H3 H1 H X;
46     cases u in H2 Hs a ⊢ %; intros (a Hs H);
47     [1: left; split; [apply le_n]
48         generalize in match H;
49         generalize in match Hs;
50         rewrite > (?:s = O); 
51         [2: cases Hs; lapply (os_le_to_nat_le ?? H1);
52             apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin).
53         |1: intros; lapply (os_le_to_nat_le (\fst (a O)) O (H2 O));
54             lapply (le_n_O_to_eq ? Hletin); assumption;]
55     |2: right; cases Hs; rewrite > (sym_plus s O); split; [apply le_S_S; apply le_O_n];
56         apply (trans_le ??? (os_le_to_nat_le ?? H1));
57         apply le_plus_n_r;] 
58 |2: clear H6; cut (s = \fst (a (aux n1))); [2:
59       cases (le_to_or_lt_eq ?? H5); [2: assumption]
60       cases (?:False); apply (H2 (aux n1) H6);] clear H5;
61       generalize in match Hcut; clear Hcut; intro H5;
62 |1: clear H6]
63 [2,1:
64     cases (aux n1) in H5 ⊢ %; intros;
65     change in match (a ≪w,H5≫) in H6 ⊢ % with (a w);
66     cases H5; clear H5; cases H7; clear H7;
67     [1: left; split; [ apply (le_S ?? H5); | assumption]
68     |3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6);
69     |*: cases (cmp_nat u (S n1));
70         [1,3: left; split; [1,3: assumption |2: assumption]
71             cut (u = S n1); [2: apply le_to_le_to_eq; assumption ]
72             clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
73             cut (s = S (\fst (a w)));
74             [2: apply le_to_le_to_eq; [2: assumption]
75                 change in H8 with (s + n1 ≤ S (n1 + \fst (a w)));
76                 rewrite > plus_n_Sm in H8; rewrite > sym_plus in H8;
77                 apply (le_plus_to_le ??? H8);]
78             cases (H3 (a w) H6);
79             change with (s = \fst (a w1));
80             change in H4 with (\fst (a w) < \fst (a w1));
81             apply le_to_le_to_eq; [ rewrite > Hcut; assumption ]
82             apply (os_le_to_nat_le (\fst (a w1)) s (H2 w1));
83         |*: right; split; try assumption;
84             [1: rewrite > sym_plus in ⊢ (? ? %);
85                 rewrite < H6; apply le_plus_r; assumption;
86             |2: cases (H3 (a w) H6);
87                 change with (s + S n1 ≤ u + \fst (a w1));rewrite < plus_n_Sm;
88                 apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
89                 apply (le_plus ???? (le_n ?) H9);]]]]
90 clearbody m; unfold spec in m; clear spec;
91 letin find ≝ (
92  let rec find i u on u : nat ≝
93   match u with
94   [ O ⇒ (m i:nat)
95   | S w ⇒ match eqb (\fst (a (m i))) s with
96           [ true ⇒ (m i:nat)
97           | false ⇒ find (S i) w]]
98  in find
99  :
100   ∀i,bound.∃j.i + bound = u → s = \fst (a j));
101 [1: cases (find (S n) n2); intro; change with (s = \fst (a w));
102     apply H6; rewrite < H7; simplify; apply plus_n_Sm;
103 |2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
104 |3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
105     cases (m u); cases H4; clear H4; cases H5; clear H5; [assumption]
106     cases (not_le_Sn_n ? H4)]
107 clearbody find; cases (find O u);
108 exists [apply w]; intros; change with (s = \fst (a j));
109 rewrite > (H4 ?); [2: reflexivity]
110 apply le_to_le_to_eq;
111 [1: apply os_le_to_nat_le;
112     apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5));
113 |2: apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);]
114     rewrite < (H4 ?); [2: reflexivity] apply le_n;]
115 qed.
116
117 alias symbol "pi1" = "exT \fst".
118 alias symbol "leq" = "natural 'less or equal to'".
119 alias symbol "N" = "ordered set N".
120 axiom nat_dedekind_sigma_complete_r:
121   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing → 
122     ∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).