1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "models/nat_uniform.ma".
16 include "supremum.ma".
17 include "nat/le_arith.ma".
18 include "russell_support.ma".
20 inductive cmp_cases (n,m:nat) : CProp ≝
21 | cmp_lt : n < m → cmp_cases n m
22 | cmp_eq : n = m → cmp_cases n m
23 | cmp_gt : m < n → cmp_cases n m.
25 lemma cmp_nat: ∀n,m.cmp_cases n m.
26 intros; generalize in match (nat_compare_to_Prop n m);
27 cases (nat_compare n m); intros;
28 [constructor 1|constructor 2|constructor 3] assumption;
31 alias symbol "pi1" = "exT fst".
32 alias symbol "leq" = "natural 'less or equal to'".
33 lemma nat_dedekind_sigma_complete:
34 ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
35 ∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
36 intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉);
37 fold normalize X; intros; cases H1;
38 letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = fst (a j)) ∨ (i < u ∧ s+i ≤ u + fst (a j))); (* s - aj <= max 0 (u - i) *)
46 match cmp_nat (fst apred) s with
48 | cmp_gt nP ⇒ match ? in False return λ_.nat with []
49 | cmp_lt nP ⇒ fst (H3 apred nP)]]
52 ∀i:nat.∃j:nat.spec i j));unfold spec in aux ⊢ %;
53 [1: apply (H2 pred nP);
54 |4: unfold X in H2; clear H4 n aux spec H3 H1 H X;
55 generalize in match H2;
56 generalize in match Hs;
57 generalize in match a;
58 clear H2 Hs a; cases u; intros (a Hs H);
59 [1: left; split; [apply le_n]
60 generalize in match H;
61 generalize in match Hs;
63 [2: cases Hs; lapply (os_le_to_nat_le ?? H1);
64 apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin).
65 |1: intros; lapply (os_le_to_nat_le (fst (a O)) O (H2 O));
66 lapply (le_n_O_to_eq ? Hletin); assumption;]
67 |2: right; cases Hs; rewrite > (sym_plus s O); split; [apply le_S_S; apply le_O_n];
68 apply (trans_le ??? (os_le_to_nat_le ?? H1));
71 generalize in match H5; clear H5; cases (aux n1); intros;
72 change in match (a 〈w,H5〉) in H6 ⊢ % with (a w);
73 cases H5; clear H5; cases H7; clear H7;
74 [1: left; split; [ apply (le_S ?? H5); | assumption]
75 |3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6);
76 |*: cut (u ≤ S n1 ∨ S n1 < u);
77 [2,4: cases (cmp_nat u (S n1));
78 [1,4: left; apply lt_to_le; assumption
79 |2,5: rewrite > H7; left; apply le_n
80 |3,6: right; assumption ]
81 |*: cases Hcut; clear Hcut
82 [1,3: left; split; [1,3: assumption |2: symmetry; assumption]
83 cut (u = S n1); [2: apply le_to_le_to_eq; assumption ]
84 clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
85 cut (s = S (fst (a w)));
86 [2: apply le_to_le_to_eq; [2: assumption]
87 change in H8 with (s + n1 ≤ S (n1 + fst (a w)));
88 rewrite > plus_n_Sm in H8; rewrite > sym_plus in H8;
89 apply (le_plus_to_le ??? H8);]
91 change with (s = fst (a w1));
92 change in H4 with (fst (a w) < fst (a w1));
93 apply le_to_le_to_eq; [ rewrite > Hcut; assumption ]
94 apply (os_le_to_nat_le (fst (a w1)) s (H2 w1));
95 |*: right; split; try assumption;
96 [1: rewrite > sym_plus in ⊢ (? ? %);
97 rewrite < H6; apply le_plus_r; assumption;
98 |2: cases (H3 (a w) H6);
99 change with (s + S n1 ≤ u + fst (a w1));rewrite < plus_n_Sm;
100 apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
101 apply (le_plus ???? (le_n ?) H9);]]]]]
102 clearbody m; unfold spec in m; clear spec;
104 let rec find i u on u : nat ≝
107 | S w ⇒ match eqb (fst (a (m i))) s with
109 | false ⇒ find (S i) w]]
112 ∀i,bound.∃j.i + bound = u → s = fst (a j));
113 [1: cases (find (S n) n2); intro; change with (s = fst (a w));
114 apply H6; rewrite < H7; simplify; apply plus_n_Sm;
115 |2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
116 |3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
117 cases (m u); cases H4; clear H4; cases H5; clear H5; [assumption]
118 cases (not_le_Sn_n ? H4)]
119 clearbody find; cases (find O u);
120 exists [apply w]; intros; change with (s = fst (a j));
121 rewrite > (H4 ?); [2: reflexivity]
122 apply le_to_le_to_eq;
123 [1: apply os_le_to_nat_le;
124 apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5));
125 |2: apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);]
126 rewrite < (H4 ?); [2: reflexivity] apply le_n;]
129 alias symbol "pi1" = "exT fst".
130 alias symbol "leq" = "natural 'less or equal to'".
131 axiom nat_dedekind_sigma_complete_r:
132 ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing →
133 ∀x.x is_infimum a → ∃i.∀j.i ≤ j → fst x = fst (a j).