From: Enrico Tassi Date: Thu, 20 Nov 2008 15:53:09 +0000 (+0000) Subject: dama into the library X-Git-Tag: make_still_working~4532 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6fbeff97e37927fd95b3aee3eb23b4309fc465c4;p=helm.git dama into the library --- diff --git a/helm/software/matita/library/dama/Makefile b/helm/software/matita/library/dama/Makefile new file mode 100644 index 000000000..92a16d1f0 --- /dev/null +++ b/helm/software/matita/library/dama/Makefile @@ -0,0 +1,16 @@ +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 diff --git a/helm/software/matita/library/dama/bishop_set.ma b/helm/software/matita/library/dama/bishop_set.ma new file mode 100644 index 000000000..d69bb2732 --- /dev/null +++ b/helm/software/matita/library/dama/bishop_set.ma @@ -0,0 +1,89 @@ +(**************************************************************************) +(* ___ *) +(* ||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 diff --git a/helm/software/matita/library/dama/bishop_set_rewrite.ma b/helm/software/matita/library/dama/bishop_set_rewrite.ma new file mode 100644 index 000000000..ff063e29a --- /dev/null +++ b/helm/software/matita/library/dama/bishop_set_rewrite.ma @@ -0,0 +1,87 @@ +(**************************************************************************) +(* ___ *) +(* ||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 _ _ _). +*) diff --git a/helm/software/matita/library/dama/depends b/helm/software/matita/library/dama/depends new file mode 100644 index 000000000..7e0d8968e --- /dev/null +++ b/helm/software/matita/library/dama/depends @@ -0,0 +1,35 @@ +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 diff --git a/helm/software/matita/library/dama/depends.png b/helm/software/matita/library/dama/depends.png new file mode 100644 index 000000000..1c10c2366 Binary files /dev/null and b/helm/software/matita/library/dama/depends.png differ diff --git a/helm/software/matita/library/dama/doc/apal.pdf b/helm/software/matita/library/dama/doc/apal.pdf new file mode 100644 index 000000000..393e71e9d Binary files /dev/null and b/helm/software/matita/library/dama/doc/apal.pdf differ diff --git a/helm/software/matita/library/dama/lebesgue.ma b/helm/software/matita/library/dama/lebesgue.ma new file mode 100644 index 000000000..f81c5ce46 --- /dev/null +++ b/helm/software/matita/library/dama/lebesgue.ma @@ -0,0 +1,125 @@ +(**************************************************************************) +(* ___ *) +(* ||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. + + + diff --git a/helm/software/matita/library/dama/models/discrete_uniformity.ma b/helm/software/matita/library/dama/models/discrete_uniformity.ma new file mode 100644 index 000000000..76461f3f4 --- /dev/null +++ b/helm/software/matita/library/dama/models/discrete_uniformity.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma new file mode 100644 index 000000000..58626ff15 --- /dev/null +++ b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma @@ -0,0 +1,138 @@ +(**************************************************************************) +(* ___ *) +(* ||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). diff --git a/helm/software/matita/library/dama/models/list_support.ma b/helm/software/matita/library/dama/models/list_support.ma new file mode 100644 index 000000000..eb70322a9 --- /dev/null +++ b/helm/software/matita/library/dama/models/list_support.ma @@ -0,0 +1,282 @@ +(**************************************************************************) +(* ___ *) +(* ||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 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). + diff --git a/helm/software/matita/library/dama/models/nat_lebesgue.ma b/helm/software/matita/library/dama/models/nat_lebesgue.ma new file mode 100644 index 000000000..d5e65215e --- /dev/null +++ b/helm/software/matita/library/dama/models/nat_lebesgue.ma @@ -0,0 +1,26 @@ + (**************************************************************************) +(* ___ *) +(* ||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. + diff --git a/helm/software/matita/library/dama/models/nat_order_continuous.ma b/helm/software/matita/library/dama/models/nat_order_continuous.ma new file mode 100644 index 000000000..5f00dc338 --- /dev/null +++ b/helm/software/matita/library/dama/models/nat_order_continuous.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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. + diff --git a/helm/software/matita/library/dama/models/nat_ordered_uniform.ma b/helm/software/matita/library/dama/models/nat_ordered_uniform.ma new file mode 100644 index 000000000..becbab2fb --- /dev/null +++ b/helm/software/matita/library/dama/models/nat_ordered_uniform.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/helm/software/matita/library/dama/models/nat_uniform.ma b/helm/software/matita/library/dama/models/nat_uniform.ma new file mode 100644 index 000000000..0b2d43563 --- /dev/null +++ b/helm/software/matita/library/dama/models/nat_uniform.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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 diff --git a/helm/software/matita/library/dama/models/q_bars.ma b/helm/software/matita/library/dama/models/q_bars.ma new file mode 100644 index 000000000..1d2107b7c --- /dev/null +++ b/helm/software/matita/library/dama/models/q_bars.ma @@ -0,0 +1,201 @@ +(**************************************************************************) +(* ___ *) +(* ||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 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 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 _). + diff --git a/helm/software/matita/library/dama/models/q_copy.ma b/helm/software/matita/library/dama/models/q_copy.ma new file mode 100644 index 000000000..de7384077 --- /dev/null +++ b/helm/software/matita/library/dama/models/q_copy.ma @@ -0,0 +1,146 @@ +(**************************************************************************) +(* ___ *) +(* ||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 diff --git a/helm/software/matita/library/dama/models/q_rebase.ma b/helm/software/matita/library/dama/models/q_rebase.ma new file mode 100644 index 000000000..f8243d6d1 --- /dev/null +++ b/helm/software/matita/library/dama/models/q_rebase.ma @@ -0,0 +1,299 @@ +(**************************************************************************) +(* ___ *) +(* ||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 (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 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)). + diff --git a/helm/software/matita/library/dama/models/q_support.ma b/helm/software/matita/library/dama/models/q_support.ma new file mode 100644 index 000000000..4f27f398a --- /dev/null +++ b/helm/software/matita/library/dama/models/q_support.ma @@ -0,0 +1,122 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/helm/software/matita/library/dama/nat_ordered_set.ma b/helm/software/matita/library/dama/nat_ordered_set.ma new file mode 100644 index 000000000..26e2f0d29 --- /dev/null +++ b/helm/software/matita/library/dama/nat_ordered_set.ma @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||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 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. + diff --git a/helm/software/matita/library/dama/ordered_set.ma b/helm/software/matita/library/dama/ordered_set.ma new file mode 100644 index 000000000..890164ea9 --- /dev/null +++ b/helm/software/matita/library/dama/ordered_set.ma @@ -0,0 +1,181 @@ +(**************************************************************************) +(* ___ *) +(* ||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). + diff --git a/helm/software/matita/library/dama/ordered_uniform.ma b/helm/software/matita/library/dama/ordered_uniform.ma new file mode 100644 index 000000000..5a712f127 --- /dev/null +++ b/helm/software/matita/library/dama/ordered_uniform.ma @@ -0,0 +1,243 @@ +(**************************************************************************) +(* ___ *) +(* ||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. + diff --git a/helm/software/matita/library/dama/property_exhaustivity.ma b/helm/software/matita/library/dama/property_exhaustivity.ma new file mode 100644 index 000000000..deddf8804 --- /dev/null +++ b/helm/software/matita/library/dama/property_exhaustivity.ma @@ -0,0 +1,171 @@ +(**************************************************************************) +(* ___ *) +(* ||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 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. diff --git a/helm/software/matita/library/dama/root b/helm/software/matita/library/dama/root new file mode 100644 index 000000000..c12f54b7e --- /dev/null +++ b/helm/software/matita/library/dama/root @@ -0,0 +1 @@ +baseuri=cic:/matita/dama diff --git a/helm/software/matita/library/dama/russell_support.ma b/helm/software/matita/library/dama/russell_support.ma new file mode 100644 index 000000000..deb5fc950 --- /dev/null +++ b/helm/software/matita/library/dama/russell_support.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/helm/software/matita/library/dama/sandwich.ma b/helm/software/matita/library/dama/sandwich.ma new file mode 100644 index 000000000..68bb4453c --- /dev/null +++ b/helm/software/matita/library/dama/sandwich.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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. + diff --git a/helm/software/matita/library/dama/sequence.ma b/helm/software/matita/library/dama/sequence.ma new file mode 100644 index 000000000..948d14f67 --- /dev/null +++ b/helm/software/matita/library/dama/sequence.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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). diff --git a/helm/software/matita/library/dama/supremum.ma b/helm/software/matita/library/dama/supremum.ma new file mode 100644 index 000000000..0de61b292 --- /dev/null +++ b/helm/software/matita/library/dama/supremum.ma @@ -0,0 +1,442 @@ +(**************************************************************************) +(* ___ *) +(* ||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 H3; apply H;] + |2: cases (?:False); change in Hp with (n "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 "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 _)). diff --git a/helm/software/matita/library/dama/uniform.ma b/helm/software/matita/library/dama/uniform.ma new file mode 100644 index 000000000..759037124 --- /dev/null +++ b/helm/software/matita/library/dama/uniform.ma @@ -0,0 +1,92 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 63cf77a16..d07f31b55 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -1109,8 +1109,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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