+sandwich.ma ordered_uniform.ma
+property_sigma.ma ordered_uniform.ma russell_support.ma
+uniform.ma supremum.ma
bishop_set.ma ordered_set.ma
-ordered_set.ma cprop_connectives.ma
-cprop_connectives.ma logic/equality.ma
-bishop_set_rewrite.ma bishop_set.ma
sequence.ma nat/nat.ma
-uniform.ma supremum.ma
-supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma
-nat_ordered_set.ma bishop_set.ma nat/compare.ma
-property_sigma.ma ordered_uniform.ma russell_support.ma
ordered_uniform.ma uniform.ma
+supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma
property_exhaustivity.ma ordered_uniform.ma property_sigma.ma
+bishop_set_rewrite.ma bishop_set.ma
+cprop_connectives.ma logic/equality.ma
+nat_ordered_set.ma bishop_set.ma nat/compare.ma
lebesgue.ma property_exhaustivity.ma sandwich.ma
-sandwich.ma ordered_uniform.ma
+ordered_set.ma cprop_connectives.ma
russell_support.ma cprop_connectives.ma nat/nat.ma
-models/uniformnat.ma bishop_set_rewrite.ma nat/le_arith.ma nat_ordered_set.ma ordered_uniform.ma russell_support.ma uniform.ma
+models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma
+models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma
+models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma
+models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma
+models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma
+models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma
datatypes/constructors.ma
logic/equality.ma
nat/compare.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "uniform.ma".
+include "bishop_set_rewrite.ma".
+
+definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
+intro C; apply (mk_uniform_space C);
+[1: intro;
+ alias symbol "pi2" = "pair pi2".
+ alias symbol "pi1" = "pair pi1".
+ alias symbol "and" = "logical and".
+ apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n));
+|2: intros 4 (U H x Hx); simplify in Hx;
+ cases H (_ H1); cases (H1 x); apply H2; apply Hx;
+|3: intros; cases H (_ PU); cases H1 (_ PV);
+ exists[apply (λx.U x ∧ V x)] split;
+ [1: exists[apply something] intro; cases (PU n); cases (PV n);
+ split; intros; try split;[apply H2;|apply H4] try assumption;
+ apply H3; cases H6; assumption;
+ |2: simplify; intros; assumption;]
+|4: intros; cases H (_ PU); exists [apply U] split;
+ [1: exists [apply something] intro n; cases (PU n);
+ split; intros; try split;[apply H1;|apply H2] assumption;
+ |2: intros 2 (x Hx); cases Hx; cases H1; clear H1;
+ cases (PU 〈(fst x),x1〉); lapply (H4 H2) as H5; simplify in H5;
+ cases (PU 〈x1,(snd x)〉); lapply (H7 H3) as H8; simplify in H8;
+ generalize in match H5; generalize in match H8;
+ generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8;
+ cases x; simplify; intros; cases H1; clear H1; apply H4;
+ apply (eq_trans ???? H3 H2);]
+|5: intros; cases H (_ H1); split; cases x;
+ [2: cases (H1 〈b,b1〉); intro; apply H2; cases (H1 〈b1,b〉);
+ lapply (H6 H4) as H7; apply eq_sym; apply H7;
+ |1: cases (H1 〈b1,b〉); intro; apply H2; cases (H1 〈b,b1〉);
+ lapply (H6 H4) as H7; apply eq_sym; apply H7;]]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "models/nat_uniform.ma".
+include "supremum.ma".
+include "nat/le_arith.ma".
+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; generalize in match (nat_compare_to_Prop n m);
+cases (nat_compare n m); intros;
+[constructor 1|constructor 2|constructor 3] assumption;
+qed.
+
+alias symbol "pi1" = "exT fst".
+alias symbol "leq" = "natural 'less or equal to'".
+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:ℕ.(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
+ | 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 pred nP);
+|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: cases (?: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 ??? 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; try assumption;
+ [1: rewrite > sym_plus in ⊢ (? ? %);
+ rewrite < H6; apply le_plus_r; assumption;
+ |2: cases (H3 (a w) H6);
+ change with (s + S n1 ≤ u + fst (a w1));rewrite < plus_n_Sm;
+ apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
+ apply (le_plus ???? (le_n ?) H9);]]]]]
+clearbody m; unfold spec in m; clear spec;
+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 (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;
+[1: apply os_le_to_nat_le;
+ apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5));
+|2: apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);]
+ rewrite < (H4 ?); [2: reflexivity] apply le_n;]
+qed.
+
+alias symbol "pi1" = "exT fst".
+alias symbol "leq" = "natural 'less or equal to'".
+axiom nat_dedekind_sigma_complete_r:
+ ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing →
+ ∀x.x is_infimum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "lebesgue.ma".
+include "models/nat_order_continuous.ma".
+
+alias symbol "pair" = "dependent pair".
+theorem nat_lebesgue_oc:
+ ∀a:sequence ℕ.∀l,u:nat_ordered_uniform_space.∀H:∀i:nat.a i ∈ [l,u].
+ ∀x:ℕ.a order_converges x →
+ x ∈ [l,u] ∧
+ ∀h:x ∈ [l,u].
+ uniform_converge {[l,u]} (⌊n,〈a n,H n〉⌋) 〈x,h〉.
+intros; apply lebesgue_oc; [apply nat_us_is_oc] assumption;
+qed.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "models/nat_dedekind_sigma_complete.ma".
+include "models/nat_ordered_uniform.ma".
+
+lemma nat_us_is_oc: ∀l,u:ℕ.order_continuity (segment_ordered_uniform_space ℕ l u).
+intros 4; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;
+[1: cases (nat_dedekind_sigma_complete l u a H1 ? H2);
+ exists [apply w1]; intros;
+ apply (restrict nat_ordered_uniform_space l u ??? H4);
+ generalize in match (H ? H5);
+ cases x; intro;
+ generalize in match (refl_eq ? (a i):a i = a i);
+ generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X;
+ intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify;
+ apply (us_phi1 nat_uniform_space ? H3); simplify; apply eq_reflexive;
+|2: cases (nat_dedekind_sigma_complete_r l u a H1 ? H2);
+ exists [apply w1]; intros;
+ apply (restrict nat_ordered_uniform_space l u ??? H4);
+ generalize in match (H ? H5);
+ cases x; intro;
+ generalize in match (refl_eq ? (a i):a i = a i);
+ generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X;
+ intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify;
+ apply (us_phi1 nat_uniform_space ? H3); simplify; apply eq_reflexive;]
+qed.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "models/nat_uniform.ma".
+include "bishop_set_rewrite.ma".
+include "ordered_uniform.ma".
+
+definition nat_ordered_uniform_space:ordered_uniform_space.
+ apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ)));
+simplify; intros 7; cases H3;
+cases H (_); cases (H8 y); apply H9; cases (H8 p);
+lapply (H12 H1) as H13; apply (le_le_eq);
+[1: apply (le_transitive ???? H4); apply (Le≪ ? H13); assumption;
+|2: apply (le_transitive ????? H5); apply (Le≫ (snd p) H13); assumption;]
+qed.
+
+interpretation "Ordered uniform space N" 'nat = nat_ordered_uniform_space.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "nat_ordered_set.ma".
+include "models/discrete_uniformity.ma".
+
+definition nat_uniform_space: uniform_space.
+apply (discrete_uniform_space_of_bishop_set ℕ);
+qed.
+
+interpretation "Uniform space N" 'nat = nat_uniform_space.
\ No newline at end of file
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "nat/le_arith.ma".
-include "nat_ordered_set.ma".
-include "bishop_set_rewrite.ma".
-include "uniform.ma".
-
-definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
-intro C; apply (mk_uniform_space C);
-[1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n));
-|2: intros 4 (U H x Hx); simplify in Hx;
- cases H (_ H1); cases (H1 x); apply H2; apply Hx;
-|3: intros; cases H (_ PU); cases H1 (_ PV);
- exists[apply (λx.U x ∧ V x)] split;
- [1: exists[apply something] intro; cases (PU n); cases (PV n);
- split; intros; try split;[apply H2;|apply H4] try assumption;
- apply H3; cases H6; assumption;
- |2: simplify; intros; assumption;]
-|4: intros; cases H (_ PU); exists [apply U] split;
- [1: exists [apply something] intro n; cases (PU n);
- split; intros; try split;[apply H1;|apply H2] assumption;
- |2: intros 2 (x Hx); cases Hx; cases H1; clear H1;
- cases (PU 〈(fst x),x1〉); lapply (H4 H2) as H5; simplify in H5;
- cases (PU 〈x1,(snd x)〉); lapply (H7 H3) as H8; simplify in H8;
- generalize in match H5; generalize in match H8;
- generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8;
- cases x; simplify; intros; cases H1; clear H1; apply H4;
- apply (eq_trans ???? H3 H2);]
-|5: intros; cases H (_ H1); split; cases x;
- [2: cases (H1 〈b,b1〉); intro; apply H2; cases (H1 〈b1,b〉);
- lapply (H6 H4) as H7; apply eq_sym; apply H7;
- |1: cases (H1 〈b1,b〉); intro; apply H2; cases (H1 〈b,b1〉);
- lapply (H6 H4) as H7; apply eq_sym; apply H7;]]
-qed.
-
-
-notation "\naturals" non associative with precedence 99 for @{'nat}.
-
-interpretation "naturals" 'nat = nat.
-interpretation "Ordered set N" 'nat = nat_ordered_set.
-
-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.
-
-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.(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
- | 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 pred nP);
-|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;
-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 (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 ℕ);
-qed.
-
-interpretation "Uniform space N" 'nat = nat_uniform_space.
-
-include "ordered_uniform.ma".
-
-definition nat_ordered_uniform_space:ordered_uniform_space.
-apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ)));
-simplify; intros 7; cases H3; cases H4; cases H5; clear H5 H4;
-cases H (_); cases (H4 y); apply H5; clear H5 H10; cases (H4 p);
-lapply (H10 H1) as H11; clear H10 H5; apply (le_le_eq);
-[1: apply (le_transitive ???? H6); apply (Le≪ ? H11); assumption;
-|2: apply (le_transitive ????? H7); apply (Le≫ (snd p) H11); assumption;]
-qed.
-
-interpretation "Uniform space N" 'nat = nat_ordered_uniform_space.
-
-lemma nat_us_is_oc: ∀l,u:ℕ.order_continuity {[l,u]}.
-intros 4; split; intros 3; cases H; cases H3; clear H3 H;
-cases (H5 (a i));
-cases (H10 (sig_in ?? x1 H2));
-
-exists [1,3:apply x1]
-intros; apply H6;
-
|2: apply nat_excess_cotransitive]
qed.
+notation "\naturals" non associative with precedence 90 for @{'nat}.
+interpretation "ordered set N" 'nat = nat_ordered_set.
+
alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
lemma os_le_to_nat_le:
∀a,b:nat_ordered_set.a ≤ b → le a b.
projects / helm.git / commitdiff
