(* *)
(**************************************************************************)
-include "datatypes/constructors.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
+ | cmp_gt : m < n → cmp_cases n m.
+
+lemma cmp_nat: ∀n,m.cmp_cases n m.
+intros;
+simplify; intros; generalize in match (nat_compare_to_Prop n m);
+cases (nat_compare n m); intros;
+[constructor 1|constructor 2|constructor 3]
+assumption;
+qed.
+
+lemma trans_le_lt_lt:
+ ∀n,m,o:nat.n≤m→m<o→n<o.
+intros; apply (trans_le ? (S m)); [apply le_S_S;apply H;|apply H1]
+qed.
+
+alias symbol "lt" (instance 2) = "ordered sets less than".
+lemma key:
+ ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → ∀n,m. a n < a m → 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)));
+ 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);
+ apply nat_le_to_os_le; apply le_S_S_to_le; apply le_S; apply H2]]
+qed.
+
+lemma le_lt_transitive:
+ ∀O:ordered_set.∀a,b,c:O.a≤b→b<c→a<c.
+intros;
+split;
+[1: apply (le_transitive ???? H); cases H1; assumption;
+|2: cases H1; cases (bs_cotransitive ??? a H3); [2:assumption]
+ cut (a<b);[2: split; [assumption] apply bs_symmetric; assumption]
+ cut (a<c);[2: apply (lt_transitive ???? Hcut H1);]
+ cases Hcut1; assumption]
+qed.
+
+alias symbol "pi1" = "sigma pi1".
lemma nat_dedekind_sigma_complete:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
- ∀x.x is_supremum a → ∃i.∀j.i ≤ j → x ≈ a j.
-intros 5; cases x; clear x; intros;
-cases H2;
+ ∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
+intros 5; cases x (s Hs); clear x; letin X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) s Hs);
+fold normalize X; intros; cases H1;
+alias symbol "pi1" = "sigma pi1".
+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 ≝ (
let rec aux i ≝
match i with
- [ O ⇒ match eqb (fst (a O)) x1 with
- [ true ⇒ O
- | false ⇒ match H4 (a O) ? with
- [ ex_introT n _ ⇒ n]]
- | S m ⇒ let pred ≝ aux m in
- match eqb (fst (a pred)) x1 with
- [ true ⇒ pred
- | false ⇒ match H4 (a pred) ? with
- [ ex_introT n _ ⇒ n]]]
- in aux
+ [ O ⇒ O
+ | 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.a j = x1 ∨ a i < a j);
-
-cases (∀n.a n = x1 ∨ x1 ≰ a n);
-
- elim x1 in H1 ⊢ % 0;
-[1: intro H2; letin X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) O H2); intros;
- fold unfold X X in H1 ⊢ %;
- exists [apply O] cases H1; intros; apply le_le_eq;[2: apply H3;]
- intro; alias symbol "pi1" = "sigma pi1".
- change in H6 with (fst (a j) < O);
- apply (not_le_Sn_O (fst (a j))); apply H6;
-|2: intros 3; letin S_X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) (S n) H2); intros;
- fold unfold S_X S_X in H3 ⊢ %;
- generalize in match (leb_to_Prop l n); elim (leb l n); simplify in H4;
- [1: cut (n ≤ u); [2: cases H2; normalize in H5 ⊢ %;
- apply le_S_S_to_le; lapply (not_lt_to_le ?? H5) as XX;
- apply le_S; apply XX;]
- cases H1; [2:split; apply nat_le_to_os_le; assumption|3:simplify;
+ ∀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);]]]]]
+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
+ [ O ⇒ (m i:nat)
+ | S w ⇒ match eqb (fst (a (m i))) s with
+ [ true ⇒ (m i:nat)
+ | false ⇒ find (S i) w]]
+ in find
+ :
+ ∀i,bound.∃j.i + bound = u → s = fst (a j));
+[1: cases (find (S n) n2); intro; change with (s = fst (a w));
+ 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)
+
- elim (or_lt_le (S n) l);
- [ cases (?:l = S n ∨ l < S n);[
- unfold lt; cases H2; normalize in H5;
- apply (Right (eq nat n (S n)) (lt n (S n)) ?).apply (not_le_to_lt (S n) n ?).apply (not_le_Sn_n n).]
- [ destruct H4;
-
- ∀x.∃i.x ≰ a i ∨ x ≤ a i.
-intros; elim x;
+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
+
definition nat_uniform_space: uniform_space.
apply (discrete_uniform_space_of_bishop_set ℕ);
projects / helm.git / commitdiff