--- /dev/null
+include ../../Makefile.defs
+
+DIR=$(shell basename $$PWD)
+
+$(DIR) all:
+ $(BIN)../matitac
+$(DIR).opt opt all.opt:
+ $(BIN)../matitac.opt
+clean:
+ $(BIN)../matitaclean
+clean.opt:
+ $(BIN)../matitaclean.opt
+depend:
+ $(BIN)../matitadep -dot && rm depends.dot
+depend.opt:
+ $(BIN)../matitadep.opt -dot && rm depends.dot
--- /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 _ _ _).
+*)
--- /dev/null
+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/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
+Q/q/qplus.ma
+Q/q/qtimes.ma
+datatypes/constructors.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.
+
+
+
--- /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 "nat/minus.ma".
+include "list/list.ma".
+
+interpretation "list nth" 'nth = (nth _).
+interpretation "list nth" 'nth_appl l d i = (nth _ l d i).
+notation "\nth" with precedence 90 for @{'nth}.
+notation < "\nth \nbsp term 90 l \nbsp term 90 d \nbsp term 90 i"
+with precedence 69 for @{'nth_appl $l $d $i}.
+
+definition make_list ≝
+ λA:Type.λdef:nat→A.
+ let rec make_list (n:nat) on n ≝
+ match n with [ O ⇒ nil ? | S m ⇒ def m :: make_list m]
+ in make_list.
+
+interpretation "\mk_list appl" 'mk_list_appl f n = (make_list _ f n).
+interpretation "\mk_list" 'mk_list = (make_list _).
+notation "\mk_list" with precedence 90 for @{'mk_list}.
+notation < "\mk_list \nbsp term 90 f \nbsp term 90 n"
+with precedence 69 for @{'mk_list_appl $f $n}.
+
+notation "\len" with precedence 90 for @{'len}.
+interpretation "len" 'len = (length _).
+notation < "\len \nbsp term 90 l" with precedence 69 for @{'len_appl $l}.
+interpretation "len appl" 'len_appl l = (length _ l).
+
+lemma mk_list_ext: ∀T:Type.∀f1,f2:nat→T.∀n. (∀x.x<n → f1 x = f2 x) → \mk_list f1 n = \mk_list f2 n.
+intros 4;elim n; [reflexivity] simplify; rewrite > H1; [2: apply le_n]
+apply eq_f; apply H; intros; apply H1; apply (trans_le ??? H2); apply le_S; apply le_n;
+qed.
+
+lemma len_mk_list : ∀T:Type.∀f:nat→T.∀n.\len (\mk_list f n) = n.
+intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity;
+qed.
+
+record rel (rel_T : Type) : Type ≝ {
+ rel_op :2> rel_T → rel_T → Prop
+}.
+
+record trans_rel : Type ≝ {
+ o_T :> Type;
+ o_rel :> rel o_T;
+ o_tra : ∀x,y,z: o_T.o_rel x y → o_rel y z → o_rel x z
+}.
+
+lemma trans: ∀r:trans_rel.∀x,y,z:r.r x y → r y z → r x z.
+apply o_tra;
+qed.
+
+inductive sorted (lt : trans_rel): list (o_T lt) → Prop ≝
+| sorted_nil : sorted lt []
+| sorted_one : ∀x. sorted lt [x]
+| sorted_cons : ∀x,y,tl. lt x y → sorted lt (y::tl) → sorted lt (x::y::tl).
+
+lemma nth_nil: ∀T,i.∀def:T. \nth [] def i = def.
+intros; elim i; simplify; [reflexivity;] assumption; qed.
+
+lemma len_append: ∀T:Type.∀l1,l2:list T. \len (l1@l2) = \len l1 + \len l2.
+intros; elim l1; [reflexivity] simplify; rewrite < H; reflexivity;
+qed.
+
+coinductive non_empty_list (A:Type) : list A → Type :=
+| show_head: ∀x,l. non_empty_list A (x::l).
+
+lemma len_gt_non_empty :
+ ∀T.∀l:list T.O < \len l → non_empty_list T l.
+intros; cases l in H; [intros; cases (not_le_Sn_O ? H);] intros; constructor 1;
+qed.
+
+lemma sorted_tail: ∀r,x,l.sorted r (x::l) → sorted r l.
+intros; inversion H; intros; [destruct H1;|destruct H1;constructor 1;]
+destruct H4; assumption;
+qed.
+
+lemma sorted_skip: ∀r,x,y,l. sorted r (x::y::l) → sorted r (x::l).
+intros (r x y l H1); inversion H1; intros; [1,2: destruct H]
+destruct H4; inversion H2; intros; [destruct H4]
+[1: destruct H4; constructor 2;
+|2: destruct H7; constructor 3;
+ [ apply (o_tra ? ??? H H4); | apply (sorted_tail ??? H2);]]
+qed.
+
+lemma sorted_tail_bigger : ∀r,x,l,d.sorted r (x::l) → ∀i. i < \len l → r x (\nth l d i).
+intros 4; elim l; [ cases (not_le_Sn_O i H1);]
+cases i in H2;
+[2: intros; apply (H ? n);[apply (sorted_skip ???? H1)|apply le_S_S_to_le; apply H2]
+|1: intros; inversion H1; intros; [1,2: destruct H3]
+ destruct H6; simplify; assumption;]
+qed.
+
+(* move in nat/ *)
+lemma lt_n_plus_n_Sm : ∀n,m:nat.n < n + S m.
+intros; rewrite > sym_plus; apply (le_S_S n (m+n)); alias id "le_plus_n" = "cic:/matita/nat/le_arith/le_plus_n.con".
+apply (le_plus_n m n); qed.
+
+lemma nth_append_lt_len:
+ ∀T:Type.∀l1,l2:list T.∀def.∀i.i < \len l1 → \nth (l1@l2) def i = \nth l1 def i.
+intros 4; elim l1; [cases (not_le_Sn_O ? H)] cases i in H H1; simplify; intros;
+[reflexivity| rewrite < H;[reflexivity] apply le_S_S_to_le; apply H1]
+qed.
+
+lemma nth_append_ge_len:
+ ∀T:Type.∀l1,l2:list T.∀def.∀i.
+ \len l1 ≤ i → \nth (l1@l2) def i = \nth l2 def (i - \len l1).
+intros 4; elim l1; [ rewrite < minus_n_O; reflexivity]
+cases i in H1; simplify; intros; [cases (not_le_Sn_O ? H1)]
+apply H; apply le_S_S_to_le; apply H1;
+qed.
+
+lemma nth_len:
+ ∀T:Type.∀l1,l2:list T.∀def,x.
+ \nth (l1@x::l2) def (\len l1) = x.
+intros 2; elim l1;[reflexivity] simplify; apply H; qed.
+
+lemma sorted_head_smaller:
+ ∀r,l,p,d. sorted r (p::l) → ∀i.i < \len l → r p (\nth l d i).
+intros 2 (r l); elim l; [cases (not_le_Sn_O ? H1)] cases i in H2; simplify; intros;
+[1: inversion H1; [1,2: simplify; intros; destruct H3] intros; destruct H6; assumption;
+|2: apply (H p ?? n ?); [apply (sorted_skip ???? H1)] apply le_S_S_to_le; apply H2]
+qed.
+
+alias symbol "lt" = "natural 'less than'".
+lemma sorted_pivot:
+ ∀r,l1,l2,p,d. sorted r (l1@p::l2) →
+ (∀i. i < \len l1 → r (\nth l1 d i) p) ∧
+ (∀i. i < \len l2 → r p (\nth l2 d i)).
+intros 2 (r l); elim l;
+[1: split; [intros; cases (not_le_Sn_O ? H1);] intros;
+ apply sorted_head_smaller; assumption;
+|2: simplify in H1; cases (H ?? d (sorted_tail ??? H1));
+ lapply depth = 0 (sorted_head_smaller ??? d H1) as Hs;
+ split; simplify; intros;
+ [1: cases i in H4; simplify; intros;
+ [1: lapply depth = 0 (Hs (\len l1)) as HS;
+ rewrite > nth_len in HS; apply HS;
+ rewrite > len_append; simplify; apply lt_n_plus_n_Sm;
+ |2: apply (H2 n); apply le_S_S_to_le; apply H4]
+ |2: apply H3; assumption]]
+qed.
+
+coinductive cases_bool (p:bool) : bool → CProp ≝
+| case_true : p = true → cases_bool p true
+| cases_false : p = false → cases_bool p false.
+
+lemma case_b : ∀A:Type.∀f:A → bool. ∀x.cases_bool (f x) (f x).
+intros; cases (f x);[left;|right] reflexivity;
+qed.
+
+coinductive break_spec (T : Type) (n : nat) (l : list T) : list T → CProp ≝
+| break_to: ∀l1,x,l2. \len l1 = n → l = l1 @ [x] @ l2 → break_spec T n l l.
+
+lemma list_break: ∀T,n,l. n < \len l → break_spec T n l l.
+intros 2; elim n;
+[1: elim l in H; [cases (not_le_Sn_O ? H)]
+ apply (break_to ?? ? [] a l1); reflexivity;
+|2: cases (H l); [2: apply lt_S_to_lt; assumption;] cases l2 in H3; intros;
+ [1: rewrite < H2 in H1; rewrite > H3 in H1; rewrite > append_nil in H1;
+ rewrite > len_append in H1; rewrite > plus_n_SO in H1;
+ cases (not_le_Sn_n ? H1);
+ |2: apply (break_to ?? ? (l1@[x]) t l3);
+ [2: simplify; rewrite > associative_append; assumption;
+ |1: rewrite < H2; rewrite > len_append; rewrite > plus_n_SO; reflexivity]]]
+qed.
+
+include "logic/cprop_connectives.ma".
+
+definition eject_N ≝
+ λP.λp:∃x:nat.P x.match p with [ex_introT p _ ⇒ p].
+coercion eject_N.
+definition inject_N ≝ λP.λp:nat.λh:P p. ex_introT ? P p h.
+coercion inject_N with 0 1 nocomposites.
+
+coinductive find_spec (T:Type) (P:T→bool) (l:list T) (d:T) (res : nat) : nat → CProp ≝
+| found:
+ ∀i. i < \len l → P (\nth l d i) = true → res = i →
+ (∀j. j < i → P (\nth l d j) = false) → find_spec T P l d res i
+| not_found: ∀i. i = \len l → res = i →
+ (∀j.j < \len l → P (\nth l d j) = false) → find_spec T P l d res i.
+
+lemma find_lemma : ∀T.∀P:T→bool.∀l:list T.∀d.∃i.find_spec ? P l d i i.
+intros;
+letin find ≝ (
+ let rec aux (acc: nat) (l : list T) on l : nat ≝
+ match l with
+ [ nil ⇒ acc
+ | cons x tl ⇒
+ match P x with
+ [ false ⇒ aux (S acc) tl
+ | true ⇒ acc]]
+ in aux :
+ ∀acc,l1.∃p:nat.
+ ∀story. story @ l1 = l → acc = \len story →
+ find_spec ? P story d acc acc →
+ find_spec ? P (story @ l1) d p p);
+[4: clearbody find; cases (find 0 l);
+ lapply (H [] (refl_eq ??) (refl_eq ??)) as K;
+ [2: apply (not_found ?? [] d); intros; try reflexivity; cases (not_le_Sn_O ? H1);
+ |1: cases K; clear K;
+ [2: exists[apply (\len l)]
+ apply not_found; try reflexivity; apply H3;
+ |1: exists[apply i] apply found; try reflexivity; assumption;]]
+|1: intros; cases (aux (S n) l2); simplify; clear aux;
+ lapply depth = 0 (H5 (story@[t])) as K; clear H5;
+ change with (find_spec ? P (story @ ([t] @ l2)) d w w);
+ rewrite < associative_append; apply K; clear K;
+ [1: rewrite > associative_append; apply H2;
+ |2: rewrite > H3; rewrite > len_append; rewrite > sym_plus; reflexivity;
+ |3: cases H4; clear H4; destruct H7;
+ [2: rewrite > H5; rewrite > (?:S (\len story) = \len (story @ [t])); [2:
+ rewrite > len_append; rewrite > sym_plus; reflexivity;]
+ apply not_found; try reflexivity; intros; cases (cmp_nat (S j) (\len story));
+ [1: rewrite > (nth_append_lt_len ????? H8); apply H7; apply H8;
+ |2: rewrite > (nth_append_ge_len ????? (le_S_S_to_le ?? H8));
+ rewrite > (?: j - \len story = 0);[assumption]
+ rewrite > (?:j = \len story);[rewrite > minus_n_n; reflexivity]
+ apply le_to_le_to_eq; [2: apply le_S_S_to_le; assumption;]
+ rewrite > len_append in H4;rewrite > sym_plus in H4;
+ apply le_S_S_to_le; apply H4;]
+ |1: rewrite < H3 in H5; cases (not_le_Sn_n ? H5);]]
+|2: intros; cases H4; clear H4;
+ [1: destruct H7; rewrite > H3 in H5; cases (not_le_Sn_n ? H5);
+ |2: apply found; try reflexivity;
+ [1: rewrite > len_append; simplify; rewrite > H5; apply lt_n_plus_n_Sm;
+ |2: rewrite > H5; rewrite > nth_append_ge_len; [2: apply le_n]
+ rewrite < minus_n_n; assumption;
+ |3: intros; rewrite > H5 in H4; rewrite > nth_append_lt_len; [2:assumption]
+ apply H7; assumption]]
+|3: intros; rewrite > append_nil; assumption;]
+qed.
+
+lemma find : ∀T:Type.∀P:T→bool.∀l:list T.∀d:T.nat.
+intros; cases (find_lemma ? f l t); apply w; qed.
+
+lemma cases_find: ∀T,P,l,d. find_spec T P l d (find T P l d) (find T P l d).
+intros; unfold find; cases (find_lemma T P l d); simplify; assumption; qed.
+
+lemma list_elim_with_len:
+ ∀T:Type.∀P: nat → list T → CProp.
+ P O [] → (∀l,a,n.P (\len l) l → P (S n) (a::l)) →
+ ∀l.P (\len l) l.
+intros;elim l; [assumption] simplify; apply H1; apply H2;
+qed.
+
+lemma sorted_near:
+ ∀r,l. sorted r l → ∀i,d. S i < \len l → r (\nth l d i) (\nth l d (S i)).
+ intros 3; elim H;
+ [1: cases (not_le_Sn_O ? H1);
+ |2: simplify in H1; cases (not_le_Sn_O ? (le_S_S_to_le ?? H1));
+ |3: simplify; cases i in H4; intros; [apply H1]
+ apply H3; apply le_S_S_to_le; apply H4]
+qed.
+
+definition last ≝
+ λT:Type.λd.λl:list T. \nth l d (pred (\len l)).
+
+notation > "\last" non associative with precedence 90 for @{'last}.
+notation < "\last d l" non associative with precedence 70 for @{'last2 $d $l}.
+interpretation "list last" 'last = (last _).
+interpretation "list last applied" 'last2 d l = (last _ d l).
+
+definition head ≝
+ λT:Type.λd.λl:list T.\nth l d O.
+
+notation > "\hd" non associative with precedence 90 for @{'hd}.
+notation < "\hd d l" non associative with precedence 70 for @{'hd2 $d $l}.
+interpretation "list head" 'hd = (head _).
+interpretation "list head applied" 'hd2 d l = (head _ d l).
+
--- /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
--- /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/q_support.ma".
+include "models/list_support.ma".
+include "logic/cprop_connectives.ma".
+
+definition bar ≝ ℚ × (ℚ × ℚ).
+
+notation < "\rationals \sup 2" non associative with precedence 90 for @{'q2}.
+interpretation "Q x Q" 'q2 = (Prod Q Q).
+
+definition empty_bar : bar ≝ 〈Qpos one,〈OQ,OQ〉〉.
+notation "\rect" with precedence 90 for @{'empty_bar}.
+interpretation "q0" 'empty_bar = empty_bar.
+
+notation < "\ldots\rect\square\EmptySmallSquare\ldots" with precedence 90 for @{'lq2}.
+interpretation "lq2" 'lq2 = (list bar).
+
+definition q2_lt := mk_rel bar (λx,y:bar.\fst x < \fst y).
+
+interpretation "bar lt" 'lt x y = (rel_op _ q2_lt x y).
+
+lemma q2_trans : ∀a,b,c:bar. a < b → b < c → a < c.
+intros 3; cases a; cases b; cases c; unfold q2_lt; simplify; intros;
+apply (q_lt_trans ??? H H1);
+qed.
+
+definition q2_trel := mk_trans_rel bar q2_lt q2_trans.
+
+interpretation "bar lt" 'lt x y = (FunClass_2_OF_trans_rel q2_trel x y).
+
+definition canonical_q_lt : rel bar → trans_rel ≝ λx:rel bar.q2_trel.
+
+coercion canonical_q_lt with nocomposites.
+
+interpretation "bar lt" 'lt x y = (FunClass_2_OF_trans_rel (canonical_q_lt _) x y).
+
+definition nth_base ≝ λf,n. \fst (\nth f ▭ n).
+definition nth_height ≝ λf,n. \snd (\nth f ▭ n).
+
+record q_f : Type ≝ {
+ bars: list bar;
+ bars_sorted : sorted q2_lt bars;
+ bars_begin_OQ : nth_base bars O = OQ;
+ bars_end_OQ : nth_height bars (pred (\len bars)) = 〈OQ,OQ〉
+}.
+
+lemma len_bases_gt_O: ∀f.O < \len (bars f).
+intros; generalize in match (bars_begin_OQ f); cases (bars f); intros;
+[2: simplify; apply le_S_S; apply le_O_n;
+|1: normalize in H; destruct H;]
+qed.
+
+lemma all_bases_positive : ∀f:q_f.∀i. OQ < nth_base (bars f) (S i).
+intro f; generalize in match (bars_begin_OQ f); generalize in match (bars_sorted f);
+cases (len_gt_non_empty ?? (len_bases_gt_O f)); intros;
+cases (cmp_nat (\len l) i);
+[2: lapply (sorted_tail_bigger q2_lt ?? ▭ H ? H2) as K;
+ simplify in H1; rewrite < H1; apply K;
+|1: simplify; elim l in i H2;[simplify; rewrite > nth_nil; apply (q_pos_OQ one)]
+ cases n in H3; intros; [simplify in H3; cases (not_le_Sn_O ? H3)]
+ apply (H2 n1); simplify in H3; apply (le_S_S_to_le ?? H3);]
+qed.
+
+alias symbol "lt" (instance 9) = "Q less than".
+alias symbol "lt" (instance 7) = "natural 'less than'".
+alias symbol "lt" (instance 6) = "natural 'less than'".
+alias symbol "lt" (instance 5) = "Q less than".
+alias symbol "lt" (instance 4) = "natural 'less than'".
+alias symbol "lt" (instance 2) = "natural 'less than'".
+alias symbol "leq" = "Q less or equal than".
+coinductive value_spec (f : list bar) (i : ℚ) : ℚ × ℚ → CProp ≝
+| value_of : ∀j,q.
+ nth_height f j = q → nth_base f j < i → j < \len f →
+ (∀n.n<j → nth_base f n < i) →
+ (∀n.j < n → n < \len f → i ≤ nth_base f n) → value_spec f i q.
+
+definition match_pred ≝
+ λi.λx:bar.match q_cmp (Qpos i) (\fst x) with[ q_leq _ ⇒ true| q_gt _ ⇒ false].
+
+definition match_domain ≝
+ λf: list bar.λi:ratio. pred (find ? (match_pred i) f ▭).
+
+definition value_simple ≝
+ λf: list bar.λi:ratio. nth_height f (match_domain f i).
+
+alias symbol "lt" (instance 5) = "Q less than".
+alias symbol "lt" (instance 6) = "natural 'less than'".
+definition value_lemma :
+ ∀f:list bar.sorted q2_lt f → O < length bar f →
+ ∀i:ratio.nth_base f O < Qpos i → ∃p:ℚ×ℚ.value_spec f (Qpos i) p.
+intros (f bars_sorted_f len_bases_gt_O_f i bars_begin_OQ_f);
+exists [apply (value_simple f i);]
+apply (value_of ?? (match_domain f i));
+[1: reflexivity
+|2: unfold match_domain; cases (cases_find bar (match_pred i) f ▭);
+ [1: cases i1 in H H1 H2 H3; simplify; intros;
+ [1: generalize in match (bars_begin_OQ_f);
+ cases (len_gt_non_empty ?? (len_bases_gt_O_f)); simplify; intros;
+ assumption;
+ |2: cases (len_gt_non_empty ?? (len_bases_gt_O_f)) in H3;
+ intros; lapply (H3 n (le_n ?)) as K; unfold match_pred in K;
+ cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ n))) in K;
+ simplify; intros; [destruct H5] assumption]
+ |2: destruct H; cases (len_gt_non_empty ?? (len_bases_gt_O_f)) in H2;
+ simplify; intros; lapply (H (\len l) (le_n ?)) as K; clear H;
+ unfold match_pred in K; cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ (\len l)))) in K;
+ simplify; intros; [destruct H2] assumption;]
+|5: intro; unfold match_domain; cases (cases_find bar (match_pred i) f ▭); intros;
+ [1: generalize in match (bars_sorted_f);
+ cases (list_break ??? H) in H1; rewrite > H6;
+ rewrite < H1; simplify; rewrite > nth_len; unfold match_pred;
+ cases (q_cmp (Qpos i) (\fst x)); simplify;
+ intros (X Hs); [2: destruct X] clear X;
+ cases (sorted_pivot q2_lt ??? ▭ Hs);
+ cut (\len l1 ≤ n) as Hn; [2:
+ rewrite > H1; cases i1 in H4; simplify; intro X; [2: assumption]
+ apply lt_to_le; assumption;]
+ unfold nth_base; rewrite > (nth_append_ge_len ????? Hn);
+ cut (n - \len l1 < \len (x::l2)) as K; [2:
+ simplify; rewrite > H1; rewrite > (?:\len l2 = \len f - \len (l1 @ [x]));[2:
+ rewrite > H6; repeat rewrite > len_append; simplify;
+ repeat rewrite < plus_n_Sm; rewrite < plus_n_O; simplify;
+ rewrite > sym_plus; rewrite < minus_plus_m_m; reflexivity;]
+ rewrite > len_append; rewrite > H1; simplify; rewrite < plus_n_SO;
+ apply le_S_S; clear H1 H6 H7 Hs H8 H9 Hn x l2 l1 H4 H3 H2 H;
+ elim (\len f) in i1 n H5; [cases (not_le_Sn_O ? H);]
+ simplify; cases n2; [ repeat rewrite < minus_n_O; apply le_S_S_to_le; assumption]
+ cases n1 in H1; [intros; rewrite > eq_minus_n_m_O; apply le_O_n]
+ intros; simplify; apply H; apply le_S_S_to_le; assumption;]
+ cases (n - \len l1) in K; simplify; intros; [ assumption]
+ lapply (H9 ? (le_S_S_to_le ?? H10)) as W; apply (q_le_trans ??? H7);
+ apply q_lt_to_le; apply W;
+ |2: cases (not_le_Sn_n i1); rewrite > H in ⊢ (??%);
+ apply (trans_le ??? ? H4); cases i1 in H3; intros; apply le_S_S;
+ [ apply le_O_n; | assumption]]
+|3: unfold match_domain; cases (cases_find bar (match_pred i) f ▭); [
+ cases i1 in H; intros; simplify; [assumption]
+ apply lt_S_to_lt; assumption;]
+ rewrite > H; cases (\len f) in len_bases_gt_O_f; intros; [cases (not_le_Sn_O ? H3)]
+ simplify; apply le_n;
+|4: intros; unfold match_domain in H; cases (cases_find bar (match_pred i) f ▭) in H; simplify; intros;
+ [1: lapply (H3 n); [2: cases i1 in H4; intros [assumption] apply le_S; assumption;]
+ unfold match_pred in Hletin; cases (q_cmp (Qpos i) (\fst (\nth f ▭ n))) in Hletin;
+ simplify; intros; [destruct H6] assumption;
+ |2: destruct H; cases f in len_bases_gt_O_f H2 H3; clear H1; simplify; intros;
+ [cases (not_le_Sn_O ? H)] lapply (H1 n); [2: apply le_S; assumption]
+ unfold match_pred in Hletin; cases (q_cmp (Qpos i) (\fst (\nth (b::l) ▭ n))) in Hletin;
+ simplify; intros; [destruct H4] assumption;]]
+qed.
+
+lemma bars_begin_lt_Qpos : ∀q,r. nth_base (bars q) O<Qpos r.
+intros; rewrite > bars_begin_OQ; apply q_pos_OQ;
+qed.
+
+lemma value : q_f → ratio → ℚ × ℚ.
+intros; cases (value_lemma (bars q) ?? r);
+[ apply bars_sorted.
+| apply len_bases_gt_O;
+| apply w;
+| apply bars_begin_lt_Qpos;]
+qed.
+
+lemma cases_value : ∀f,i. value_spec (bars f) (Qpos i) (value f i).
+intros; unfold value;
+cases (value_lemma (bars f) (bars_sorted f) (len_bases_gt_O f) i (bars_begin_lt_Qpos f i));
+assumption;
+qed.
+
+definition same_values ≝ λl1,l2:q_f.∀input. value l1 input = value l2 input.
+
+definition same_bases ≝ λl1,l2:list bar. ∀i.\fst (\nth l1 ▭ i) = \fst (\nth l2 ▭ i).
+
+lemma same_bases_cons: ∀a,b,l1,l2.
+ same_bases l1 l2 → \fst a = \fst b → same_bases (a::l1) (b::l2).
+intros; intro; cases i; simplify; [assumption;] apply (H n);
+qed.
+
+alias symbol "lt" = "Q less than".
+lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x.
+intro; cases x; intros; [2:exists [apply r] reflexivity]
+cases (?:False);
+[ apply (q_lt_corefl ? H)| cases (q_lt_le_incompat ?? (q_neg_gt ?) (q_lt_to_le ?? H))]
+qed.
+
+notation < "x \blacksquare" non associative with precedence 50 for @{'unpos $x}.
+interpretation "hide unpos proof" 'unpos x = (unpos x _).
+
--- /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/q_bars.ma".
+
+(* move in nat/minus *)
+lemma minus_lt : ∀i,j. i < j → j - i = S (j - S i).
+intros 2;
+apply (nat_elim2 ???? i j); simplify; intros;
+[1: cases n in H; intros; rewrite < minus_n_O; [cases (not_le_Sn_O ? H);]
+ simplify; rewrite < minus_n_O; reflexivity;
+|2: cases (not_le_Sn_O ? H);
+|3: apply H; apply le_S_S_to_le; assumption;]
+qed.
+
+alias symbol "lt" = "bar lt".
+lemma inversion_sorted:
+ ∀a,l. sorted q2_lt (a::l) → Or (a < \hd ▭ l) (l = []).
+intros 2; elim l; [right;reflexivity] left; inversion H1; intros;
+[1,2:destruct H2| destruct H5; assumption]
+qed.
+
+lemma inversion_sorted2:
+ ∀a,b,l. sorted q2_lt (a::b::l) → a < b.
+intros; inversion H; intros; [1,2:destruct H1] destruct H4; assumption;
+qed.
+
+let rec copy (l : list bar) on l : list bar ≝
+ match l with
+ [ nil ⇒ []
+ | cons x tl ⇒ 〈\fst x, 〈OQ,OQ〉〉 :: copy tl].
+
+lemma sorted_copy:
+ ∀l:list bar.sorted q2_lt l → sorted q2_lt (copy l).
+intro l; elim l; [apply (sorted_nil q2_lt)] simplify;
+cases l1 in H H1; simplify; intros; [apply (sorted_one q2_lt)]
+apply (sorted_cons q2_lt); [2: apply H; apply (sorted_tail q2_lt ?? H1);]
+apply (inversion_sorted2 ??? H1);
+qed.
+
+lemma len_copy: ∀l. \len (copy l) = \len l.
+intro; elim l; [reflexivity] simplify; apply eq_f; assumption;
+qed.
+
+lemma copy_same_bases: ∀l. same_bases l (copy l).
+intros; elim l; [intro; reflexivity] intro; simplify; cases i; [reflexivity]
+simplify; apply (H n);
+qed.
+
+lemma copy_OQ : ∀l,n.nth_height (copy l) n = 〈OQ,OQ〉.
+intro; elim l; [elim n;[reflexivity] simplify; assumption]
+simplify; cases n; [reflexivity] simplify; apply (H n1);
+qed.
+
+lemma prepend_sorted_with_same_head:
+ ∀r,x,l1,l2,d1,d2.
+ sorted r (x::l1) → sorted r l2 →
+ (r x (\nth l1 d1 O) → r x (\nth l2 d2 O)) → (l1 = [] → r x d1) →
+ sorted r (x::l2).
+intros 8 (R x l1 l2 d1 d2 Sl1 Sl2); inversion Sl1; inversion Sl2;
+intros; destruct; try assumption; [3: apply (sorted_one R);]
+[1: apply sorted_cons;[2:assumption] apply H2; apply H3; reflexivity;
+|2: apply sorted_cons;[2: assumption] apply H5; apply H6; reflexivity;
+|3: apply sorted_cons;[2: assumption] apply H5; assumption;
+|4: apply sorted_cons;[2: assumption] apply H8; apply H4;]
+qed.
+
+lemma move_head_sorted: ∀x,l1,l2.
+ sorted q2_lt (x::l1) → sorted q2_lt l2 → nth_base l2 O = nth_base l1 O →
+ l1 ≠ [] → sorted q2_lt (x::l2).
+intros; apply (prepend_sorted_with_same_head q2_lt x l1 l2 ▭ ▭);
+try assumption; intros; unfold nth_base in H2; whd in H4;
+[1: rewrite < H2 in H4; assumption;
+|2: cases (H3 H4);]
+qed.
+
+
+lemma sort_q2lt_same_base:
+ ∀b,h1,h2,l. sorted q2_lt (〈b,h1〉::l) → sorted q2_lt (〈b,h2〉::l).
+intros; cases (inversion_sorted ?? H); [2: rewrite > H1; apply (sorted_one q2_lt)]
+lapply (sorted_tail q2_lt ?? H) as K; clear H; cases l in H1 K; simplify; intros;
+[apply (sorted_one q2_lt);|apply (sorted_cons q2_lt);[2: assumption] apply H]
+qed.
+
+lemma value_head : ∀a,l,i.Qpos i ≤ \fst a → value_simple (a::l) i = \snd a.
+intros; unfold value_simple; unfold match_domain; cases (cases_find bar (match_pred i) (a::l) ▭);
+[1: cases i1 in H2 H3 H4; intros; [reflexivity] lapply (H4 O) as K; [2: apply le_S_S; apply le_O_n;]
+ simplify in K; unfold match_pred in K; cases (q_cmp (Qpos i) (\fst a)) in K;
+ simplify; intros; [destruct H6] lapply (q_le_lt_trans ??? H H5) as K; cases (q_lt_corefl ? K);
+|2: cases (?:False); lapply (H3 0); [2: simplify; apply le_S_S; apply le_O_n;]
+ unfold match_pred in Hletin; simplify in Hletin; cases (q_cmp (Qpos i) (\fst a)) in Hletin;
+ simplify; intros; [destruct H5] lapply (q_le_lt_trans ??? H H4); apply (q_lt_corefl ? Hletin);]
+qed.
+
+lemma value_unit : ∀x,i. value_simple [x] i = \snd x.
+intros; unfold value_simple; unfold match_domain;
+cases (cases_find bar (match_pred i) [x] ▭);
+[1: cases i1 in H; intros; [reflexivity] simplify in H;
+ cases (not_le_Sn_O ? (le_S_S_to_le ?? H));
+|2: simplify in H; destruct H; reflexivity;]
+qed.
+
+lemma value_tail :
+ ∀a,b,l,i.\fst a < Qpos i → \fst b ≤ Qpos i → value_simple (a::b::l) i = value_simple (b::l) i.
+intros; unfold value_simple; unfold match_domain;
+cases (cases_find bar (match_pred i) (a::b::l) ▭);
+[1: cases i1 in H3 H2 H4 H5; intros 1; simplify in ⊢ (? ? (? ? %) ?→?); unfold in ⊢ (? ? % ?→?); intros;
+ [1: cases (?:False); cases (q_cmp (Qpos i) (\fst a)) in H3; simplify; intros;[2: destruct H6]
+ apply (q_lt_corefl ? (q_lt_le_trans ??? H H3));
+ |2:
+
+normalize in ⊢ (? ? % ?→?); simplify;
+[1: rewrite > (value_head);
+
+lemma value_copy :
+ ∀l,i.rewrite > (value_u
+ value_simple (copy l) i = 〈OQ,OQ〉.
+intros; elim l;
+[1: reflexivity;
+|2: cases l1 in H; intros; simplify in ⊢ (? ? (? % ?) ?);
+ [1: rewrite > (value_unit); reflexivity;
+ |2: cases (q_cmp (\fst b) (Qpos i));
+
+ change with (\fst ▭ = \lamsimplify in ⊢ (? ? (? % ?) ?); unfold value_simple; unfold match_domain;
+ cases (cases_find bar (match_pred i) [〈\fst x,〈OQ,OQ〉〉] ▭);
+ [1: simplify in H1:(??%%);
+
+ unfold match_pred;
+ rewrite > (value_unit 〈\fst a,〈OQ,OQ〉〉); reflexivity;
+|2: intros; simplify in H2 H3 H4 ⊢ (? ? (? % ? ? ? ?) ?);
+ cases (q_cmp (Qpos i) (\fst b));
+ [2: rewrite > (value_tail ??? H2 H3 ? H4 H1); apply H;
+ |1: rewrite > (value_head ??? H2 H3 ? H4 H1); reflexivity]]
+qed.
+
\ 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 "russell_support.ma".
+include "models/q_copy.ma".
+(*
+definition rebase_spec ≝
+ λl1,l2:q_f.λp:q_f × q_f.
+ And3
+ (same_bases (bars (\fst p)) (bars (\snd p)))
+ (same_values l1 (\fst p))
+ (same_values l2 (\snd p)).
+
+inductive rebase_cases : list bar → list bar → (list bar) × (list bar) → Prop ≝
+| rb_fst_full : ∀b,h1,xs.
+ rebase_cases (〈b,h1〉::xs) [] 〈〈b,h1〉::xs,〈b,〈OQ,OQ〉〉::copy xs〉
+| rb_snd_full : ∀b,h1,ys.
+ rebase_cases [] (〈b,h1〉::ys) 〈〈b,〈OQ,OQ〉〉::copy ys,〈b,h1〉::ys〉
+| rb_all_full : ∀b,h1,h2,h3,h4,xs,ys,r1,r2.
+ \snd(\last ▭ (〈b,h1〉::xs)) = \snd(\last ▭ (〈b,h3〉::r1)) →
+ \snd(\last ▭ (〈b,h2〉::ys)) = \snd(\last ▭ (〈b,h4〉::r2)) →
+ rebase_cases (〈b,h1〉::xs) (〈b,h2〉::ys) 〈〈b,h3〉::r1,〈b,h4〉::r2〉
+| rb_all_full_l : ∀b1,b2,h1,h2,xs,ys,r1,r2.
+ \snd(\last ▭ (〈b1,h1〉::xs)) = \snd(\last ▭ (〈b1,h1〉::r1)) →
+ \snd(\last ▭ (〈b2,h2〉::ys)) = \snd(\last ▭ (〈b1,h2〉::r2)) →
+ b1 < b2 →
+ rebase_cases (〈b1,h1〉::xs) (〈b2,h2〉::ys) 〈〈b1,h1〉::r1,〈b1,〈OQ,OQ〉〉::r2〉
+| rb_all_full_r : ∀b1,b2,h1,h2,xs,ys,r1,r2.
+ \snd(\last ▭ (〈b1,h1〉::xs)) = \snd(\last ▭ (〈b2,h1〉::r1)) →
+ \snd(\last ▭ (〈b2,h2〉::ys)) = \snd(\last ▭ (〈b2,h2〉::r2)) →
+ b2 < b1 →
+ rebase_cases (〈b1,h1〉::xs) (〈b2,h2〉::ys) 〈〈b2,〈OQ,OQ〉〉::r1,〈b2,h2〉::r2〉
+| rb_all_empty : rebase_cases [] [] 〈[],[]〉.
+
+alias symbol "pi2" = "pair pi2".
+alias symbol "pi1" = "pair pi1".
+alias symbol "leq" = "natural 'less or equal to'".
+inductive rebase_spec_aux_p (l1, l2:list bar) (p:(list bar) × (list bar)) : Prop ≝
+| prove_rebase_spec_aux:
+ rebase_cases l1 l2 p →
+ (sorted q2_lt (\fst p)) →
+ (sorted q2_lt (\snd p)) →
+ (same_bases (\fst p) (\snd p)) →
+ (same_values_simpl l1 (\fst p)) →
+ (same_values_simpl l2 (\snd p)) →
+ rebase_spec_aux_p l1 l2 p.
+
+lemma aux_preserves_sorting:
+ ∀b,b3,l2,l3,w. rebase_cases l2 l3 w →
+ sorted q2_lt (b::l2) → sorted q2_lt (b3::l3) → \fst b3 = \fst b →
+ sorted q2_lt (\fst w) → sorted q2_lt (\snd w) →
+ same_bases (\fst w) (\snd w) →
+ sorted q2_lt (b :: \fst w).
+intros 6; cases H; simplify; intros; clear H;
+[ apply (sorted_cons q2_lt); [2:assumption] apply (inversion_sorted2 ??? H1);
+| apply (sorted_cons q2_lt); [2:assumption]
+ whd; rewrite < H3; apply (inversion_sorted2 ??? H2);
+| apply (sorted_cons q2_lt); [2:assumption] apply (inversion_sorted2 ??? H3);
+| apply (sorted_cons q2_lt); [2:assumption] apply (inversion_sorted2 ??? H4);
+| apply (sorted_cons q2_lt); [2:assumption]
+ whd; rewrite < H6; apply (inversion_sorted2 ??? H5);
+| apply (sorted_one q2_lt);]
+qed.
+
+lemma aux_preserves_sorting2:
+ ∀b,b3,l2,l3,w. rebase_cases l2 l3 w →
+ sorted q2_lt (b::l2) → sorted q2_lt (b3::l3) → \fst b3 = \fst b →
+ sorted q2_lt (\fst w) → sorted q2_lt (\snd w) → same_bases (\fst w) (\snd w) →
+ sorted q2_lt (b :: \snd w).
+intros 6; cases H; simplify; intros; clear H;
+[ apply (sorted_cons q2_lt); [2:assumption] apply (inversion_sorted2 ??? H1);
+| apply (sorted_cons q2_lt); [2:assumption]
+ whd; rewrite < H3; apply (inversion_sorted2 ??? H2);
+| apply (sorted_cons q2_lt); [2: assumption] apply (inversion_sorted2 ??? H3);
+| apply (sorted_cons q2_lt); [2: assumption] apply (inversion_sorted2 ??? H4);
+| apply (sorted_cons q2_lt); [2: assumption]
+ whd; rewrite < H6; apply (inversion_sorted2 ??? H5);
+| apply (sorted_one q2_lt);]
+qed.
+*)
+
+
+
+definition rebase_spec_aux ≝
+ λl1,l2
+ :list bar.λp:(list bar) × (list bar).
+ sorted q2_lt l1 → (\snd (\last ▭ l1) = 〈OQ,OQ〉) →
+ sorted q2_lt l2 → (\snd (\last ▭ l2) = 〈OQ,OQ〉) →
+ rebase_spec_aux_p l1 l2 p.
+
+alias symbol "lt" = "Q less than".
+alias symbol "Q" = "Rationals".
+axiom q_unlimited: ∀x:ℚ.∃y:ratio.x<Qpos y.
+axiom q_halving: ∀x,y:ℚ.∃z:ℚ.x<z ∧ z<y.
+alias symbol "not" = "logical not".
+axiom q_not_OQ_lt_Qneg: ∀r. ¬ (OQ < Qneg r).
+lemma same_values_unit_OQ:
+ ∀b1,b2,h1,l. OQ < b2 → b2 < b1 → sorted q2_lt (〈b1,h1〉::l) →
+ sorted q2_lt [〈b2,〈OQ,OQ〉〉] →
+ same_values_simpl (〈b1,h1〉::l) [〈b2,〈OQ,OQ〉〉] → h1 = 〈OQ,OQ〉.
+intros 5 (b1 b2 h1 l POS); cases l;
+[1: intros; cases (q_unlimited b1); cut (b2 < Qpos w); [2:apply (q_lt_trans ??? H H4);]
+ lapply (H3 H1 ? H2 ? w H4 Hcut) as K; simplify; [1,2: autobatch]
+ rewrite > (value_unit 〈b1,h1〉) in K;
+ rewrite > (value_unit 〈b2,〈OQ,OQ〉〉) in K; assumption;
+|2: intros; unfold in H3; lapply depth=0 (H3 H1 ? H2 ?) as K; [1,2:simplify; autobatch]
+ clear H3; cases (q_halving b1 (b1 + \fst p)) (w Pw); cases w in Pw; intros;
+ [cases (q_lt_le_incompat ?? POS); apply q_lt_to_le; cases H3;
+ apply (q_lt_trans ???? H4); assumption;
+ |3: elim H3; lapply (q_lt_trans ??? H H4); lapply (q_lt_trans ??? POS Hletin);
+ cases (q_not_OQ_lt_Qneg ? Hletin1);
+ | cases H3; lapply (K r);
+ [2: simplify; assumption
+ |3: simplify; apply (q_lt_trans ???? H4); assumption;
+ |rewrite > (value_head b1,h1 .. q) in Hletin;
+
+
+
+ (* MANCA che le basi sono positive,
+ poi con halving prendi tra b1 e \fst p e hai h1=OQ,OQ*)
+
+
+definition eject ≝
+ λP.λp:∃x:(list bar) × (list bar).P x.match p with [ex_introT p _ ⇒ p].
+coercion eject.
+definition inject ≝ λP.λp:(list bar) × (list bar).λh:P p. ex_introT ? P p h.
+coercion inject with 0 1 nocomposites.
+
+definition rebase: ∀l1,l2:q_f.∃p:q_f × q_f.rebase_spec l1 l2 p.
+intros 2 (f1 f2); cases f1 (b1 Hs1 Hb1 He1); cases f2 (b2 Hs2 Hb2 He2); clear f1 f2;
+alias symbol "leq" = "natural 'less or equal to'".
+alias symbol "minus" = "Q minus".
+letin aux ≝ (
+let rec aux (l1,l2:list bar) (n : nat) on n : (list bar) × (list bar) ≝
+match n with
+[ O ⇒ 〈[], []〉
+| S m ⇒
+ match l1 with
+ [ nil ⇒ 〈copy l2, l2〉
+ | cons he1 tl1 ⇒
+ match l2 with
+ [ nil ⇒ 〈l1, copy l1〉
+ | cons he2 tl2 ⇒
+ let base1 ≝ \fst he1 in
+ let base2 ≝ \fst he2 in
+ let height1 ≝ \snd he1 in
+ let height2 ≝ \snd he2 in
+ match q_cmp base1 base2 with
+ [ q_leq Hp1 ⇒
+ match q_cmp base2 base1 with
+ [ q_leq Hp2 ⇒
+ let rc ≝ aux tl1 tl2 m in
+ 〈he1 :: \fst rc,he2 :: \snd rc〉
+ | q_gt Hp ⇒
+ let rest ≝ base2 - base1 in
+ let rc ≝ aux tl1 (〈rest,height2〉 :: tl2) m in
+ 〈〈base1,height1〉 :: \fst rc,〈base1,height2〉 :: \snd rc〉]
+ | q_gt Hp ⇒
+ let rest ≝ base1 - base2 in
+ let rc ≝ aux (〈rest,height1〉 :: tl1) tl2 m in
+ 〈〈base2,height1〉 :: \fst rc,〈base2,height2〉 :: \snd rc〉]]]]
+in aux : ∀l1,l2,m.∃z.\len l1 + \len l2 ≤ m → rebase_spec_aux l1 l2 z);
+[7: clearbody aux; cases (aux b1 b2 (\len b1 + \len b2)) (res Hres);
+ exists; [split; constructor 1; [apply (\fst res)|5:apply (\snd res)]]
+ [1,4: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); assumption;
+ |2,5: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); clear Hres aux;
+ lapply (H3 O) as K; clear H1 H2 H3 H4 H5; unfold nth_base;
+ cases H in K He1 He2 Hb1 Hb2; simplify; intros; assumption;
+ |3,6: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); clear Hres aux;
+ cases H in He1 He2; simplify; intros;
+ [1,6,8,12: assumption;
+ |2,7: rewrite > len_copy; generalize in match (\len ?); intro X;
+ cases X; [1,3: reflexivity] simplify;
+ [apply (copy_OQ ys n);|apply (copy_OQ xs n);]
+ |3,4: rewrite < H6; assumption;
+ |5: cases r1 in H6; simplify; intros; [reflexivity] rewrite < H6; assumption;
+ |9,11: rewrite < H7; assumption;
+ |10: cases r2 in H7; simplify; intros; [reflexivity] rewrite < H7; assumption]]
+ split; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); clear Hres; unfold same_values; intros;
+ [1: assumption
+ |2,3: simplify in match (\snd 〈?,?〉); simplify in match (\fst 〈?,?〉);
+ apply same_values_simpl_to_same_values; assumption]
+|3: cut (\fst b3 = \fst b) as E; [2: apply q_le_to_le_to_eq; assumption]
+ clear H6 H5 H4 H3 He2 Hb2 Hs2 b2 He1 Hb1 Hs1 b1; cases (aux l2 l3 n1) (rc Hrc);
+ clear aux; intro K; simplify in K; rewrite <plus_n_Sm in K;
+ lapply le_S_S_to_le to K as W; lapply lt_to_le to W as R;
+ simplify in match (? ≪rc,Hrc≫); intros (Hsbl2 Hendbl2 Hsb3l3 Hendb3l3);
+ change in Hendbl2 with (\snd (\last ▭ (b::l2)) = 〈OQ,OQ〉);
+ change in Hendb3l3 with (\snd (\last ▭ (b3::l3)) = 〈OQ,OQ〉);
+ cases (Hrc R) (RC S1 S2 SB SV1 SV2); clear Hrc R W K;
+ [2,4: apply (sorted_tail q2_lt);[apply b|3:apply b3]assumption;
+ |3: cases l2 in Hendbl2; simplify; intros; [reflexivity] assumption;
+ |5: cases l3 in Hendb3l3; simplify; intros; [reflexivity] assumption;]
+ constructor 1; simplify in match (\fst 〈?,?〉); simplify in match (\snd 〈?,?〉);
+ [1: cases b in E Hsbl2 Hendbl2; cases b3 in Hsb3l3 Hendb3l3; intros (Hsbl3 Hendbl2 E Hsb3l2 Hendb3l3);
+ simplify in E; destruct E; constructor 3;
+ [1: clear Hendbl2 Hsbl3 SV2 SB S2;
+ cases RC in S1 SV1 Hsb3l2 Hendb3l3; intros;
+ [1,6: reflexivity;
+ |3,4: assumption;
+ |5: simplify in H6:(??%) ⊢ %; rewrite > H3; cases r1 in H6; intros [2:reflexivity]
+ use same_values_unit_OQ;
+
+ |2: simplify in H3:(??%) ⊢ %; rewrite > H3; rewrite > len_copy; elim (\len ys); [reflexivity]
+ symmetry; apply (copy_OQ ys n2);
+ | cases H8 in H5 H7; simplify; intros; [2,6:reflexivity|3,4,5: assumption]
+ simplify; rewrite > H5; rewrite > len_copy; elim (\len xs); [reflexivity]
+ symmetry; apply (copy_OQ xs n2);]
+ |2: apply (aux_preserves_sorting ? b3 ??? H8); assumption;
+ |3: apply (aux_preserves_sorting2 ? b3 ??? H8); try assumption;
+ try reflexivity; cases (inversion_sorted ?? H4);[2:rewrite >H3; apply (sorted_one q2_lt);]
+ cases l2 in H3 H4; intros; [apply (sorted_one q2_lt)]
+ apply (sorted_cons q2_lt);[2:apply (sorted_tail q2_lt ?? H3);] whd;
+ rewrite > E; assumption;
+ |4: apply I
+ |5: apply I
+ |6: intro; elim i; intros; simplify; solve [symmetry;assumption|apply H13]
+ |7: unfold; intros; clear H9 H10 H11 H12 H13; simplify in Hi1 Hi2 H16 H18;
+ cases H8 in H14 H15 H17 H3 H16 H18 H5 H6;
+ simplify in match (\fst 〈?,?〉); simplify in match (\snd 〈?,?〉); intros;
+ [1: reflexivity;
+ |2: simplify in H3; rewrite > (value_unit b); rewrite > H3; symmetry;
+ cases b in H3 H12 Hi2; intros 2; simplify in H12; rewrite > H12;
+ intros; change in ⊢ (? ? (? % ? ? ? ?) ?) with (copy (〈q,〈OQ,OQ〉〉::〈b1,〈OQ,OQ〉〉::ys));
+ apply (value_copy (〈q,〈OQ,OQ〉〉::〈b1,〈OQ,OQ〉〉::ys));
+ |3: apply (same_value_tail b b1 h1 h3 xs r1 input); assumption;
+ |4: apply (same_value_tail b b1 h1 h1 xs r1 input); assumption;
+ |5: simplify in H9; STOP
+
+ |6: reflexivity;]
+
+ ]
+ |8:
+
+
+include "Q/q/qtimes.ma".
+
+let rec area (l:list bar) on l ≝
+ match l with
+ [ nil ⇒ OQ
+ | cons he tl ⇒ area tl + Qpos (\fst he) * ⅆ[OQ,\snd he]].
+
+alias symbol "pi1" = "exT \fst".
+alias symbol "minus" = "Q minus".
+alias symbol "exists" = "CProp exists".
+definition minus_spec_bar ≝
+ λf,g,h:list bar.
+ same_bases f g → len f = len g →
+ ∀s,i:ℚ. \snd (\fst (value (mk_q_f s h) i)) =
+ \snd (\fst (value (mk_q_f s f) i)) - \snd (\fst (value (mk_q_f s g) i)).
+
+definition minus_spec ≝
+ λf,g:q_f.
+ ∃h:q_f.
+ ∀i:ℚ. \snd (\fst (value h i)) =
+ \snd (\fst (value f i)) - \snd (\fst (value g i)).
+
+definition eject_bar : ∀P:list bar → CProp.(∃l:list bar.P l) → list bar ≝
+ λP.λp.match p with [ex_introT x _ ⇒ x].
+definition inject_bar ≝ ex_introT (list bar).
+
+coercion inject_bar with 0 1 nocomposites.
+coercion eject_bar with 0 0 nocomposites.
+
+lemma minus_q_f : ∀f,g. minus_spec f g.
+intros;
+letin aux ≝ (
+ let rec aux (l1, l2 : list bar) on l1 ≝
+ match l1 with
+ [ nil ⇒ []
+ | cons he1 tl1 ⇒
+ match l2 with
+ [ nil ⇒ []
+ | cons he2 tl2 ⇒ 〈\fst he1, \snd he1 - \snd he2〉 :: aux tl1 tl2]]
+ in aux : ∀l1,l2 : list bar.∃h.minus_spec_bar l1 l2 h);
+[2: intros 4; simplify in H3; destruct H3;
+|3: intros 4; simplify in H3; cases l1 in H2; [2: intro X; simplify in X; destruct X]
+ intros; rewrite > (value_OQ_e (mk_q_f s []) i); [2: reflexivity]
+ rewrite > q_elim_minus; rewrite > q_plus_OQ; reflexivity;
+|1: cases (aux l2 l3); unfold in H2; intros 4;
+ simplify in ⊢ (? ? (? ? ? (? ? ? (? % ?))) ?);
+ cases (q_cmp i (s + Qpos (\fst b)));
+
+
+
+definition excess ≝
+ λf,g.∃i.\snd (\fst (value f i)) < \snd (\fst (value g 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 "Q/q/qtimes.ma".
+include "Q/q/qplus.ma".
+include "logic/cprop_connectives.ma".
+
+interpretation "Q" 'Q = Q.
+
+(* group over Q *)
+axiom qp : ℚ → ℚ → ℚ.
+
+interpretation "Q plus" 'plus x y = (qp x y).
+interpretation "Q minus" 'minus x y = (qp x (Qopp y)).
+
+axiom q_plus_OQ: ∀x:ℚ.x + OQ = x.
+axiom q_plus_sym: ∀x,y:ℚ.x + y = y + x.
+axiom q_plus_minus: ∀x.x - x = OQ.
+axiom q_plus_assoc: ∀x,y,z.x + (y + z) = x + y + z.
+axiom q_opp_plus: ∀x,y,z:Q. Qopp (y + z) = Qopp y + Qopp z.
+
+(* order over Q *)
+axiom qlt : ℚ → ℚ → Prop.
+axiom qle : ℚ → ℚ → Prop.
+interpretation "Q less than" 'lt x y = (qlt x y).
+interpretation "Q less or equal than" 'leq x y = (qle x y).
+
+inductive q_comparison (a,b:ℚ) : CProp ≝
+ | q_leq : a ≤ b → q_comparison a b
+ | q_gt : b < a → q_comparison a b.
+
+axiom q_cmp:∀a,b:ℚ.q_comparison a b.
+
+inductive q_le_elimination (a,b:ℚ) : CProp ≝
+| q_le_from_eq : a = b → q_le_elimination a b
+| q_le_from_lt : a < b → q_le_elimination a b.
+
+axiom q_le_cases : ∀x,y:ℚ.x ≤ y → q_le_elimination x y.
+
+axiom q_le_to_le_to_eq : ∀x,y. x ≤ y → y ≤ x → x = y.
+
+axiom q_le_plus_l: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c.
+axiom q_le_plus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b.
+axiom q_lt_plus_l: ∀a,b,c:ℚ. a < c - b → a + b < c.
+axiom q_lt_plus_r: ∀a,b,c:ℚ. a - b < c → a < c + b.
+
+axiom q_lt_opp_opp: ∀a,b.b < a → Qopp a < Qopp b.
+
+axiom q_le_n: ∀x. x ≤ x.
+axiom q_lt_to_le: ∀a,b:ℚ.a < b → a ≤ b.
+
+axiom q_lt_corefl: ∀x:Q.x < x → False.
+axiom q_lt_le_incompat: ∀x,y:Q.x < y → y ≤ x → False.
+
+axiom q_neg_gt: ∀r:ratio.Qneg r < OQ.
+axiom q_pos_OQ: ∀x.OQ < Qpos x.
+
+axiom q_lt_trans: ∀x,y,z:Q. x < y → y < z → x < z.
+axiom q_lt_le_trans: ∀x,y,z:Q. x < y → y ≤ z → x < z.
+axiom q_le_lt_trans: ∀x,y,z:Q. x ≤ y → y < z → x < z.
+axiom q_le_trans: ∀x,y,z:Q. x ≤ y → y ≤ z → x ≤ z.
+
+axiom q_le_lt_OQ_plus_trans: ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y.
+axiom q_lt_le_OQ_plus_trans: ∀x,y:Q.OQ < x → OQ ≤ y → OQ < x + y.
+axiom q_le_OQ_plus_trans: ∀x,y:Q.OQ ≤ x → OQ ≤ y → OQ ≤ x + y.
+
+axiom q_leWl: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z.
+axiom q_ltWl: ∀x,y,z.OQ ≤ x → x + y < z → y < z.
+
+(* distance *)
+axiom q_dist : ℚ → ℚ → ℚ.
+
+notation "hbox(\dd [term 19 x, break term 19 y])" with precedence 90
+for @{'distance $x $y}.
+interpretation "ℚ distance" 'distance x y = (q_dist x y).
+
+axiom q_d_ge_OQ : ∀x,y:ℚ. OQ ≤ ⅆ[x,y].
+axiom q_d_OQ: ∀x:Q.ⅆ[x,x] = OQ.
+axiom q_d_noabs: ∀x,y. x ≤ y → ⅆ[y,x] = y - x.
+axiom q_d_sym: ∀x,y. ⅆ[x,y] = ⅆ[y,x].
+
+lemma q_2opp: ∀x:ℚ.Qopp (Qopp x) = x.
+intros; cases x; reflexivity; qed.
+
+(* derived *)
+lemma q_lt_canc_plus_r:
+ ∀x,y,z:Q.x + z < y + z → x < y.
+intros; rewrite < (q_plus_OQ y); rewrite < (q_plus_minus z);
+rewrite > q_plus_assoc; apply q_lt_plus_r; rewrite > q_2opp; assumption;
+qed.
+
+lemma q_lt_inj_plus_r:
+ ∀x,y,z:Q.x < y → x + z < y + z.
+intros; apply (q_lt_canc_plus_r ?? (Qopp z));
+do 2 rewrite < q_plus_assoc; rewrite > q_plus_minus;
+do 2 rewrite > q_plus_OQ; assumption;
+qed.
+
+lemma q_le_inj_plus_r:
+ ∀x,y,z:Q.x ≤ y → x + z ≤ y + z.
+intros;cases (q_le_cases ?? H);
+[1: rewrite > H1; apply q_le_n;
+|2: apply q_lt_to_le; apply q_lt_inj_plus_r; assumption;]
+qed.
+
+lemma q_le_canc_plus_r:
+ ∀x,y,z:Q.x + z ≤ y + z → x ≤ y.
+intros; lapply (q_le_inj_plus_r ?? (Qopp z) H) as H1;
+do 2 rewrite < q_plus_assoc in H1;
+rewrite > q_plus_minus in H1; do 2 rewrite > q_plus_OQ in H1; 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/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
+baseuri=cic:/matita/dama
--- /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.
gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile;
(match center_on with
| None -> ()
- | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri));
- HExtlib.safe_remove tmpfile
+ | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri))
+(* HExtlib.safe_remove tmpfile *)
method private dependencies direction uri () =
let dbd = LibraryDb.instance () in
projects / helm.git / commitdiff
