+++ /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 "ordered_set.ma".
-
-(* Definition 2.2, setoid *)
-record bishop_set: Type ≝ {
- bs_carr:> Type;
- bs_apart: bs_carr → bs_carr → CProp;
- bs_coreflexive: coreflexive ? bs_apart;
- bs_symmetric: symmetric ? bs_apart;
- bs_cotransitive: cotransitive ? bs_apart
-}.
-
-interpretation "bishop set apartness" 'apart x y = (bs_apart _ x y).
-
-definition bishop_set_of_ordered_set: ordered_set → bishop_set.
-intros (E); apply (mk_bishop_set E (λa,b:E. a ≰ b ∨ b ≰ a));
-[1: intro x; simplify; intro H; cases H; clear H;
- apply (exc_coreflexive x H1);
-|2: intros 3 (x y H); simplify in H ⊢ %; cases H; [right|left]assumption;
-|3: intros 4 (x y z H); simplify in H ⊢ %; cases H; clear H;
- [ cases (exc_cotransitive x y z H1); [left;left|right;left] assumption;
- | cases (exc_cotransitive y x z H1); [right;right|left;right] assumption;]]
-qed.
-
-(* Definition 2.2 (2) *)
-definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b).
-
-interpretation "Bishop set alikeness" 'napart a b = (eq _ a b).
-
-lemma eq_reflexive:∀E:bishop_set. reflexive ? (eq E).
-intros (E); unfold; intros (x); apply bs_coreflexive;
-qed.
-
-lemma eq_sym_:∀E:bishop_set.symmetric ? (eq E).
-intros 4 (E x y H); intro T; cases (H (bs_symmetric ??? T));
-qed.
-
-lemma eq_sym:∀E:bishop_set.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_.
-
-lemma eq_trans_: ∀E:bishop_set.transitive ? (eq E).
-intros 6 (E x y z Exy Eyz); intro Axy; cases (bs_cotransitive ???y Axy);
-[apply Exy|apply Eyz] assumption.
-qed.
-
-coercion bishop_set_of_ordered_set.
-
-lemma le_antisymmetric:
- ∀E:ordered_set.antisymmetric E (le (os_l E)) (eq E).
-intros 5 (E x y Lxy Lyx); intro H;
-cases H; [apply Lxy;|apply Lyx] assumption;
-qed.
-
-lemma le_le_eq: ∀E:ordered_set.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
-intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
-qed.
-
-definition bs_subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
-
-interpretation "bishop set subset" 'subseteq a b = (bs_subset _ a b).
-
-definition square_bishop_set : bishop_set → bishop_set.
-intro S; apply (mk_bishop_set (S × S));
-[1: intros (x y); apply ((\fst x # \fst y) ∨ (\snd x # \snd y));
-|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);
-|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X);
-|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
- [1: cases (bs_cotransitive ??? (\fst z) X); [left;left|right;left]assumption;
- |2: cases (bs_cotransitive ??? (\snd z) X); [left;right|right;right]assumption;]]
-qed.
-
-notation "s 2 \atop \neq" non associative with precedence 90
- for @{ 'square_bs $s }.
-notation > "s 'squareB'" non associative with precedence 90
- for @{ 'squareB $s }.
-interpretation "bishop set square" 'squareB x = (square_bishop_set x).
-interpretation "bishop set square" 'square_bs x = (square_bishop_set x).
\ 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 "bishop_set.ma".
-
-coercion eq_sym.
-
-lemma eq_trans:∀E:bishop_set.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝
- λE,x,y,z.eq_trans_ E x z y.
-
-notation > "'Eq'≈" non associative with precedence 50
- for @{'eqrewrite}.
-
-interpretation "eq_rew" 'eqrewrite = (eq_trans _ _ _).
-
-lemma le_rewl: ∀E:ordered_set.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z.
-intros (E z y x Exy Lxz); apply (le_transitive ??? ? Lxz);
-intro Xyz; apply Exy; right; assumption;
-qed.
-
-lemma le_rewr: ∀E:ordered_set.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y.
-intros (E z y x Exy Lxz); apply (le_transitive ??? Lxz);
-intro Xyz; apply Exy; left; assumption;
-qed.
-
-notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}.
-interpretation "le_rewl" 'lerewritel = (le_rewl _ _ _).
-notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}.
-interpretation "le_rewr" 'lerewriter = (le_rewr _ _ _).
-
-lemma ap_rewl: ∀A:bishop_set.∀x,z,y:A. x ≈ y → y # z → x # z.
-intros (A x z y Exy Ayz); cases (bs_cotransitive ???x Ayz); [2:assumption]
-cases (eq_sym ??? Exy H);
-qed.
-
-lemma ap_rewr: ∀A:bishop_set.∀x,z,y:A. x ≈ y → z # y → z # x.
-intros (A x z y Exy Azy); apply bs_symmetric; apply (ap_rewl ???? Exy);
-apply bs_symmetric; assumption;
-qed.
-
-notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}.
-interpretation "ap_rewl" 'aprewritel = (ap_rewl _ _ _).
-notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}.
-interpretation "ap_rewr" 'aprewriter = (ap_rewr _ _ _).
-
-lemma exc_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
-intros (A x z y Exy Ayz); cases (exc_cotransitive ?? x Ayz); [2:assumption]
-cases Exy; right; assumption;
-qed.
-
-lemma exc_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x.
-intros (A x z y Exy Azy); cases (exc_cotransitive ??x Azy); [assumption]
-cases (Exy); left; assumption;
-qed.
-
-notation > "'Ex'≪" non associative with precedence 50 for @{'ordered_setrewritel}.
-interpretation "exc_rewl" 'ordered_setrewritel = (exc_rewl _ _ _).
-notation > "'Ex'≫" non associative with precedence 50 for @{'ordered_setrewriter}.
-interpretation "exc_rewr" 'ordered_setrewriter = (exc_rewr _ _ _).
-
-(*
-lemma lt_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z < y → z < x.
-intros (A x y z E H); split; cases H;
-[apply (Le≫ ? (eq_sym ??? E));|apply (Ap≫ ? E)] assumption;
-qed.
-
-lemma lt_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y < z → x < z.
-intros (A x y z E H); split; cases H;
-[apply (Le≪ ? (eq_sym ??? E));| apply (Ap≪ ? E);] assumption;
-qed.
-
-notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
-interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
-notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
-interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
-*)
-property_exhaustivity.ma ordered_uniform.ma property_sigma.ma
-sequence.ma nat/nat.ma
-supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma
-bishop_set_rewrite.ma bishop_set.ma
-property_sigma.ma ordered_uniform.ma russell_support.ma
models/q_support.ma Q/q/qplus.ma Q/q/qtimes.ma logic/cprop_connectives.ma
-models/increasing_supremum_stabilizes.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma
-ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma
-sandwich.ma ordered_uniform.ma
-nat_ordered_set.ma bishop_set.ma nat/compare.ma
-models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma
+models/q_bars.ma dama/nat_ordered_set.ma logic/cprop_connectives.ma models/list_support.ma models/q_support.ma
models/list_support.ma list/list.ma logic/cprop_connectives.ma nat/minus.ma
-models/q_bars.ma logic/cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma
.unnamed.ma
-lebesgue.ma ordered_set.ma property_exhaustivity.ma sandwich.ma
-bishop_set.ma ordered_set.ma
-models/nat_order_continuous.ma models/increasing_supremum_stabilizes.ma models/nat_ordered_uniform.ma
-models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma
-russell_support.ma logic/cprop_connectives.ma nat/nat.ma
models/q_copy.ma models/q_bars.ma
-models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma
-models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma
-ordered_uniform.ma uniform.ma
-uniform.ma supremum.ma
-models/q_rebase.ma Q/q/qtimes.ma models/q_copy.ma russell_support.ma
+models/q_rebase.ma Q/q/qtimes.ma dama/russell_support.ma models/q_copy.ma
Q/q/qplus.ma
Q/q/qtimes.ma
-datatypes/constructors.ma
+dama/nat_ordered_set.ma
+dama/russell_support.ma
list/list.ma
logic/cprop_connectives.ma
-nat/compare.ma
-nat/le_arith.ma
nat/minus.ma
-nat/nat.ma
-nat/plus.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 *)
-(* *)
-(**************************************************************************)
-
-(* manca un pezzo del pullback, se inverto poi non tipa *)
-include "sandwich.ma".
-include "property_exhaustivity.ma".
-
-(* NOT DUALIZED *)
-alias symbol "low" = "lower".
-alias id "le" = "cic:/matita/dama/ordered_set/le.con".
-lemma order_converges_bigger_lowsegment:
- ∀C:ordered_set.
- ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s.
- ∀x:C.∀p:order_converge C a x.
- ∀j. 𝕝_s ≤ (pi1exT23 ???? p j).
-intros; cases p (xi yi Ux Dy Hxy); clear p; simplify;
-cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
-cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
-intro H2; cases (SSa 𝕝_s H2) (w Hw); simplify in Hw;
-lapply (H (w+j)) as K; cases (cases_in_segment ? s ? K); apply H3; apply Hw;
-qed.
-
-alias symbol "upp" = "uppper".
-alias symbol "leq" = "Ordered set less or equal than".
-lemma order_converges_smaller_upsegment:
- ∀C:ordered_set.
- ∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s.
- ∀x:C.∀p:order_converge C a x.
- ∀j. (pi2exT23 ???? p j) ≤ 𝕦_s.
-intros; cases p (xi yi Ux Dy Hxy); clear p; simplify;
-cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
-cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
-intro H2; cases (SIa 𝕦_s H2) (w Hw); lapply (H (w+j)) as K;
-cases (cases_in_segment ? s ? K); apply H1; apply Hw;
-qed.
-
-(* Theorem 3.10 *)
-theorem lebesgue_oc:
- ∀C:ordered_uniform_space.
- (∀s:‡C.order_continuity {[s]}) →
- ∀a:sequence C.∀s:‡C.∀H:∀i:nat.a i ∈ s.
- ∀x:C.a order_converges x →
- x ∈ s ∧
- ∀h:x ∈ s.
- uniform_converge {[s]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
-intros;
-generalize in match (order_converges_bigger_lowsegment ? a s H1 ? H2);
-generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
-cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
-cut (∀i.xi i ∈ s) as Hxi; [2:
- intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
- lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
- simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
-cut (∀i.yi i ∈ s) as Hyi; [2:
- intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
- lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
- apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
-split;
-[1: apply (uparrow_to_in_segment s ? Hxi ? Hx);
-|2: intros 3 (h);
- letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
- letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
- letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
- apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;]
- [1: intro j; cases (Hxy j); cases H3; cases H4; split; clear H3 H4; simplify in H5 H7;
- [apply (l2sl_ ? s (Xi j) (Ai j) (H5 0));|apply (l2sl_ ? s (Ai j) (Yi j) (H7 0))]
- |2: cases (H s Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [intro i; apply (l2sl_ ? s (Xi i) (Xi (S i)) (H3 i));]
- cases H4; split; [intro i; apply (l2sl_ ? s (Xi i) ≪x,h≫ (H5 i))]
- intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x_ ? s ? y Hy)]
- exists [apply w] apply (x2sx_ ? s (Xi w) y H7);
- |3: cases (H s Yi ≪?,h≫) (Ux Uy); apply Uy; cases Hy; split; [intro i; apply (l2sl_ ? s (Yi (S i)) (Yi i) (H3 i));]
- cases H4; split; [intro i; apply (l2sl_ ? s ≪x,h≫ (Yi i) (H5 i))]
- intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x_ ? s y ≪x,h≫ Hy)]
- exists [apply w] apply (x2sx_ ? s y (Yi w) H7);]]
-qed.
-
-
-(* Theorem 3.9 *)
-theorem lebesgue_se:
- ∀C:ordered_uniform_space.property_sigma C →
- (∀s:‡C.exhaustive {[s]}) →
- ∀a:sequence C.∀s:‡C.∀H:∀i:nat.a i ∈ s.
- ∀x:C.a order_converges x →
- x ∈ s ∧
- ∀h:x ∈ s.
- uniform_converge {[s]} (⌊n,≪a n,H n≫⌋) ≪x,h≫.
-intros (C S);
-generalize in match (order_converges_bigger_lowsegment ? a s H1 ? H2);
-generalize in match (order_converges_smaller_upsegment ? a s H1 ? H2);
-cases H2 (xi yi Hx Hy Hxy); clear H2; simplify in ⊢ ((?→???%) → (?→???%) → ?); intros;
-cut (∀i.xi i ∈ s) as Hxi; [2:
- intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
- lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
- simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
-cut (∀i.yi i ∈ s) as Hyi; [2:
- intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
- lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
- apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
-letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
-letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
-cases (restrict_uniform_convergence_uparrow ? S ? (H s) Xi x Hx);
-cases (restrict_uniform_convergence_downarrow ? S ? (H s) Yi x Hy);
-split; [1: assumption]
-intros 3;
-lapply (uparrow_upperlocated xi x Hx)as Ux;
-lapply (downarrow_lowerlocated yi x Hy)as Uy;
-letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
-apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;|2:apply H3;|3:apply H5]
-intro j; cases (Hxy j); cases H7; cases H8; split;
-[apply (l2sl_ ? s (Xi j) (Ai j) (H9 0));|apply (l2sl_ ? s (Ai j) (Yi j) (H11 0))]
-qed.
-
-
-
(* *)
(**************************************************************************)
-include "nat_ordered_set.ma".
+include "dama/nat_ordered_set.ma".
include "models/q_support.ma".
include "models/list_support.ma".
include "logic/cprop_connectives.ma".
(* *)
(**************************************************************************)
-include "russell_support.ma".
+include "dama/russell_support.ma".
include "models/q_copy.ma".
(*
definition rebase_spec ≝
+++ /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/compare.ma".
-include "bishop_set.ma".
-
-definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
-
-lemma nat_elim2:
- ∀R:nat → nat → CProp.
- (∀ n:nat. R O n) → (∀n:nat. R (S n) O) → (∀n,m:nat. R n m → R (S n) (S m)) →
- ∀n,m:nat. R n m.
-intros 5;elim n; [apply H]
-cases m;[ apply H1| apply H2; apply H3 ]
-qed.
-
-alias symbol "lt" = "natural 'less than'".
-lemma nat_discriminable: ∀x,y:nat.x < y ∨ x = y ∨ y < x.
-intros (x y); apply (nat_elim2 ???? x y);
-[1: intro;left;cases n; [right;reflexivity] left; apply lt_O_S;
-|2: intro;right;apply lt_O_S;
-|3: intros; cases H;
- [1: cases H1; [left; left; apply le_S_S; assumption]
- left;right;rewrite > H2; reflexivity;
- |2: right;apply le_S_S; assumption]]
-qed.
-
-lemma nat_excess_cotransitive: cotransitive ? nat_excess.
-intros 3 (x y z); unfold nat_excess; simplify; intros;
-cases (nat_discriminable x z); [2: left; assumption] cases H1; clear H1;
-[1: right; apply (trans_lt ??? H H2);
-|2: right; rewrite < H2; assumption;]
-qed.
-
-lemma nat_ordered_set : ordered_set.
-letin hos ≝ (mk_half_ordered_set nat (λT,R:Type.λf:T→T→R.f) ? nat_excess ? nat_excess_cotransitive);
-[ intros; left; intros; reflexivity;
-| intro x; intro H; apply (not_le_Sn_n ? H);]
-constructor 1; apply hos;
-qed.
-
-interpretation "ordered set N" 'N = 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.
-intros; normalize in H; apply (not_lt_to_le b a H);
-qed.
-
-lemma nat_le_to_os_le:
- ∀a,b:nat_ordered_set.le a b → a ≤ b.
-intros 3; apply (le_to_not_lt a b);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 "datatypes/constructors.ma".
-include "logic/cprop_connectives.ma".
-
-
-(* TEMPLATES
-notation "''" non associative with precedence 90 for @{'}.
-notation "''" non associative with precedence 90 for @{'}.
-
-interpretation "" ' = ( (os_l _)).
-interpretation "" ' = ( (os_r _)).
-*)
-
-(* Definition 2.1 *)
-record half_ordered_set: Type ≝ {
- hos_carr:> Type;
- wloss: ∀A,B:Type. (A → A → B) → A → A → B;
- wloss_prop: (∀T,R,P,x,y.P x y = wloss T R P x y) ∨ (∀T,R,P,x,y.P y x = wloss T R P x y);
- hos_excess_: hos_carr → hos_carr → CProp;
- hos_coreflexive: coreflexive ? (wloss ?? hos_excess_);
- hos_cotransitive: cotransitive ? (wloss ?? hos_excess_)
-}.
-
-definition hos_excess ≝ λO:half_ordered_set.wloss O ?? (hos_excess_ O).
-
-definition dual_hos : half_ordered_set → half_ordered_set.
-intro; constructor 1;
-[ apply (hos_carr h);
-| apply (λT,R,f,x,y.wloss h T R f y x);
-| intros; cases (wloss_prop h);[right|left]intros;apply H;
-| apply (hos_excess_ h);
-| apply (hos_coreflexive h);
-| intros 4 (x y z H); simplify in H ⊢ %; cases (hos_cotransitive h y x z H);
- [right|left] assumption;]
-qed.
-
-record ordered_set : Type ≝ {
- os_l : half_ordered_set
-}.
-
-definition os_r : ordered_set → half_ordered_set.
-intro o; apply (dual_hos (os_l o)); qed.
-
-lemma half2full : half_ordered_set → ordered_set.
-intro hos;
-constructor 1; apply hos;
-qed.
-
-definition Type_of_ordered_set : ordered_set → Type.
-intro o; apply (hos_carr (os_l o)); qed.
-
-definition Type_of_ordered_set_dual : ordered_set → Type.
-intro o; apply (hos_carr (os_r o)); qed.
-
-coercion Type_of_ordered_set_dual.
-coercion Type_of_ordered_set.
-
-notation "a ≰≰ b" non associative with precedence 45 for @{'nleq_low $a $b}.
-interpretation "Ordered half set excess" 'nleq_low a b = (hos_excess _ a b).
-
-interpretation "Ordered set excess (dual)" 'ngeq a b = (hos_excess (os_r _) a b).
-interpretation "Ordered set excess" 'nleq a b = (hos_excess (os_l _) a b).
-
-notation "'exc_coreflexive'" non associative with precedence 90 for @{'exc_coreflexive}.
-notation "'cxe_coreflexive'" non associative with precedence 90 for @{'cxe_coreflexive}.
-
-interpretation "exc_coreflexive" 'exc_coreflexive = ((hos_coreflexive (os_l _))).
-interpretation "cxe_coreflexive" 'cxe_coreflexive = ((hos_coreflexive (os_r _))).
-
-notation "'exc_cotransitive'" non associative with precedence 90 for @{'exc_cotransitive}.
-notation "'cxe_cotransitive'" non associative with precedence 90 for @{'cxe_cotransitive}.
-
-interpretation "exc_cotransitive" 'exc_cotransitive = ((hos_cotransitive (os_l _))).
-interpretation "cxe_cotransitive" 'cxe_cotransitive = ((hos_cotransitive (os_r _))).
-
-(* Definition 2.2 (3) *)
-definition le ≝ λE:half_ordered_set.λa,b:E. ¬ (a ≰≰ b).
-
-notation "hvbox(a break ≤≤ b)" non associative with precedence 45 for @{ 'leq_low $a $b }.
-interpretation "Half ordered set greater or equal than" 'leq_low a b = ((le _ a b)).
-
-interpretation "Ordered set greater or equal than" 'geq a b = ((le (os_r _) a b)).
-interpretation "Ordered set less or equal than" 'leq a b = ((le (os_l _) a b)).
-
-lemma hle_reflexive: ∀E.reflexive ? (le E).
-unfold reflexive; intros 3; apply (hos_coreflexive ? x H);
-qed.
-
-notation "'le_reflexive'" non associative with precedence 90 for @{'le_reflexive}.
-notation "'ge_reflexive'" non associative with precedence 90 for @{'ge_reflexive}.
-
-interpretation "le reflexive" 'le_reflexive = (hle_reflexive (os_l _)).
-interpretation "ge reflexive" 'ge_reflexive = (hle_reflexive (os_r _)).
-
-(* DUALITY TESTS
-lemma test_le_ge_convertible :∀o:ordered_set.∀x,y:o. x ≤ y → y ≥ x.
-intros; assumption; qed.
-
-lemma test_ge_reflexive :∀o:ordered_set.∀x:o. x ≥ x.
-intros; apply ge_reflexive. qed.
-
-lemma test_le_reflexive :∀o:ordered_set.∀x:o. x ≤ x.
-intros; apply le_reflexive. qed.
-*)
-
-lemma hle_transitive: ∀E.transitive ? (le E).
-unfold transitive; intros 7 (E x y z H1 H2 H3); cases (hos_cotransitive E x z y H3) (H4 H4);
-[cases (H1 H4)|cases (H2 H4)]
-qed.
-
-notation "'le_transitive'" non associative with precedence 90 for @{'le_transitive}.
-notation "'ge_transitive'" non associative with precedence 90 for @{'ge_transitive}.
-
-interpretation "le transitive" 'le_transitive = (hle_transitive (os_l _)).
-interpretation "ge transitive" 'ge_transitive = (hle_transitive (os_r _)).
-
-(* Lemma 2.3 *)
-lemma exc_hle_variance:
- ∀O:half_ordered_set.∀a,b,a',b':O.a ≰≰ b → a ≤≤ a' → b' ≤≤ b → a' ≰≰ b'.
-intros (O a b a1 b1 Eab Laa1 Lb1b);
-cases (hos_cotransitive ? a b a1 Eab) (H H); [cases (Laa1 H)]
-cases (hos_cotransitive ? ?? b1 H) (H1 H1); [assumption]
-cases (Lb1b H1);
-qed.
-
-notation "'exc_le_variance'" non associative with precedence 90 for @{'exc_le_variance}.
-notation "'exc_ge_variance'" non associative with precedence 90 for @{'exc_ge_variance}.
-
-interpretation "exc_le_variance" 'exc_le_variance = (exc_hle_variance (os_l _)).
-interpretation "exc_ge_variance" 'exc_ge_variance = (exc_hle_variance (os_r _)).
-
-definition square_exc ≝
- λO:half_ordered_set.λx,y:O×O.\fst x ≰≰ \fst y ∨ \snd x ≰≰ \snd y.
-
-lemma square_half_ordered_set: half_ordered_set → half_ordered_set.
-intro O;
-apply (mk_half_ordered_set (O × O));
-[1: apply (wloss O);
-|2: intros; cases (wloss_prop O); [left|right] intros; apply H;
-|3: apply (square_exc O);
-|4: intro x; cases (wloss_prop O); rewrite < (H ?? (square_exc O) x x); clear H;
- cases x; clear x; unfold square_exc; intro H; cases H; clear H; simplify in H1;
- [1,3: apply (hos_coreflexive O h H1);
- |*: apply (hos_coreflexive O h1 H1);]
-|5: intros 3 (x0 y0 z0); cases (wloss_prop O);
- do 3 rewrite < (H ?? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0;
- simplify; intro H; cases H; clear H;
- [1: cases (hos_cotransitive ? h h2 h4 H1); [left;left|right;left] assumption;
- |2: cases (hos_cotransitive ? h1 h3 h5 H1); [left;right|right;right] assumption;
- |3: cases (hos_cotransitive ? h2 h h4 H1); [right;left|left;left] assumption;
- |4: cases (hos_cotransitive ? h3 h1 h5 H1); [right;right|left;right] assumption;]]
-qed.
-
-lemma square_ordered_set: ordered_set → ordered_set.
-intro O; constructor 1; apply (square_half_ordered_set (os_l O));
-qed.
-
-notation "s 2 \atop \nleq" non associative with precedence 90
- for @{ 'square_os $s }.
-notation > "s 'squareO'" non associative with precedence 90
- for @{ 'squareO $s }.
-interpretation "ordered set square" 'squareO s = (square_ordered_set s).
-interpretation "ordered set square" 'square_os s = (square_ordered_set s).
-
-definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
-
-interpretation "ordered set subset" 'subseteq a b = (os_subset _ a b).
-
+++ /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".
-
-record ordered_uniform_space_ : Type ≝ {
- ous_os:> ordered_set;
- ous_us_: uniform_space;
- with_ : us_carr ous_us_ = bishop_set_of_ordered_set ous_os
-}.
-
-lemma ous_unifspace: ordered_uniform_space_ → uniform_space.
-intro X; apply (mk_uniform_space (bishop_set_of_ordered_set X));
-unfold bishop_set_OF_ordered_uniform_space_;
-[1: rewrite < (with_ X); simplify; apply (us_unifbase (ous_us_ X));
-|2: cases (with_ X); simplify; apply (us_phi1 (ous_us_ X));
-|3: cases (with_ X); simplify; apply (us_phi2 (ous_us_ X));
-|4: cases (with_ X); simplify; apply (us_phi3 (ous_us_ X));
-|5: cases (with_ X); simplify; apply (us_phi4 (ous_us_ X))]
-qed.
-
-coercion ous_unifspace.
-
-record ordered_uniform_space : Type ≝ {
- ous_stuff :> ordered_uniform_space_;
- ous_convex_l: ∀U.us_unifbase ous_stuff U → convex (os_l ous_stuff) U;
- ous_convex_r: ∀U.us_unifbase ous_stuff U → convex (os_r ous_stuff) U
-}.
-
-definition half_ordered_set_OF_ordered_uniform_space : ordered_uniform_space → half_ordered_set.
-intro; compose ordered_set_OF_ordered_uniform_space with os_l. apply (f o);
-qed.
-
-definition invert_os_relation ≝
- λC:ordered_set.λU:C squareO → Prop.
- λx:C squareO. U 〈\snd x,\fst x〉.
-
-interpretation "relation invertion" 'invert a = (invert_os_relation _ a).
-interpretation "relation invertion" 'invert_symbol = (invert_os_relation _).
-interpretation "relation invertion" 'invert_appl a x = (invert_os_relation _ a x).
-
-lemma hint_segment: ∀O.
- segment (Type_of_ordered_set O) →
- segment (hos_carr (os_l O)).
-intros; assumption;
-qed.
-
-coercion hint_segment nocomposites.
-
-lemma segment_square_of_ordered_set_square:
- ∀O:ordered_set.∀s:‡O.∀x:O squareO.
- \fst x ∈ s → \snd x ∈ s → {[s]} squareO.
-intros; split; exists; [1: apply (\fst x) |3: apply (\snd x)] assumption;
-qed.
-
-coercion segment_square_of_ordered_set_square with 0 2 nocomposites.
-
-alias symbol "pi1" (instance 4) = "exT \fst".
-alias symbol "pi1" (instance 2) = "exT \fst".
-lemma ordered_set_square_of_segment_square :
- ∀O:ordered_set.∀s:‡O.{[s]} squareO → O squareO ≝
- λO:ordered_set.λs:‡O.λb:{[s]} squareO.〈\fst(\fst b),\fst(\snd b)〉.
-
-coercion ordered_set_square_of_segment_square nocomposites.
-
-lemma restriction_agreement :
- ∀O:ordered_uniform_space.∀s:‡O.∀P:{[s]} squareO → Prop.∀OP:O squareO → Prop.Prop.
-apply(λO:ordered_uniform_space.λs:‡O.
- λP:{[s]} squareO → Prop. λOP:O squareO → Prop.
- ∀b:{[s]} squareO.(P b → OP b) ∧ (OP b → P b));
-qed.
-
-lemma unrestrict: ∀O:ordered_uniform_space.∀s:‡O.∀U,u.∀x:{[s]} squareO.
- restriction_agreement ? s U u → U x → u x.
-intros 6; cases (H x); assumption;
-qed.
-
-lemma restrict: ∀O:ordered_uniform_space.∀s:‡O.∀U,u.∀x:{[s]} squareO.
- restriction_agreement ? s U u → u x → U x.
-intros 6; cases (H x); assumption;
-qed.
-
-lemma invert_restriction_agreement:
- ∀O:ordered_uniform_space.∀s:‡O.
- ∀U:{[s]} squareO → Prop.∀u:O squareO → Prop.
- restriction_agreement ? s U u →
- restriction_agreement ? s (\inv U) (\inv u).
-intros 6; cases b;
-generalize in match (H 〈h1,h〉); cases h; cases h1; simplify;
-intro X; cases X; split; assumption;
-qed.
-
-lemma bs2_of_bss2:
- ∀O:ordered_set.∀s:‡O.(bishop_set_of_ordered_set {[s]}) squareB → (bishop_set_of_ordered_set O) squareB ≝
- λO:ordered_set.λs:‡O.λb:{[s]} squareO.〈\fst(\fst b),\fst(\snd b)〉.
-
-coercion bs2_of_bss2 nocomposites.
-
-
-lemma a2sa :
- ∀O:ordered_uniform_space.∀s:‡(ordered_set_OF_ordered_uniform_space O).
- ∀x:
- bs_carr
- (square_bishop_set
- (bishop_set_of_ordered_set
- (segment_ordered_set
- (ordered_set_OF_ordered_uniform_space O) s))).
- (\fst x) ≈ (\snd x) →
- (\fst (bs2_of_bss2 (ordered_set_OF_ordered_uniform_space O) s x))
- ≈
- (\snd (bs2_of_bss2 (ordered_set_OF_ordered_uniform_space O) s x)).
-intros 3; cases x (a b); clear x; simplify in match (\fst ?);
-simplify in match (\snd ?); intros 2 (K H); apply K; clear K;
-cases H;
-[ left; change in H1:(? ? % ?) with (\fst a);
- change in H1:(? ? ? %) with (\fst b);
- change in a with (hos_carr (half_segment_ordered_set ? s));
- change in b with (hos_carr (half_segment_ordered_set ? s));
- apply rule H1;
-| right; change in H1:(? ? % ?) with (\fst b);
- change in H1:(? ? ? %) with (\fst a);
- change in a with (hos_carr (half_segment_ordered_set ? s));
- change in b with (hos_carr (half_segment_ordered_set ? s));
- apply rule H1;]
-qed.
-
-
-lemma segment_ordered_uniform_space:
- ∀O:ordered_uniform_space.∀s:‡O.ordered_uniform_space.
-intros (O s); apply mk_ordered_uniform_space;
-[1: apply (mk_ordered_uniform_space_ {[s]});
- [1: alias symbol "and" = "constructive and".
- letin f ≝ (λP:{[s]} squareO → Prop. ∃OP:O squareO → Prop.
- (us_unifbase O OP) ∧ restriction_agreement ?? P OP);
- apply (mk_uniform_space (bishop_set_of_ordered_set {[s]}) f);
- [1: intros (U H); intro x; simplify;
- cases H (w Hw); cases Hw (Gw Hwp); clear H Hw; intro Hm;
- lapply (us_phi1 O w Gw x (a2sa ??? Hm)) as IH;
- apply (restrict ? s ??? Hwp IH);
- |2: intros (U V HU HV); cases HU (u Hu); cases HV (v Hv); clear HU HV;
- cases Hu (Gu HuU); cases Hv (Gv HvV); clear Hu Hv;
- cases (us_phi2 O u v Gu Gv) (w HW); cases HW (Gw Hw); clear HW;
- exists; [apply (λb:{[s]} squareB.w b)] split;
- [1: unfold f; simplify; clearbody f;
- exists; [apply w]; split; [assumption] intro b; simplify;
- unfold segment_square_of_ordered_set_square;
- cases b; intros; split; intros; assumption;
- |2: intros 2 (x Hx); cases (Hw ? Hx); split;
- [apply (restrict O s ??? HuU H)|apply (restrict O s ??? HvV H1);]]
- |3: intros (U Hu); cases Hu (u HU); cases HU (Gu HuU); clear Hu HU;
- cases (us_phi3 O u Gu) (w HW); cases HW (Gw Hwu); clear HW;
- exists; [apply (λx:{[s]} squareB.w x)] split;
- [1: exists;[apply w];split;[assumption] intros; simplify; intro;
- unfold segment_square_of_ordered_set_square;
- cases b; intros; split; intro; assumption;
- |2: intros 2 (x Hx); apply (restrict O s ??? HuU); apply Hwu;
- cases Hx (m Hm); exists[apply (\fst m)] apply Hm;]
- |4: intros (U HU x); cases HU (u Hu); cases Hu (Gu HuU); clear HU Hu;
- cases (us_phi4 O u Gu x) (Hul Hur);
- split; intros;
- [1: lapply (invert_restriction_agreement O s ?? HuU) as Ra;
- apply (restrict O s ?? x Ra);
- apply Hul; apply (unrestrict O s ??? HuU H);
- |2: apply (restrict O s ??? HuU); apply Hur;
- apply (unrestrict O s ??? (invert_restriction_agreement O s ?? HuU) H);]]
- |2: simplify; reflexivity;]
-|2: simplify; unfold convex; intros 3; cases s1; intros;
- (* TODO: x2sx is for ≰, we need one for ≤ *)
- cases H (u HU); cases HU (Gu HuU); clear HU H;
- lapply depth=0 (ous_convex_l ?? Gu 〈\fst h,\fst h1〉 ???????) as K3;
- [2: intro; apply H2; apply (x2sx_ (os_l O) s h h1 H);
- |3: apply 〈\fst (\fst y),\fst (\snd y)〉;
- |4: intro; change in H with (\fst (\fst y) ≰ \fst h1); apply H3;
- apply (x2sx_ (os_l O) s (\fst y) h1 H);
- |5: change with (\fst h ≤ \fst (\fst y)); intro; apply H4;
- apply (x2sx_ (os_l O) s h (\fst y) H);
- |6: change with (\fst (\snd y) ≤ \fst h1); intro; apply H5;
- apply (x2sx_ (os_l O) s (\snd y) h1 H);
- |7: change with (\fst (\fst y) ≤ \fst (\snd y)); intro; apply H6;
- apply (x2sx_ (os_l O) s (\fst y) (\snd y) H);
- |8: apply (restrict O s U u y HuU K3);
- |1: apply (unrestrict O s ?? 〈h,h1〉 HuU H1);]
-|3: simplify; unfold convex; intros 3; cases s1; intros;
- cases H (u HU); cases HU (Gu HuU); clear HU H;
- lapply depth=0 (ous_convex_r ?? Gu 〈\fst h,\fst h1〉 ???????) as K3;
- [2: intro; apply H2; apply (x2sx_ (os_r O) s h h1 H);
- |3: apply 〈\fst (\fst y),\fst (\snd y)〉;
- |4: intro; apply H3;
- apply (x2sx_ (os_r O) s (\fst y) h1 H);
- |5: intro; apply H4;
- apply (x2sx_ (os_r O) s h (\fst y) H);
- |6: intro; apply H5;
- apply (x2sx_ (os_r O) s (\snd y) h1 H);
- |7: intro; apply H6;
- apply (x2sx_ (os_r O) s (\fst y) (\snd y) H);
- |8: apply (restrict O s U u y HuU K3);
- |1: apply (unrestrict O s ?? 〈h,h1〉 HuU H1);]
-]
-qed.
-
-interpretation "Ordered uniform space segment" 'segset a =
- (segment_ordered_uniform_space _ a).
-
-(* Lemma 3.2 *)
-alias symbol "pi1" = "exT \fst".
-lemma restric_uniform_convergence:
- ∀O:ordered_uniform_space.∀s:‡O.
- ∀x:{[s]}.
- ∀a:sequence {[s]}.
- (⌊n, \fst (a n)⌋ : sequence O) uniform_converges (\fst x) →
- a uniform_converges x.
-intros 7; cases H1; cases H2; clear H2 H1;
-cases (H ? H3) (m Hm); exists [apply m]; intros;
-apply (restrict ? s ??? H4); apply (Hm ? H1);
-qed.
-
-definition order_continuity ≝
- λC:ordered_uniform_space.∀a:sequence C.∀x:C.
- (a ↑ x → a uniform_converges x) ∧ (a ↓ x → a uniform_converges x).
-
-lemma hint_boh1: ∀O. Type_OF_ordered_uniform_space O → hos_carr (os_l O).
-intros; assumption;
-qed.
-
-coercion hint_boh1 nocomposites.
-
-lemma hint_boh2: ∀O:ordered_uniform_space. hos_carr (os_l O) → Type_OF_ordered_uniform_space O.
-intros; assumption;
-qed.
-
-coercion hint_boh2 nocomposites.
-
+++ /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 "ordered_uniform.ma".
-include "property_sigma.ma".
-
-lemma h_segment_upperbound:
- ∀C:half_ordered_set.
- ∀s:segment C.
- ∀a:sequence (half_segment_ordered_set C s).
- upper_bound ? ⌊n,\fst (a n)⌋ (seg_u C s).
-intros 4; simplify; cases (a n); simplify; unfold in H;
-cases (wloss_prop C); rewrite < H1 in H; simplify; cases H;
-assumption;
-qed.
-
-notation "'segment_upperbound'" non associative with precedence 90 for @{'segment_upperbound}.
-notation "'segment_lowerbound'" non associative with precedence 90 for @{'segment_lowerbound}.
-
-interpretation "segment_upperbound" 'segment_upperbound = (h_segment_upperbound (os_l _)).
-interpretation "segment_lowerbound" 'segment_lowerbound = (h_segment_upperbound (os_r _)).
-
-lemma h_segment_preserves_uparrow:
- ∀C:half_ordered_set.∀s:segment C.∀a:sequence (half_segment_ordered_set C s).
- ∀x,h. uparrow C ⌊n,\fst (a n)⌋ x → uparrow (half_segment_ordered_set C s) a ≪x,h≫.
-intros; cases H (Ha Hx); split;
-[ intro n; intro H; apply (Ha n); apply rule H;
-| cases Hx; split;
- [ intro n; intro H; apply (H1 n);apply rule H;
- | intros; cases (H2 (\fst y)); [2: apply rule H3;]
- exists [apply w] apply (x2sx_ ?? (a w) y H4);]]
-qed.
-
-notation "'segment_preserves_uparrow'" non associative with precedence 90 for @{'segment_preserves_uparrow}.
-notation "'segment_preserves_downarrow'" non associative with precedence 90 for @{'segment_preserves_downarrow}.
-
-interpretation "segment_preserves_uparrow" 'segment_preserves_uparrow = (h_segment_preserves_uparrow (os_l _)).
-interpretation "segment_preserves_downarrow" 'segment_preserves_downarrow = (h_segment_preserves_uparrow (os_r _)).
-
-(* Fact 2.18 *)
-lemma segment_cauchy:
- ∀C:ordered_uniform_space.∀s:‡C.∀a:sequence {[s]}.
- a is_cauchy → ⌊n,\fst (a n)⌋ is_cauchy.
-intros 6;
-alias symbol "pi1" (instance 3) = "pair pi1".
-alias symbol "pi2" = "pair pi2".
-apply (H (λx:{[s]} squareB.U 〈\fst (\fst x),\fst (\snd x)〉));
-(unfold segment_ordered_uniform_space; simplify);
-exists [apply U] split; [assumption;]
-intro; cases b; intros; simplify; split; intros; assumption;
-qed.
-
-(* Definition 3.7 *)
-definition exhaustive ≝
- λC:ordered_uniform_space.
- ∀a,b:sequence C.
- (a is_increasing → a is_upper_located → a is_cauchy) ∧
- (b is_decreasing → b is_lower_located → b is_cauchy).
-
-lemma h_uparrow_to_in_segment:
- ∀C:half_ordered_set.
- ∀s:segment C.
- ∀a:sequence C.
- (∀i.a i ∈ s) →
- ∀x:C. uparrow C a x →
- in_segment C s x.
-intros (C H a H1 x H2); unfold in H2; cases H2; clear H2;unfold in H3 H4; cases H4; clear H4; unfold in H2;
-cases (wloss_prop C) (W W); apply prove_in_segment; unfold;
-[ apply (hle_transitive ??? x ? (H2 O)); lapply (H1 O) as K; unfold in K; rewrite <W in K;
- cases K; unfold in H4 H6; apply H4;
-| intro; cases (H5 ? H4); clear H5 H4;lapply(H1 w) as K; unfold in K; rewrite<W in K;
- cases K; unfold in H5 H4; apply H5; apply H6;
-| apply (hle_transitive ??? x ? (H2 O)); lapply (H1 0) as K; unfold in K; rewrite <W in K;
- cases K; unfold in H4 H6; apply H6;
-| intro; cases (H5 ? H4); clear H5 H4;lapply(H1 w) as K; unfold in K; rewrite<W in K;
- cases K; unfold in H5 H4; apply (H4 H6);]
-qed.
-
-notation "'uparrow_to_in_segment'" non associative with precedence 90 for @{'uparrow_to_in_segment}.
-notation "'downarrow_to_in_segment'" non associative with precedence 90 for @{'downarrow_to_in_segment}.
-
-interpretation "uparrow_to_in_segment" 'uparrow_to_in_segment = (h_uparrow_to_in_segment (os_l _)).
-interpretation "downarrow_to_in_segment" 'downarrow_to_in_segment = (h_uparrow_to_in_segment (os_r _)).
-
-(* Lemma 3.8 NON DUALIZZATO *)
-lemma restrict_uniform_convergence_uparrow:
- ∀C:ordered_uniform_space.property_sigma C →
- ∀s:segment (os_l C).exhaustive (segment_ordered_uniform_space C s) →
- ∀a:sequence (segment_ordered_uniform_space C s).
- ∀x:C. ⌊n,\fst (a n)⌋ ↑ x →
- in_segment (os_l C) s x ∧ ∀h:x ∈ s.a uniform_converges ≪x,h≫.
-intros; split;
-[1: apply (uparrow_to_in_segment s ⌊n,\fst (a \sub n)⌋ ? x H2);
- simplify; intros; cases (a i); assumption;
-|2: intros;
- lapply (uparrow_upperlocated a ≪x,h≫) as Ha1;
- [2: apply (segment_preserves_uparrow s); assumption;]
- lapply (segment_preserves_supremum s a ≪?,h≫ H2) as Ha2;
- cases Ha2; clear Ha2;
- cases (H1 a a); lapply (H5 H3 Ha1) as HaC;
- lapply (segment_cauchy C s ? HaC) as Ha;
- lapply (sigma_cauchy ? H ? x ? Ha); [left; assumption]
- apply (restric_uniform_convergence C s ≪x,h≫ a Hletin)]
-qed.
-
-lemma hint_mah1:
- ∀C. Type_OF_ordered_uniform_space1 C → hos_carr (os_r C).
- intros; assumption; qed.
-
-coercion hint_mah1 nocomposites.
-
-lemma hint_mah2:
- ∀C. sequence (hos_carr (os_l C)) → sequence (hos_carr (os_r C)).
- intros; assumption; qed.
-
-coercion hint_mah2 nocomposites.
-
-lemma hint_mah3:
- ∀C. Type_OF_ordered_uniform_space C → hos_carr (os_r C).
- intros; assumption; qed.
-
-coercion hint_mah3 nocomposites.
-
-lemma hint_mah4:
- ∀C. sequence (hos_carr (os_r C)) → sequence (hos_carr (os_l C)).
- intros; assumption; qed.
-
-coercion hint_mah4 nocomposites.
-
-lemma hint_mah5:
- ∀C. segment (hos_carr (os_r C)) → segment (hos_carr (os_l C)).
- intros; assumption; qed.
-
-coercion hint_mah5 nocomposites.
-
-lemma hint_mah6:
- ∀C. segment (hos_carr (os_l C)) → segment (hos_carr (os_r C)).
- intros; assumption; qed.
-
-coercion hint_mah6 nocomposites.
-
-lemma restrict_uniform_convergence_downarrow:
- ∀C:ordered_uniform_space.property_sigma C →
- ∀s:segment (os_l C).exhaustive (segment_ordered_uniform_space C s) →
- ∀a:sequence (segment_ordered_uniform_space C s).
- ∀x:C. ⌊n,\fst (a n)⌋ ↓ x →
- in_segment (os_l C) s x ∧ ∀h:x ∈ s.a uniform_converges ≪x,h≫.
-intros; split;
-[1: apply (downarrow_to_in_segment s ⌊n,\fst (a n)⌋ ? x); [2: apply H2];
- simplify; intros; cases (a i); assumption;
-|2: intros;
- lapply (downarrow_lowerlocated a ≪x,h≫) as Ha1;
- [2: apply (segment_preserves_downarrow s a x h H2);]
- lapply (segment_preserves_infimum s a ≪?,h≫ H2) as Ha2;
- cases Ha2; clear Ha2;
- cases (H1 a a); lapply (H6 H3 Ha1) as HaC;
- lapply (segment_cauchy C s ? HaC) as Ha;
- lapply (sigma_cauchy ? H ? x ? Ha); [right; assumption]
- apply (restric_uniform_convergence C s ≪x,h≫ a Hletin)]
-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 "ordered_uniform.ma".
-include "russell_support.ma".
-
-(* Definition 3.5 *)
-alias num (instance 0) = "natural number".
-definition property_sigma ≝
- λC:ordered_uniform_space.
- ∀U.us_unifbase ? U →
- ∃V:sequence (C squareB → Prop).
- (∀i.us_unifbase ? (V i)) ∧
- ∀a:sequence C.∀x:C.(a ↑ x ∨ a ↓ x) →
- (∀n.∀i,j.n ≤ i → n ≤ j → V n 〈a i,a j〉) → U 〈a 0,x〉.
-
-definition max ≝
- λm,n.match leb n m with [true ⇒ m | false ⇒ n].
-
-lemma le_max: ∀n,m.m ≤ max n m.
-intros; unfold max; apply leb_elim; simplify; intros; [assumption] apply le_n;
-qed.
-
-lemma max_le_l: ∀n,m,z.max n m ≤ z → n ≤ z.
-intros 3; unfold max; apply leb_elim; simplify; intros; [assumption]
-apply lt_to_le; apply (lt_to_le_to_lt ???? H1);
-apply not_le_to_lt; assumption;
-qed.
-
-lemma sym_max: ∀n,m.max n m = max m n.
-intros; apply (nat_elim2 ???? n m); simplify; intros;
-[1: elim n1; [reflexivity] rewrite < H in ⊢ (? ? ? (? %));
- simplify; rewrite > H; reflexivity;
-|2: reflexivity
-|3: apply leb_elim; apply leb_elim; simplify;
- [1: intros; apply le_to_le_to_eq; apply le_S_S;assumption;
- |2,3: intros; reflexivity;
- |4: intros; unfold max in H;
- rewrite > (?:leb n1 m1 = false) in H; [2:
- apply lt_to_leb_false; apply not_le_to_lt; assumption;]
- rewrite > (?:leb m1 n1 = false) in H; [2:
- apply lt_to_leb_false; apply not_le_to_lt; assumption;]
- apply eq_f; assumption;]]
-qed.
-
-lemma max_le_r: ∀n,m,z.max n m ≤ z → m ≤ z.
-intros; rewrite > sym_max in H; apply (max_le_l ??? H);
-qed.
-
-(* Lemma 3.6 *)
-lemma sigma_cauchy:
- ∀C:ordered_uniform_space.property_sigma C →
- ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
-intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
-letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉);
-letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
- match i with
- [ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
- | S i' ⇒ max (match H2 (w i) ? with [ ex_introT k _ ⇒ k ]) (S (aux i'))
- ] in aux
- : ∀z.∃k. spec z k)); unfold spec in aux ⊢ %;
- [1,2:apply H8;
- |3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
- simplify in ⊢ (?→? (? % ?) ?→?);
- intros; lapply (H5 i j) as H14;
- [2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
- cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]
- cases (aux n1) in H6 H7 ⊢ %; simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
- apply H6; [3: apply le_S_S_to_le; assumption]
- apply lt_to_le; apply (max_le_r w1); assumption;
- |4: intros; clear H6; rewrite > H4 in H5;
- rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;]
-cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
- intro n; change with (S (m n) ≤ m (S n)); unfold m;
- whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
-cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_increasing) as Hm1; [2:
- intro n; intro L; change in L with (m (S n) < m n);
- lapply (Hm n) as L1; change in L1 with (m n < m (S n));
- lapply (trans_lt ??? L L1) as L3; apply (not_le_Sn_n ? L3);]
-clearbody m; unfold spec in m Hm Hm1; clear spec;
-cut (⌊x,a (m x)⌋ ↑ l ∨ ⌊x,a (m x)⌋ ↓ l) as H10; [2:
- cases H1;
- [ left; apply (selection_uparrow ? Hm a l H4);
- | right; apply (selection_downarrow ? Hm a l H4);]]
-lapply (H9 ?? H10) as H11; [
- exists [apply (m 0:nat)] intros;
- cases H1; cases H5; cases H7; cases (us_phi4 ?? H3 〈l,a i〉);
- apply H15; change with (U 〈a i,l〉);
- [apply (ous_convex_l C ? H3 ? H11 (H12 (m O)));
- |apply (ous_convex_r C ? H3 ? H11 (H12 (m O)));]
- [1:apply (H12 i);
- |3: apply (le_reflexive l);
- |4: apply (H12 i);
- |2:change with (a (m O) ≤ a i);
- apply (trans_increasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);
- |5:apply (H12 i);
- |7:apply (ge_reflexive (l : hos_carr (os_r C)));
- |8:apply (H12 i);
- |6:change with (a i ≤ a (m O));
- apply (trans_decreasing ? H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]
-clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
-generalize in match (refl_eq nat (m p));
-generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;
-intros (H16); simplify in H16:(? ? ? %); destruct H16;
-apply H15; [3: apply le_n]
-[1: lapply (trans_increasing ? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
- apply (le_to_not_lt p q H4);
-|2: lapply (trans_increasing ? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
- apply (le_to_not_lt p r H5);]
-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 "nat/nat.ma".
-include "logic/cprop_connectives.ma".
-
-definition hide ≝ λT:Type.λx:T.x.
-
-notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
-interpretation "hide" 'hide = (hide _ _).
-interpretation "hide2" 'hide = (hide _ _ _).
-
-definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p.
-coercion cic:/matita/dama/russell_support/inject.con 0 1.
-definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ ex_introT w _ ⇒ w].
-coercion cic:/matita/dama/russell_support/eject.con.
+++ /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 "ordered_uniform.ma".
-
-lemma le_w_plus: ∀n,m,o.n+m≤o → m ≤ o.
-intro; elim n; simplify; [assumption]
-lapply (le_S ?? H1); apply H; apply le_S_S_to_le; assumption;
-qed.
-
-alias symbol "leq" = "Ordered set less or equal than".
-alias symbol "and" = "logical and".
-theorem sandwich:
- ∀O:ordered_uniform_space.∀l:O.∀a,b,x:sequence O.
- (∀i:nat.a i ≤ x i ∧ x i ≤ b i) →
- a uniform_converges l →
- b uniform_converges l →
- x uniform_converges l.
-intros 10;
-cases (us_phi3 ? ? H3) (V GV); cases GV (Gv HV); clear GV;
-cases (us_phi3 ? ? Gv) (W GW); cases GW (Gw HW); clear GW;
-cases (H1 ? Gw) (ma Hma); cases (H2 ? Gw) (mb Hmb); clear H1 H2;
-exists [apply (ma + mb)] intros; apply (HV 〈l,(x i)〉);
-unfold; simplify; exists [apply (a i)] split;
-[2: apply (ous_convex_l ?? Gv 〈a i,b i〉); cases (H i) (Lax Lxb); clear H;
- [1: apply HW; exists [apply l]simplify; split;
- [1: cases (us_phi4 ?? Gw 〈(a i),l〉); apply H2; clear H2 H;
- apply (Hma i); rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;
- |2: apply Hmb; apply (le_w_plus ma); assumption]
- |2,3: simplify; apply (le_transitive (a i) ?? Lax Lxb);
- |4: apply (le_reflexive);
- |5,6: assumption;]
-|1: apply HW; exists[apply l] simplify; split;
- [1: apply (us_phi1 ?? Gw); unfold; apply eq_reflexive;
- |2: apply Hma; rewrite > sym_plus in H1; apply (le_w_plus mb); 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 "nat/nat.ma".
-
-inductive sequence (O:Type) : Type ≝
- | mk_seq : (nat → O) → sequence O.
-
-definition fun_of_seq: ∀O:Type.sequence O → nat → O ≝
- λO.λx:sequence O.match x with [ mk_seq f ⇒ f ].
-
-coercion cic:/matita/dama/sequence/fun_of_seq.con 1.
-
-notation < "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90
-for @{ 'sequence (\lambda ${ident i} : $t . $p)}.
-
-notation > "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90
-for @{ 'sequence (\lambda ${ident i} . $p)}.
-
-notation > "hvbox(\lfloor ident i, term 19 p \rfloor)" with precedence 90
-for @{ 'sequence (\lambda ${ident i} . $p)}.
-
-notation "a \sub i" left associative with precedence 90
- for @{ 'sequence_appl $a $i }.
-
-interpretation "sequence" 'sequence \eta.x = (mk_seq _ x).
-interpretation "sequence element" 'sequence_appl s i = (fun_of_seq _ s i).
+++ /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 "datatypes/constructors.ma".
-include "nat/plus.ma".
-include "nat_ordered_set.ma".
-include "sequence.ma".
-
-(* Definition 2.4 *)
-definition upper_bound ≝
- λO:half_ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤≤ u.
-
-definition supremum ≝
- λO:half_ordered_set.λs:sequence O.λx.
- upper_bound ? s x ∧ (∀y:O.x ≰≰ y → ∃n.s n ≰≰ y).
-
-definition increasing ≝
- λO:half_ordered_set.λa:sequence O.∀n:nat.a n ≤≤ a (S n).
-
-notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 45
- for @{'upper_bound $s $x}.
-notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 45
- for @{'lower_bound $s $x}.
-notation < "s \nbsp 'is_increasing'" non associative with precedence 45
- for @{'increasing $s}.
-notation < "s \nbsp 'is_decreasing'" non associative with precedence 45
- for @{'decreasing $s}.
-notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 45
- for @{'supremum $s $x}.
-notation < "x \nbsp 'is_infimum' \nbsp s" non associative with precedence 45
- for @{'infimum $s $x}.
-notation > "x 'is_upper_bound' s" non associative with precedence 45
- for @{'upper_bound $s $x}.
-notation > "x 'is_lower_bound' s" non associative with precedence 45
- for @{'lower_bound $s $x}.
-notation > "s 'is_increasing'" non associative with precedence 45
- for @{'increasing $s}.
-notation > "s 'is_decreasing'" non associative with precedence 45
- for @{'decreasing $s}.
-notation > "x 'is_supremum' s" non associative with precedence 45
- for @{'supremum $s $x}.
-notation > "x 'is_infimum' s" non associative with precedence 45
- for @{'infimum $s $x}.
-
-interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound (os_l _) s x).
-interpretation "Ordered set lower bound" 'lower_bound s x = (upper_bound (os_r _) s x).
-
-interpretation "Ordered set increasing" 'increasing s = (increasing (os_l _) s).
-interpretation "Ordered set decreasing" 'decreasing s = (increasing (os_r _) s).
-
-interpretation "Ordered set strong sup" 'supremum s x = (supremum (os_l _) s x).
-interpretation "Ordered set strong inf" 'infimum s x = (supremum (os_r _) s x).
-
-(* Fact 2.5 *)
-lemma h_supremum_is_upper_bound:
- ∀C:half_ordered_set.∀a:sequence C.∀u:C.
- supremum ? a u → ∀v.upper_bound ? a v → u ≤≤ v.
-intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
-cases (H1 ? H) (w Hw); apply Hv; [apply w] assumption;
-qed.
-
-notation "'supremum_is_upper_bound'" non associative with precedence 90 for @{'supremum_is_upper_bound}.
-notation "'infimum_is_lower_bound'" non associative with precedence 90 for @{'infimum_is_lower_bound}.
-
-interpretation "supremum_is_upper_bound" 'supremum_is_upper_bound = (h_supremum_is_upper_bound (os_l _)).
-interpretation "infimum_is_lower_bound" 'infimum_is_lower_bound = (h_supremum_is_upper_bound (os_r _)).
-
-(* Lemma 2.6 *)
-definition strictly_increasing ≝
- λC:half_ordered_set.λa:sequence C.∀n:nat.a (S n) ≰≰ a n.
-
-notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 45
- for @{'strictly_increasing $s}.
-notation > "s 'is_strictly_increasing'" non associative with precedence 45
- for @{'strictly_increasing $s}.
-interpretation "Ordered set strict increasing" 'strictly_increasing s =
- (strictly_increasing (os_l _) s).
-
-notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45
- for @{'strictly_decreasing $s}.
-notation > "s 'is_strictly_decreasing'" non associative with precedence 45
- for @{'strictly_decreasing $s}.
-interpretation "Ordered set strict decreasing" 'strictly_decreasing s =
- (strictly_increasing (os_r _) s).
-
-definition uparrow ≝
- λC:half_ordered_set.λs:sequence C.λu:C.
- increasing ? s ∧ supremum ? s u.
-
-interpretation "Ordered set uparrow" 'funion s u = (uparrow (os_l _) s u).
-interpretation "Ordered set downarrow" 'fintersects s u = (uparrow (os_r _) s u).
-
-lemma h_trans_increasing:
- ∀C:half_ordered_set.∀a:sequence C.increasing ? a →
- ∀n,m:nat_ordered_set. n ≤ m → a n ≤≤ a m.
-intros 5 (C a Hs n m); elim m; [
- rewrite > (le_n_O_to_eq n (not_lt_to_le O n H));
- intro X; cases (hos_coreflexive ? (a n) X);]
-cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1;
-[2: rewrite > H2; intro; cases (hos_coreflexive ? (a (S n1)) H1);
-|1: apply (hle_transitive ???? (H ?) (Hs ?));
- intro; whd in H1; apply (not_le_Sn_n n); apply (transitive_le ??? H2 H1);]
-qed.
-
-notation "'trans_increasing'" non associative with precedence 90 for @{'trans_increasing}.
-notation "'trans_decreasing'" non associative with precedence 90 for @{'trans_decreasing}.
-
-interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l _)).
-interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)).
-
-lemma hint_nat :
- Type_of_ordered_set nat_ordered_set →
- hos_carr (os_l (nat_ordered_set)).
-intros; assumption;
-qed.
-
-coercion hint_nat nocomposites.
-
-lemma h_trans_increasing_exc:
- ∀C:half_ordered_set.∀a:sequence C.increasing ? a →
- ∀n,m:nat_ordered_set. m ≰≰ n → a n ≤≤ a m.
-intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
-intro; apply H;
-[1: change in n1 with (hos_carr (os_l nat_ordered_set));
- change with (n<n1);
- cases (le_to_or_lt_eq ?? H1); [apply le_S_S_to_le;assumption]
- cases (Hs n); rewrite < H3 in H2; assumption;
-|2: cases (hos_cotransitive ? (a n) (a (S n1)) (a n1) H2); [assumption]
- cases (Hs n1); assumption;]
-qed.
-
-notation "'trans_increasing_exc'" non associative with precedence 90 for @{'trans_increasing_exc}.
-notation "'trans_decreasing_exc'" non associative with precedence 90 for @{'trans_decreasing_exc}.
-
-interpretation "trans_increasing_exc" 'trans_increasing_exc = (h_trans_increasing_exc (os_l _)).
-interpretation "trans_decreasing_exc" 'trans_decreasing_exc = (h_trans_increasing_exc (os_r _)).
-
-alias symbol "exists" = "CProp exists".
-lemma nat_strictly_increasing_reaches:
- ∀m:sequence nat_ordered_set.
- m is_strictly_increasing → ∀w.∃t.m t ≰ w.
-intros; elim w;
-[1: cases (nat_discriminable O (m O)); [2: cases (not_le_Sn_n O (ltn_to_ltO ?? H1))]
- cases H1; [exists [apply O] apply H2;]
- exists [apply (S O)] lapply (H O) as H3; rewrite < H2 in H3; assumption
-|2: cases H1 (p Hp); cases (nat_discriminable (S n) (m p));
- [1: cases H2; clear H2;
- [1: exists [apply p]; assumption;
- |2: exists [apply (S p)]; rewrite > H3; apply H;]
- |2: cases (?:False); change in Hp with (n<m p);
- apply (not_le_Sn_n (m p));
- apply (transitive_le ??? H2 Hp);]]
-qed.
-
-lemma h_selection_uparrow:
- ∀C:half_ordered_set.∀m:sequence nat_ordered_set.
- m is_strictly_increasing →
- ∀a:sequence C.∀u.uparrow ? a u → uparrow ? ⌊x,a (m x)⌋ u.
-intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
-[1: intro n; simplify; apply (h_trans_increasing_exc ? a Ia); apply (Hm n);
-|2: intro n; simplify; apply Uu;
-|3: intros (y Hy); simplify; cases (Hu ? Hy);
- cases (nat_strictly_increasing_reaches ? Hm w);
- exists [apply w1]; cases (hos_cotransitive ? (a w) y (a (m w1)) H); [2:assumption]
- cases (h_trans_increasing_exc ?? Ia w (m w1) H1); assumption;]
-qed.
-
-notation "'selection_uparrow'" non associative with precedence 90 for @{'selection_uparrow}.
-notation "'selection_downarrow'" non associative with precedence 90 for @{'selection_downarrow}.
-
-interpretation "selection_uparrow" 'selection_uparrow = (h_selection_uparrow (os_l _)).
-interpretation "selection_downarrow" 'selection_downarrow = (h_selection_uparrow (os_r _)).
-
-(* Definition 2.7 *)
-definition order_converge ≝
- λO:ordered_set.λa:sequence O.λx:O.
- exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
- (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧
- (u i) is_supremum ⌊w,a (w+i)⌋).
-
-notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45
- for @{'order_converge $a $x}.
-notation > "a 'order_converges' x" non associative with precedence 45
- for @{'order_converge $a $x}.
-interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).
-
-(* Definition 2.8 *)
-record segment (O : Type) : Type ≝ {
- seg_l_ : O;
- seg_u_ : O
-}.
-
-notation > "𝕦_term 90 s" non associative with precedence 90 for @{'upp $s}.
-notation "𝕦 \sub term 90 s" non associative with precedence 90 for @{'upp $s}.
-notation > "𝕝_term 90 s" non associative with precedence 90 for @{'low $s}.
-notation "𝕝 \sub term 90 s" non associative with precedence 90 for @{'low $s}.
-
-definition seg_u ≝
- λO:half_ordered_set.λs:segment O.
- wloss O ?? (λl,u.l) (seg_u_ ? s) (seg_l_ ? s).
-definition seg_l ≝
- λO:half_ordered_set.λs:segment O.
- wloss O ?? (λl,u.l) (seg_l_ ? s) (seg_u_ ? s).
-
-interpretation "uppper" 'upp s = (seg_u (os_l _) s).
-interpretation "lower" 'low s = (seg_l (os_l _) s).
-interpretation "uppper dual" 'upp s = (seg_l (os_r _) s).
-interpretation "lower dual" 'low s = (seg_u (os_r _) s).
-
-definition in_segment ≝
- λO:half_ordered_set.λs:segment O.λx:O.
- wloss O ?? (λp1,p2.p1 ∧ p2) (seg_l ? s ≤≤ x) (x ≤≤ seg_u ? s).
-
-notation "‡O" non associative with precedence 90 for @{'segment $O}.
-interpretation "Ordered set sergment" 'segment x = (segment x).
-
-interpretation "Ordered set sergment in" 'mem x s = (in_segment _ s x).
-
-definition segment_ordered_set_carr ≝
- λO:half_ordered_set.λs:‡O.∃x.x ∈ s.
-definition segment_ordered_set_exc ≝
- λO:half_ordered_set.λs:‡O.
- λx,y:segment_ordered_set_carr O s.hos_excess_ O (\fst x) (\fst y).
-lemma segment_ordered_set_corefl:
- ∀O,s. coreflexive ? (wloss O ?? (segment_ordered_set_exc O s)).
-intros 3; cases x; cases (wloss_prop O);
-generalize in match (hos_coreflexive O w);
-rewrite < (H1 ?? (segment_ordered_set_exc O s));
-rewrite < (H1 ?? (hos_excess_ O)); intros; assumption;
-qed.
-lemma segment_ordered_set_cotrans :
- ∀O,s. cotransitive ? (wloss O ?? (segment_ordered_set_exc O s)).
-intros 5 (O s x y z); cases x; cases y ; cases z; clear x y z;
-generalize in match (hos_cotransitive O w w1 w2);
-cases (wloss_prop O);
-do 3 rewrite < (H3 ?? (segment_ordered_set_exc O s));
-do 3 rewrite < (H3 ?? (hos_excess_ O)); intros; apply H4; assumption;
-qed.
-
-lemma half_segment_ordered_set:
- ∀O:half_ordered_set.∀s:segment O.half_ordered_set.
-intros (O a); constructor 1;
-[ apply (segment_ordered_set_carr O a);
-| apply (wloss O);
-| apply (wloss_prop O);
-| apply (segment_ordered_set_exc O a);
-| apply (segment_ordered_set_corefl O a);
-| apply (segment_ordered_set_cotrans ??);
-]
-qed.
-
-lemma segment_ordered_set:
- ∀O:ordered_set.∀s:‡O.ordered_set.
-intros (O s);
-apply half2full; apply (half_segment_ordered_set (os_l O) s);
-qed.
-
-notation "{[ term 19 s ]}" non associative with precedence 90 for @{'segset $s}.
-interpretation "Ordered set segment" 'segset s = (segment_ordered_set _ s).
-
-(* test :
- ∀O:ordered_set.∀s: segment (os_l O).∀x:O.
- in_segment (os_l O) s x
- =
- in_segment (os_r O) s x.
-intros; try reflexivity;
-*)
-
-lemma prove_in_segment:
- ∀O:half_ordered_set.∀s:segment O.∀x:O.
- (seg_l O s) ≤≤ x → x ≤≤ (seg_u O s) → x ∈ s.
-intros; unfold; cases (wloss_prop O); rewrite < H2;
-split; assumption;
-qed.
-
-lemma cases_in_segment:
- ∀C:half_ordered_set.∀s:segment C.∀x. x ∈ s → (seg_l C s) ≤≤ x ∧ x ≤≤ (seg_u C s).
-intros; unfold in H; cases (wloss_prop C) (W W); rewrite<W in H; [cases H; split;assumption]
-cases H; split; assumption;
-qed.
-
-definition hint_sequence:
- ∀C:ordered_set.
- sequence (hos_carr (os_l C)) → sequence (Type_of_ordered_set C).
-intros;assumption;
-qed.
-
-definition hint_sequence1:
- ∀C:ordered_set.
- sequence (hos_carr (os_r C)) → sequence (Type_of_ordered_set_dual C).
-intros;assumption;
-qed.
-
-definition hint_sequence2:
- ∀C:ordered_set.
- sequence (Type_of_ordered_set C) → sequence (hos_carr (os_l C)).
-intros;assumption;
-qed.
-
-definition hint_sequence3:
- ∀C:ordered_set.
- sequence (Type_of_ordered_set_dual C) → sequence (hos_carr (os_r C)).
-intros;assumption;
-qed.
-
-coercion hint_sequence nocomposites.
-coercion hint_sequence1 nocomposites.
-coercion hint_sequence2 nocomposites.
-coercion hint_sequence3 nocomposites.
-
-(* Lemma 2.9 - non easily dualizable *)
-
-lemma x2sx_:
- ∀O:half_ordered_set.
- ∀s:segment O.∀x,y:half_segment_ordered_set ? s.
- \fst x ≰≰ \fst y → x ≰≰ y.
-intros 4; cases x; cases y; clear x y; simplify; unfold hos_excess;
-whd in ⊢ (?→? (% ? ?)? ? ? ? ?); simplify in ⊢ (?→%);
-cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
-qed.
-
-lemma sx2x_:
- ∀O:half_ordered_set.
- ∀s:segment O.∀x,y:half_segment_ordered_set ? s.
- x ≰≰ y → \fst x ≰≰ \fst y.
-intros 4; cases x; cases y; clear x y; simplify; unfold hos_excess;
-whd in ⊢ (? (% ? ?) ?? ? ? ? → ?); simplify in ⊢ (% → ?);
-cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
-qed.
-
-lemma l2sl_:
- ∀C,s.∀x,y:half_segment_ordered_set C s. \fst x ≤≤ \fst y → x ≤≤ y.
-intros; intro; apply H; apply sx2x_; apply H1;
-qed.
-
-
-lemma sl2l_:
- ∀C,s.∀x,y:half_segment_ordered_set C s. x ≤≤ y → \fst x ≤≤ \fst y.
-intros; intro; apply H; apply x2sx_; apply H1;
-qed.
-
-coercion x2sx_ nocomposites.
-coercion sx2x_ nocomposites.
-coercion l2sl_ nocomposites.
-coercion sl2l_ nocomposites.
-
-lemma h_segment_preserves_supremum:
- ∀O:half_ordered_set.∀s:segment O.
- ∀a:sequence (half_segment_ordered_set ? s).
- ∀x:half_segment_ordered_set ? s.
- increasing ? ⌊n,\fst (a n)⌋ ∧
- supremum ? ⌊n,\fst (a n)⌋ (\fst x) → uparrow ? a x.
-intros; split; cases H; clear H;
-[1: intro n; lapply (H1 n) as K; clear H1 H2;
- intro; apply K; clear K; apply rule H;
-|2: cases H2; split; clear H2;
- [1: intro n; lapply (H n) as K; intro W; apply K;
- apply rule W;
- |2: clear H1 H; intros (y0 Hy0); cases (H3 (\fst y0));[exists[apply w]]
- [1: change in H with (\fst (a w) ≰≰ \fst y0); apply rule H;
- |2: apply rule Hy0;]]]
-qed.
-
-notation "'segment_preserves_supremum'" non associative with precedence 90 for @{'segment_preserves_supremum}.
-notation "'segment_preserves_infimum'" non associative with precedence 90 for @{'segment_preserves_infimum}.
-
-interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l _)).
-interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r _)).
-
-(*
-test segment_preserves_infimum2:
- ∀O:ordered_set.∀s:‡O.∀a:sequence {[s]}.∀x:{[s]}.
- ⌊n,\fst (a n)⌋ is_decreasing ∧
- (\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
-intros; apply (segment_preserves_infimum s a x H);
-qed.
-*)
-
-(* Definition 2.10 *)
-
-alias symbol "pi2" = "pair pi2".
-alias symbol "pi1" = "pair pi1".
-(*
-definition square_segment ≝
- λO:half_ordered_set.λs:segment O.λx: square_half_ordered_set O.
- in_segment ? s (\fst x) ∧ in_segment ? s (\snd x).
-*)
-definition convex ≝
- λO:half_ordered_set.λU:square_half_ordered_set O → Prop.
- ∀s.U s → le O (\fst s) (\snd s) →
- ∀y.
- le O (\fst y) (\snd s) →
- le O (\fst s) (\fst y) →
- le O (\snd y) (\snd s) →
- le O (\fst y) (\snd y) →
- U y.
-
-(* Definition 2.11 *)
-definition upper_located ≝
- λO:half_ordered_set.λa:sequence O.∀x,y:O. y ≰≰ x →
- (∃i:nat.a i ≰≰ x) ∨ (∃b:O.y ≰≰ b ∧ ∀i:nat.a i ≤≤ b).
-
-notation < "s \nbsp 'is_upper_located'" non associative with precedence 45
- for @{'upper_located $s}.
-notation > "s 'is_upper_located'" non associative with precedence 45
- for @{'upper_located $s}.
-interpretation "Ordered set upper locatedness" 'upper_located s =
- (upper_located (os_l _) s).
-
-notation < "s \nbsp 'is_lower_located'" non associative with precedence 45
- for @{'lower_located $s}.
-notation > "s 'is_lower_located'" non associative with precedence 45
- for @{'lower_located $s}.
-interpretation "Ordered set lower locatedness" 'lower_located s =
- (upper_located (os_r _) s).
-
-(* Lemma 2.12 *)
-lemma h_uparrow_upperlocated:
- ∀C:half_ordered_set.∀a:sequence C.∀u:C.uparrow ? a u → upper_located ? a.
-intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
-cases H3 (H4 H5); clear H3; cases (hos_cotransitive C y x u Hxy) (W W);
-[2: cases (H5 x W) (w Hw); left; exists [apply w] assumption;
-|1: right; exists [apply u]; split; [apply W|apply H4]]
-qed.
-
-notation "'uparrow_upperlocated'" non associative with precedence 90 for @{'uparrow_upperlocated}.
-notation "'downarrow_lowerlocated'" non associative with precedence 90 for @{'downarrow_lowerlocated}.
-
-interpretation "uparrow_upperlocated" 'uparrow_upperlocated = (h_uparrow_upperlocated (os_l _)).
-interpretation "downarrow_lowerlocated" 'downarrow_lowerlocated = (h_uparrow_upperlocated (os_r _)).
+++ /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 "supremum.ma".
-
-(* Definition 2.13 *)
-alias symbol "pair" = "Pair construction".
-alias symbol "exists" = "exists".
-alias symbol "and" = "logical and".
-definition compose_bs_relations ≝
- λC:bishop_set.λU,V:C squareB → Prop.
- λx:C squareB.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
-
-definition compose_os_relations ≝
- λC:ordered_set.λU,V:C squareB → Prop.
- λx:C squareB.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
-
-interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations _ a b).
-interpretation "ordered set relations composition" 'compose a b = (compose_os_relations _ a b).
-
-definition invert_bs_relation ≝
- λC:bishop_set.λU:C squareB → Prop.
- λx:C squareB. U 〈\snd x,\fst x〉.
-
-notation > "\inv" with precedence 60 for @{ 'invert_symbol }.
-interpretation "relation invertion" 'invert a = (invert_bs_relation _ a).
-interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _).
-interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x).
-
-alias symbol "exists" = "CProp exists".
-alias symbol "compose" = "bishop set relations composition".
-alias symbol "and" (instance 21) = "constructive and".
-alias symbol "and" (instance 16) = "constructive and".
-alias symbol "and" (instance 9) = "constructive and".
-record uniform_space : Type ≝ {
- us_carr:> bishop_set;
- us_unifbase: (us_carr squareB → Prop) → CProp;
- us_phi1: ∀U:us_carr squareB → Prop. us_unifbase U →
- (λx:us_carr squareB.\fst x ≈ \snd x) ⊆ U;
- us_phi2: ∀U,V:us_carr squareB → Prop. us_unifbase U → us_unifbase V →
- ∃W:us_carr squareB → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
- us_phi3: ∀U:us_carr squareB → Prop. us_unifbase U →
- ∃W:us_carr squareB → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
- us_phi4: ∀U:us_carr squareB → Prop. us_unifbase U → ∀x.(U x → (\inv U) x) ∧ ((\inv U) x → U x)
-}.
-
-(* Definition 2.14 *)
-alias symbol "leq" = "natural 'less or equal to'".
-definition cauchy ≝
- λC:uniform_space.λa:sequence C.∀U.us_unifbase C U →
- ∃n. ∀i,j. n ≤ i → n ≤ j → U 〈a i,a j〉.
-
-notation < "a \nbsp 'is_cauchy'" non associative with precedence 45
- for @{'cauchy $a}.
-notation > "a 'is_cauchy'" non associative with precedence 45
- for @{'cauchy $a}.
-interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).
-
-(* Definition 2.15 *)
-definition uniform_converge ≝
- λC:uniform_space.λa:sequence C.λu:C.
- ∀U.us_unifbase C U → ∃n. ∀i. n ≤ i → U 〈u,a i〉.
-
-notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45
- for @{'uniform_converge $a $x}.
-notation > "a 'uniform_converges' x" non associative with precedence 45
- for @{'uniform_converge $a $x}.
-interpretation "Uniform convergence" 'uniform_converge s u =
- (uniform_converge _ s u).
-
-(* Lemma 2.16 *)
-lemma uniform_converge_is_cauchy :
- ∀C:uniform_space.∀a:sequence C.∀x:C.
- a uniform_converges x → a is_cauchy.
-intros (C a x Ha); intros 2 (u Hu);
-cases (us_phi3 ?? Hu) (v Hv0); cases Hv0 (Hv H); clear Hv0;
-cases (Ha ? Hv) (n Hn); exists [apply n]; intros;
-apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)]
-cases (us_phi4 ?? Hv 〈a i,x〉) (P1 P2); apply P2;
-apply (Hn ? H1);
-qed.
projects / helm.git / commitdiff
