(* *)
(**************************************************************************)
+include "nat/le_arith.ma".
include "nat_ordered_set.ma".
include "bishop_set_rewrite.ma".
include "uniform.ma".
interpretation "naturals" 'nat = nat.
interpretation "Ordered set N" 'nat = nat_ordered_set.
-include "russell_support.ma".
-
inductive cmp_cases (n,m:nat) : CProp ≝
| cmp_lt : n < m → cmp_cases n m
| cmp_eq : n = m → cmp_cases n m
intros; cases (cmp_nat n m);
[assumption
|generalize in match H1; rewrite < H2; intros;
- cases (not_lt_n_n (fst (a n))); apply os_lt_to_nat_lt; apply H3;
-|cases (not_lt_n_n (fst (a m)));
+ cases (Not_lt_n_n (fst (a n))); apply os_lt_to_nat_lt; apply H3;
+|cases (Not_lt_n_n (fst (a m)));
apply (trans_le_lt_lt ? (fst (a n)));
[2: apply os_lt_to_nat_lt; apply H1;
|1: apply os_le_to_nat_le; apply (trans_increasing ?? H m n);
cases Hcut1; assumption]
qed.
+include "russell_support.ma".
+
alias symbol "pi1" = "exT fst".
lemma nat_dedekind_sigma_complete:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉);
fold normalize X; intros; cases H1;
-letin spec ≝ (λi,j.fst (a j) = s ∨ (i ≤ j ∧ match i with [ O ⇒ fst (a j) = fst (a O) | S m ⇒ fst(a m) < fst (a j)]));
-letin m ≝ (
+letin spec ≝ (λi,j.(u≤i ∧ s = fst (a j)) ∨ (i < u ∧ s+i ≤ u + fst (a j))); (* s - aj <= max 0 (u - i) *)
+letin m ≝ (hide ? (
let rec aux i ≝
match i with
[ O ⇒ O
| cmp_lt nP ⇒ fst (H3 apred nP)]]
in aux
:
- ∀i:nat.∃j:nat.spec i j);unfold spec in aux ⊢ %;
+ ∀i:nat.∃j:nat.spec i j));unfold spec in aux ⊢ %;
[1: apply (H2 pred nP);
-|4: right; split; whd; constructor 1;
-|2,3: whd in ⊢ (? ? %);
- [1: left; assumption
- |2: elim (H3 (a (aux n1)) H5) (res_n);
- change with (fst (a res_n) = s ∨ (n1 < res_n ∧ fst (a n1) < fst (a res_n)));
- change in H7 with (fst (a (aux n1)) < fst (a res_n));
- elim (aux n1) in H7 ⊢ % (pred);
- change in H8 with (fst (a pred) < fst (a res_n));
- cases H7; clear H7;
- [ left; apply le_to_le_to_eq;
- [ apply os_le_to_nat_le; apply (H2 res_n);
- | rewrite < H9; apply le_S_S_to_le; apply le_S; apply H8;]
- | cases H9; clear H9; right; split;
- [ lapply (trans_increasing ?? H n1 pred (nat_le_to_os_le ?? H7)) as H11;
- clear H6; apply (key ??? H);
- apply (le_lt_transitive ?? (a pred)); [assumption]
- generalize in match H8; cases (a pred); cases (a res_n);
- simplify; intro D; lapply (nat_lt_to_os_lt ?? D) as Q;
- cases Q; clear D Q; split; assumption;
- | generalize in match H10; generalize in match H7; clear H7 H10;
- cases n1; intros;
- [ rewrite < H9; assumption
- | clear H9; apply (trans_le_lt_lt ??? ? H8);
- apply os_le_to_nat_le; lapply (nat_le_to_os_le ?? H7) as H77;
- apply(trans_increasing ?? H (S n2) (pred) H77);]]]]]
+|4: unfold X in H2; clear H4 n aux spec H3 H1 H X;
+ generalize in match H2;
+ generalize in match Hs;
+ generalize in match a;
+ clear H2 Hs a; cases u; intros (a Hs H);
+ [1: left; split; [apply le_n]
+ generalize in match H;
+ generalize in match Hs;
+ rewrite > (?:s = O);
+ [2: cases Hs; lapply (os_le_to_nat_le ?? H1);
+ apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin).
+ |1: intros; lapply (os_le_to_nat_le (fst (a O)) O (H2 O));
+ lapply (le_n_O_to_eq ? Hletin); assumption;]
+ |2: right; cases Hs; rewrite > (sym_plus s O); split; [apply le_S_S; apply le_O_n];
+ apply (trans_le ??? (os_le_to_nat_le ?? H1));
+ apply le_plus_n_r;]
+|2,3: clear H6;
+ generalize in match H5; clear H5; cases (aux n1); intros;
+ change in match (a 〈w,H5〉) in H6 ⊢ % with (a w);
+ cases H5; clear H5; cases H7; clear H7;
+ [1: left;
+ split;
+ [ apply (le_S ?? H5)
+ | assumption]
+ |3: elimType False;
+ rewrite < H8 in H6;
+ apply (not_le_Sn_n ? H6)
+ |*: cut (u ≤ S n1 ∨ S n1 < u);
+ [2,4: cases (cmp_nat u (S n1));
+ [1,4: left; apply lt_to_le; assumption
+ |2,5: rewrite > H7; left; apply le_n
+ |3,6: right; assumption ]
+ |*: cases Hcut; clear Hcut
+ [1,3: left; split; [1,3: assumption |2: symmetry; assumption]
+ cut (u = S n1); [2: apply le_to_le_to_eq; assumption ]
+ clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
+ cut (s = S (fst (a w)))
+ [2: apply le_to_le_to_eq;
+ [2:assumption
+ | change in H8 with (s + n1 ≤ S (n1 + fst (a w)));
+ rewrite > plus_n_Sm in H8;
+ rewrite > sym_plus in H8;
+ apply le_plus_to_le [2: apply H8]]
+ | cases (H3 (a w) H6);
+ change with (s = fst (a w1));
+ change in H4 with (fst (a w) < fst (a w1));
+ apply le_to_le_to_eq;
+ [ rewrite > Hcut;
+ assumption
+ | apply (os_le_to_nat_le (fst (a w1)) s (H2 w1));]]
+ |*: right; split;
+ [1,3: assumption
+ |2: rewrite > sym_plus in ⊢ (? ? %);
+ rewrite < H6;
+ apply le_plus_r;
+ assumption
+ | cases (H3 (a w) H6);
+ change with (s + S n1 ≤ u + fst (a w1));
+ rewrite < plus_n_Sm;
+ apply (trans_le ? (S (u + fst (a w)))); [ apply le_S_S; assumption]
+ rewrite > plus_n_Sm;
+ apply le_plus; [ apply le_n ]
+ apply H9]]]]]
clearbody m; unfold spec in m; clear spec;
-cut (∀i.fst (a (m i)) = s ∨ i ≤ fst (a (m i))) as key2;[
letin find ≝ (
let rec find i u on u : nat ≝
match u with
apply H6; rewrite < H7; simplify; apply plus_n_Sm;
|2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
|3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
- cases (key2 u); [symmetry;assumption]
- cases Hs; apply le_to_le_to_eq;[2:change with (fst (a (m u)) ≤ fst X); apply os_le_to_nat_le; apply (H2 (m u));]
- apply (trans_le ??? (os_le_to_nat_le ?? H5) H4);
-|4: clearbody find; cases (find O u);
- exists [apply w]; intros; change with (s = fst (a j));
- rewrite > (H4 ?); [2: reflexivity]
- apply le_to_le_to_eq; [apply os_le_to_nat_le;
- apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5));]
- apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);]
- rewrite < (H4 ?); [2: reflexivity] apply le_n;]]
-alias symbol "pi1" (instance 15) = "exT fst".
-alias symbol "pi1" (instance 10) = "exT fst".
-alias symbol "pi1" (instance 7) = "exT fst".
-alias symbol "pi1" (instance 4) = "exT fst".
-alias symbol "nat" = "naturals".
-cut (∀i.fst (a (fst (m i))) = s
- ∨
- i ≤ fst (m i)
- ∧
- match i in nat return λn:ℕ.Prop with
- [O⇒ fst (a (fst(m i))) = fst (a O)
- |S (w:ℕ)⇒fst (a w) < fst (a (fst(m i)))]) as mitico;[2:
- intro; cases (m i); apply H4;]
-cut (∀i.fst (a (m i)) = s ∨ fst (a (m i)) < fst (a (m (S i))));[2:
- intro;
- cases (mitico (S i));
- [2: cases (mitico i);
- [2: cases H5 (H6 _); cases H4 (_ H7); clear H4 H5;
- change in H7 with (fst (a i) < fst (a (fst (m (S i)))));
- right;
-
-
- generalize in match (mitico i); clear mitico;
-
-
- cases (m i); intros; cases H5; clear H5;
- [left; assumption]
- cases H6; clear H6; simplify in H7;
-
- change with (fst (a w)=s ∨ a w<a (m (S i)));
- cases H4; [left; assumption]
- cases H5; clear H4 H5;
- cases (m (S i)); change with (fst (a w)=s ∨ a w<a w1);
- m i = w
- m Si = w1
-
-
-
- elim i;
- [1: cases (m (S O)); change with (fst (a (m O))=s∨a (m O)<a w);
- |2: cases (m (S (S n))); change with (fst (a (m (S n)))=s∨a (m (S n))<a w);
-
- cases H4; clear H4;
- [1: right; split;
- [change with (le nat_ordered_set (fst (a (m O))) (fst (a w)));
- rewrite > H5; apply (H2 (m O));
- |
- |2: cases H5; clear H5; change in H6 with (fst (a O) < fst (a w));
- right; split; [change with (le nat_ordered_set (fst (a (m O))) (fst (a w)));
- apply nat_le_to_os_le; apply le_S_S_to_le; apply le_S;
- (* apply H6; *)
- |]]
-
-
-
- cases (m O); change with (fst (a w) = s ∨ a w < a (m (S O)));
- cases H4[left; assumption] cases H5; clear H4 H5;
- change in H7 with (fst (a w) = fst (a O));
-
-
-intro; elim i; [1: right; apply le_O_n;]
-generalize in match (refl_eq ? (S n):S n = S n);
-generalize in match (S n) in ⊢ (? ? ? % → %); intro R;
-cases (m R); intros; change with (fst (a w) = s ∨ R ≤ fst (a w));
-rewrite < H6 in H5 ⊢ %; clear H6 R; cases H5; [left; assumption]
-cases H6; clear H6 H5; change in H8 with (fst (a n) < fst (a w));
-lapply (key l u a H n w);
-
-w = m (S n)
-
-
-
-STOP
-
-
-letin m ≝ (
- let rec aux i ≝
- match i with
- [ O ⇒
- let a0 ≝ a O in
- match cmp_nat (fst a0) s with
- [ cmp_eq _ ⇒ O
- | cmp_gt nP ⇒ match ? in False return λ_.nat with []
- | cmp_lt nP ⇒ fst (H3 a0 nP)]
- | S m ⇒
- let pred ≝ aux m in
- let apred ≝ a pred in
- match cmp_nat (fst apred) s with
- [ cmp_eq _ ⇒ pred
- | cmp_gt nP ⇒ match ? in False return λ_.nat with []
- | cmp_lt nP ⇒
-
- fst (H3 apred nP)]]
- in aux
- :
- ∀i:nat.∃j:nat.spec i j);unfold spec in aux ⊢ %;
-[1: apply (H2 O nP);
-|2: apply (H2 pred nP);
-|5: left; assumption;
-|6: right; cases (H3 (a O) H5); change with (fst (a O) < fst (a w));
- apply H7;
-|4: right; elim (H3 (a (aux n1)) H5); change with (fst (a (S n1)) < fst (a a1));
- rewrite < H4; elim (aux n1) in H7 ⊢ %; elim H7 in H8; clear H7;
- simplify in H9;
-
-|3: clear H6; generalize in match H5; cases (aux n1); intros; clear H5;
- simplify
-
-
-STOP
-
+ cases (m u); cases H4; clear H4; cases H5; clear H5; [assumption]
+ cases (not_le_Sn_n ? H4)
+]
+clearbody find; cases (find O u);
+exists [apply w]; intros; change with (s = fst (a j));
+rewrite > (H4 ?); [2: reflexivity]
+apply le_to_le_to_eq;
+ [ apply os_le_to_nat_le;
+ apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5));
+ | apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);]
+ rewrite < (H4 ?); [2: reflexivity] apply le_n;]
+qed.
definition nat_uniform_space: uniform_space.
apply (discrete_uniform_space_of_bishop_set ℕ);
exists [1,3:apply x1]
intros; apply H6;
+
projects / helm.git / commitdiff