+++ /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 (∃d:unit.∀n:C squareB.(\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".
-
-lemma hint1:
- ∀s.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set s))
- → sequence (hos_carr (os_l (segment_ordered_set nat_ordered_set s))).
-intros; assumption;
-qed.
-
-coercion hint1 nocomposites.
-
-alias symbol "pi1" = "exT \fst".
-alias symbol "N" = "ordered set N".
-lemma increasing_supremum_stabilizes:
- ∀sg:‡ℕ.∀a:sequence {[sg]}.
- a is_increasing →
- ∀X.X is_supremum a → ∃i.∀j.i ≤ j → \fst X = \fst (a j).
-intros 4; cases X (x Hx); clear X; letin X ≝ ≪x,Hx≫;
-fold normalize X; intros; cases H1;
-alias symbol "N" = "Natural numbers".
-letin spec ≝ (λi,j:ℕ.(𝕦_sg ≤ i ∧ x = \fst (a j)) ∨ (i < 𝕦_sg ∧ x + i ≤ 𝕦_sg + \fst (a j)));
-(* x - 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 x (\fst apred) with
- [ cmp_le _ ⇒ pred
- | cmp_gt nP ⇒ \fst (H3 apred ?)]]
- in aux
- :
- ∀i:nat.∃j:nat.spec i j));[whd; apply nP;] unfold spec in aux ⊢ %;
-[3: unfold X in H2; clear H4 n aux spec H3 H1 H X;
- cases (cases_in_segment ??? Hx);
- elim 𝕦_sg in H1 ⊢ %; intros (a Hs H);
- [1: left; split; [apply le_n]
- generalize in match H;
- generalize in match Hx;
- rewrite > (?:x = O);
- [2: cases Hx; lapply (os_le_to_nat_le ?? H1);
- apply (symmetric_eq nat O x ?).apply (le_n_O_to_eq x ?).apply (Hletin).
- |1: intros; unfold Type_of_ordered_set in sg;
- lapply (H2 O) as K; lapply (sl2l_ ?? (a O) ≪x,Hx≫ K) as P;
- simplify in P:(???%); lapply (le_transitive ??? P H1) as W;
- lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);]
- |2: right; cases Hx; rewrite > (sym_plus x O); split; [apply le_S_S; apply le_O_n];
- apply (trans_le ??? (os_le_to_nat_le ?? H3));
- apply le_plus_n_r;]
-|2: clear H6; cut (x = \fst (a (aux n1))); [2:
- cases (le_to_or_lt_eq ?? H5); [2: assumption]
- cases (?:False); apply (H2 (aux n1) H6);] clear H5;
- generalize in match Hcut; clear Hcut; intro H5;
-|1: clear H6]
-[2,1:
- cases (aux n1) in H5 ⊢ %; 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);
- |*: cases (cmp_nat 𝕦_sg (S n1));
- [1,3: left; split; [1,3: assumption |2: assumption]
- cut (𝕦_sg = S n1); [2: apply le_to_le_to_eq; assumption ]
- clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
- cut (x = S (\fst (a w)));
- [2: apply le_to_le_to_eq; [2: assumption]
- change in H8 with (x + 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 (x = \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)) x (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 (x + S n1 ≤ 𝕦_sg + \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))) x with
- [ true ⇒ (m i:nat)
- | false ⇒ find (S i) w]]
- in find
- :
- ∀i,bound.∃j.i + bound = 𝕦_sg → x = \fst (a j));
-[1: cases (find (S n) n2); intro; change with (x = \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 𝕦_sg); cases H4; clear H4; cases H5; clear H5; [assumption]
- cases (not_le_Sn_n ? H4)]
-clearbody find; cases (find O 𝕦_sg);
-exists [apply w]; intros; change with (x = \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 ? x ?);[apply os_le_to_nat_le; apply (H2 j);]
- rewrite < (H4 ?); [2: reflexivity] apply le_n;]
-qed.
-
-lemma hint2:
- ∀s.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set s))
- → sequence (hos_carr (os_r (segment_ordered_set nat_ordered_set s))).
-intros; assumption;
-qed.
-
-coercion hint2 nocomposites.
-
-alias symbol "N" = "ordered set N".
-axiom increasing_supremum_stabilizes_r:
- ∀s:‡ℕ.∀a:sequence {[s]}.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".
-
-theorem nat_lebesgue_oc:
- ∀a:sequence ℕ.∀s:‡ℕ.∀H:∀i:nat.a i ∈ s.
- ∀x:ℕ.a order_converges x →
- x ∈ s ∧
- ∀h:x ∈ s.
- uniform_converge {[s]} ⌊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/increasing_supremum_stabilizes.ma".
-include "models/nat_ordered_uniform.ma".
-
-lemma nat_us_is_oc: ∀s:‡ℕ.order_continuity (segment_ordered_uniform_space ℕ s).
-intros 3; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;
-[1: cases (increasing_supremum_stabilizes s a H1 ? H2);
- exists [apply w1]; intros;
- apply (restrict nat_ordered_uniform_space s ??? 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 (us_carr nat_uniform_space));
-|2: cases (increasing_supremum_stabilizes_r s a H1 ? H2);
- exists [apply w1]; intros;
- apply (restrict nat_ordered_uniform_space s ??? 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 (us_carr nat_uniform_space));]
-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 10; cases H (_); cases (H7 y); apply H8; cases (H7 s);
-lapply (H11 H1) as H13; apply (le_le_eq);
-[2: apply (le_transitive ??? H5); apply (Le≪ ? H13); assumption;
-|1: assumption;
-|3: change with (le (os_r ℕ) (\snd y) (\fst y));
- apply (ge_transitive ??? H5);apply (ge_transitive ???? H4);
- change with (le (os_l ℕ) (\fst s) (\snd s));
- apply (Le≫ ? H13); apply le_reflexive;
-|4: assumption;]
-qed.
-
-interpretation "Ordered uniform space N" 'N = 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" 'N = nat_uniform_space.
\ No newline at end of file
projects / helm.git / commitdiff