From: Enrico Tassi Date: Tue, 17 Jun 2008 14:30:28 +0000 (+0000) Subject: general reorganization and first (unconditional) proof of lebesgue over naturals X-Git-Tag: make_still_working~5019 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7e33e23e18dc5d008b3b3dc0052aa4d7b236415e;p=helm.git general reorganization and first (unconditional) proof of lebesgue over naturals --- diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index f2a739aa7..eafedec44 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,18 +1,23 @@ +sandwich.ma ordered_uniform.ma +property_sigma.ma ordered_uniform.ma russell_support.ma +uniform.ma supremum.ma bishop_set.ma ordered_set.ma -ordered_set.ma cprop_connectives.ma -cprop_connectives.ma logic/equality.ma -bishop_set_rewrite.ma bishop_set.ma sequence.ma nat/nat.ma -uniform.ma supremum.ma -supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma -nat_ordered_set.ma bishop_set.ma nat/compare.ma -property_sigma.ma ordered_uniform.ma russell_support.ma ordered_uniform.ma uniform.ma +supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma property_exhaustivity.ma ordered_uniform.ma property_sigma.ma +bishop_set_rewrite.ma bishop_set.ma +cprop_connectives.ma logic/equality.ma +nat_ordered_set.ma bishop_set.ma nat/compare.ma lebesgue.ma property_exhaustivity.ma sandwich.ma -sandwich.ma ordered_uniform.ma +ordered_set.ma cprop_connectives.ma russell_support.ma cprop_connectives.ma nat/nat.ma -models/uniformnat.ma bishop_set_rewrite.ma nat/le_arith.ma nat_ordered_set.ma ordered_uniform.ma russell_support.ma uniform.ma +models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma +models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma +models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma +models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma +models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma +models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma datatypes/constructors.ma logic/equality.ma nat/compare.ma diff --git a/helm/software/matita/contribs/dama/dama/depends.png b/helm/software/matita/contribs/dama/dama/depends.png new file mode 100644 index 000000000..767380377 Binary files /dev/null and b/helm/software/matita/contribs/dama/dama/depends.png differ diff --git a/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma b/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma new file mode 100644 index 000000000..8063ea0bf --- /dev/null +++ b/helm/software/matita/contribs/dama/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 (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n)); +|2: intros 4 (U H x Hx); simplify in Hx; + cases H (_ H1); cases (H1 x); apply H2; apply Hx; +|3: intros; cases H (_ PU); cases H1 (_ PV); + exists[apply (λx.U x ∧ V x)] split; + [1: exists[apply something] intro; cases (PU n); cases (PV n); + split; intros; try split;[apply H2;|apply H4] try assumption; + apply H3; cases H6; assumption; + |2: simplify; intros; assumption;] +|4: intros; cases H (_ PU); exists [apply U] split; + [1: exists [apply something] intro n; cases (PU n); + split; intros; try split;[apply H1;|apply H2] assumption; + |2: intros 2 (x Hx); cases Hx; cases H1; clear H1; + cases (PU 〈(fst x),x1〉); lapply (H4 H2) as H5; simplify in H5; + cases (PU 〈x1,(snd x)〉); lapply (H7 H3) as H8; simplify in H8; + generalize in match H5; generalize in match H8; + generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8; + cases x; simplify; intros; cases H1; clear H1; apply H4; + apply (eq_trans ???? H3 H2);] +|5: intros; cases H (_ H1); split; cases x; + [2: cases (H1 〈b,b1〉); intro; apply H2; cases (H1 〈b1,b〉); + lapply (H6 H4) as H7; apply eq_sym; apply H7; + |1: cases (H1 〈b1,b〉); intro; apply H2; cases (H1 〈b,b1〉); + lapply (H6 H4) as H7; apply eq_sym; apply H7;]] +qed. diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma new file mode 100644 index 000000000..04b861d41 --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma @@ -0,0 +1,133 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "models/nat_uniform.ma". +include "supremum.ma". +include "nat/le_arith.ma". +include "russell_support.ma". + +inductive cmp_cases (n,m:nat) : CProp ≝ + | cmp_lt : n < m → cmp_cases n m + | cmp_eq : n = m → cmp_cases n m + | cmp_gt : m < n → cmp_cases n m. + +lemma cmp_nat: ∀n,m.cmp_cases n m. +intros; generalize in match (nat_compare_to_Prop n m); +cases (nat_compare n m); intros; +[constructor 1|constructor 2|constructor 3] assumption; +qed. + +alias symbol "pi1" = "exT fst". +alias symbol "leq" = "natural 'less or equal to'". +lemma nat_dedekind_sigma_complete: + ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → + ∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j). +intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉); +fold normalize X; intros; cases H1; +letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = fst (a j)) ∨ (i < u ∧ s+i ≤ u + fst (a j))); (* s - aj <= max 0 (u - i) *) +letin m ≝ (hide ? ( + let rec aux i ≝ + match i with + [ O ⇒ O + | S m ⇒ + let pred ≝ aux m in + let apred ≝ a pred in + match cmp_nat (fst apred) s with + [ cmp_eq _ ⇒ pred + | cmp_gt nP ⇒ match ? in False return λ_.nat with [] + | cmp_lt nP ⇒ fst (H3 apred nP)]] + in aux + : + ∀i:nat.∃j:nat.spec i j));unfold spec in aux ⊢ %; +[1: apply (H2 pred nP); +|4: unfold X in H2; clear H4 n aux spec H3 H1 H X; + generalize in match H2; + generalize in match Hs; + generalize in match a; + clear H2 Hs a; cases u; intros (a Hs H); + [1: left; split; [apply le_n] + generalize in match H; + generalize in match Hs; + rewrite > (?:s = O); + [2: cases Hs; lapply (os_le_to_nat_le ?? H1); + apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin). + |1: intros; lapply (os_le_to_nat_le (fst (a O)) O (H2 O)); + lapply (le_n_O_to_eq ? Hletin); assumption;] + |2: right; cases Hs; rewrite > (sym_plus s O); split; [apply le_S_S; apply le_O_n]; + apply (trans_le ??? (os_le_to_nat_le ?? H1)); + apply le_plus_n_r;] +|2,3: clear H6; + generalize in match H5; clear H5; cases (aux n1); intros; + change in match (a 〈w,H5〉) in H6 ⊢ % with (a w); + cases H5; clear H5; cases H7; clear H7; + [1: left; split; [ apply (le_S ?? H5); | assumption] + |3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6); + |*: cut (u ≤ S n1 ∨ S n1 < u); + [2,4: cases (cmp_nat u (S n1)); + [1,4: left; apply lt_to_le; assumption + |2,5: rewrite > H7; left; apply le_n + |3,6: right; assumption ] + |*: cases Hcut; clear Hcut + [1,3: left; split; [1,3: assumption |2: symmetry; assumption] + cut (u = S n1); [2: apply le_to_le_to_eq; assumption ] + clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut; + cut (s = S (fst (a w))); + [2: apply le_to_le_to_eq; [2: assumption] + change in H8 with (s + n1 ≤ S (n1 + fst (a w))); + rewrite > plus_n_Sm in H8; rewrite > sym_plus in H8; + apply (le_plus_to_le ??? H8);] + cases (H3 (a w) H6); + change with (s = fst (a w1)); + change in H4 with (fst (a w) < fst (a w1)); + apply le_to_le_to_eq; [ rewrite > Hcut; assumption ] + apply (os_le_to_nat_le (fst (a w1)) s (H2 w1)); + |*: right; split; try assumption; + [1: rewrite > sym_plus in ⊢ (? ? %); + rewrite < H6; apply le_plus_r; assumption; + |2: cases (H3 (a w) H6); + change with (s + S n1 ≤ u + fst (a w1));rewrite < plus_n_Sm; + apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm; + apply (le_plus ???? (le_n ?) H9);]]]]] +clearbody m; unfold spec in m; clear spec; +letin find ≝ ( + let rec find i u on u : nat ≝ + match u with + [ O ⇒ (m i:nat) + | S w ⇒ match eqb (fst (a (m i))) s with + [ true ⇒ (m i:nat) + | false ⇒ find (S i) w]] + in find + : + ∀i,bound.∃j.i + bound = u → s = fst (a j)); +[1: cases (find (S n) n2); intro; change with (s = fst (a w)); + apply H6; rewrite < H7; simplify; apply plus_n_Sm; +|2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity +|3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1; + cases (m u); cases H4; clear H4; cases H5; clear H5; [assumption] + cases (not_le_Sn_n ? H4)] +clearbody find; cases (find O u); +exists [apply w]; intros; change with (s = fst (a j)); +rewrite > (H4 ?); [2: reflexivity] +apply le_to_le_to_eq; +[1: apply os_le_to_nat_le; + apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5)); +|2: apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);] + rewrite < (H4 ?); [2: reflexivity] apply le_n;] +qed. + +alias symbol "pi1" = "exT fst". +alias symbol "leq" = "natural 'less or equal to'". +axiom nat_dedekind_sigma_complete_r: + ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing → + ∀x.x is_infimum a → ∃i.∀j.i ≤ j → fst x = fst (a j). diff --git a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma new file mode 100644 index 000000000..228392dda --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.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 "lebesgue.ma". +include "models/nat_order_continuous.ma". + +alias symbol "pair" = "dependent pair". +theorem nat_lebesgue_oc: + ∀a:sequence ℕ.∀l,u:nat_ordered_uniform_space.∀H:∀i:nat.a i ∈ [l,u]. + ∀x:ℕ.a order_converges x → + x ∈ [l,u] ∧ + ∀h:x ∈ [l,u]. + uniform_converge {[l,u]} (⌊n,〈a n,H n〉⌋) 〈x,h〉. +intros; apply lebesgue_oc; [apply nat_us_is_oc] assumption; +qed. + diff --git a/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma b/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma new file mode 100644 index 000000000..b8e23cc38 --- /dev/null +++ b/helm/software/matita/contribs/dama/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/nat_dedekind_sigma_complete.ma". +include "models/nat_ordered_uniform.ma". + +lemma nat_us_is_oc: ∀l,u:ℕ.order_continuity (segment_ordered_uniform_space ℕ l u). +intros 4; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H; +[1: cases (nat_dedekind_sigma_complete l u a H1 ? H2); + exists [apply w1]; intros; + apply (restrict nat_ordered_uniform_space l u ??? H4); + generalize in match (H ? H5); + cases x; intro; + generalize in match (refl_eq ? (a i):a i = a i); + generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X; + intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify; + apply (us_phi1 nat_uniform_space ? H3); simplify; apply eq_reflexive; +|2: cases (nat_dedekind_sigma_complete_r l u a H1 ? H2); + exists [apply w1]; intros; + apply (restrict nat_ordered_uniform_space l u ??? H4); + generalize in match (H ? H5); + cases x; intro; + generalize in match (refl_eq ? (a i):a i = a i); + generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X; + intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify; + apply (us_phi1 nat_uniform_space ? H3); simplify; apply eq_reflexive;] +qed. + diff --git a/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma new file mode 100644 index 000000000..d1ea3e46b --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "models/nat_uniform.ma". +include "bishop_set_rewrite.ma". +include "ordered_uniform.ma". + +definition nat_ordered_uniform_space:ordered_uniform_space. + apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ))); +simplify; intros 7; cases H3; +cases H (_); cases (H8 y); apply H9; cases (H8 p); +lapply (H12 H1) as H13; apply (le_le_eq); +[1: apply (le_transitive ???? H4); apply (Le≪ ? H13); assumption; +|2: apply (le_transitive ????? H5); apply (Le≫ (snd p) H13); assumption;] +qed. + +interpretation "Ordered uniform space N" 'nat = nat_ordered_uniform_space. diff --git a/helm/software/matita/contribs/dama/dama/models/nat_uniform.ma b/helm/software/matita/contribs/dama/dama/models/nat_uniform.ma new file mode 100644 index 000000000..cffccb59e --- /dev/null +++ b/helm/software/matita/contribs/dama/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" 'nat = nat_uniform_space. \ No newline at end of file diff --git a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma deleted file mode 100644 index d1c90dcd6..000000000 --- a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma +++ /dev/null @@ -1,238 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "nat/le_arith.ma". -include "nat_ordered_set.ma". -include "bishop_set_rewrite.ma". -include "uniform.ma". - -definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space. -intro C; apply (mk_uniform_space C); -[1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n)); -|2: intros 4 (U H x Hx); simplify in Hx; - cases H (_ H1); cases (H1 x); apply H2; apply Hx; -|3: intros; cases H (_ PU); cases H1 (_ PV); - exists[apply (λx.U x ∧ V x)] split; - [1: exists[apply something] intro; cases (PU n); cases (PV n); - split; intros; try split;[apply H2;|apply H4] try assumption; - apply H3; cases H6; assumption; - |2: simplify; intros; assumption;] -|4: intros; cases H (_ PU); exists [apply U] split; - [1: exists [apply something] intro n; cases (PU n); - split; intros; try split;[apply H1;|apply H2] assumption; - |2: intros 2 (x Hx); cases Hx; cases H1; clear H1; - cases (PU 〈(fst x),x1〉); lapply (H4 H2) as H5; simplify in H5; - cases (PU 〈x1,(snd x)〉); lapply (H7 H3) as H8; simplify in H8; - generalize in match H5; generalize in match H8; - generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8; - cases x; simplify; intros; cases H1; clear H1; apply H4; - apply (eq_trans ???? H3 H2);] -|5: intros; cases H (_ H1); split; cases x; - [2: cases (H1 〈b,b1〉); intro; apply H2; cases (H1 〈b1,b〉); - lapply (H6 H4) as H7; apply eq_sym; apply H7; - |1: cases (H1 〈b1,b〉); intro; apply H2; cases (H1 〈b,b1〉); - lapply (H6 H4) as H7; apply eq_sym; apply H7;]] -qed. - - -notation "\naturals" non associative with precedence 99 for @{'nat}. - -interpretation "naturals" 'nat = nat. -interpretation "Ordered set N" 'nat = nat_ordered_set. - -inductive cmp_cases (n,m:nat) : CProp ≝ - | cmp_lt : n < m → cmp_cases n m - | cmp_eq : n = m → cmp_cases n m - | cmp_gt : m < n → cmp_cases n m. - -lemma cmp_nat: ∀n,m.cmp_cases n m. -intros; -simplify; intros; generalize in match (nat_compare_to_Prop n m); -cases (nat_compare n m); intros; -[constructor 1|constructor 2|constructor 3] -assumption; -qed. - -lemma trans_le_lt_lt: - ∀n,m,o:nat.n≤m→m (?:s = O); - [2: cases Hs; lapply (os_le_to_nat_le ?? H1); - apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin). - |1: intros; lapply (os_le_to_nat_le (fst (a O)) O (H2 O)); - lapply (le_n_O_to_eq ? Hletin); assumption;] - |2: right; cases Hs; rewrite > (sym_plus s O); split; [apply le_S_S; apply le_O_n]; - apply (trans_le ??? (os_le_to_nat_le ?? H1)); - apply le_plus_n_r;] -|2,3: clear H6; - generalize in match H5; clear H5; cases (aux n1); intros; - change in match (a 〈w,H5〉) in H6 ⊢ % with (a w); - cases H5; clear H5; cases H7; clear H7; - [1: left; - split; - [ apply (le_S ?? H5) - | assumption] - |3: elimType False; - rewrite < H8 in H6; - apply (not_le_Sn_n ? H6) - |*: cut (u ≤ S n1 ∨ S n1 < u); - [2,4: cases (cmp_nat u (S n1)); - [1,4: left; apply lt_to_le; assumption - |2,5: rewrite > H7; left; apply le_n - |3,6: right; assumption ] - |*: cases Hcut; clear Hcut - [1,3: left; split; [1,3: assumption |2: symmetry; assumption] - cut (u = S n1); [2: apply le_to_le_to_eq; assumption ] - clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut; - cut (s = S (fst (a w))) - [2: apply le_to_le_to_eq; - [2:assumption - | change in H8 with (s + n1 ≤ S (n1 + fst (a w))); - rewrite > plus_n_Sm in H8; - rewrite > sym_plus in H8; - apply le_plus_to_le [2: apply H8]] - | cases (H3 (a w) H6); - change with (s = fst (a w1)); - change in H4 with (fst (a w) < fst (a w1)); - apply le_to_le_to_eq; - [ rewrite > Hcut; - assumption - | apply (os_le_to_nat_le (fst (a w1)) s (H2 w1));]] - |*: right; split; - [1,3: assumption - |2: rewrite > sym_plus in ⊢ (? ? %); - rewrite < H6; - apply le_plus_r; - assumption - | cases (H3 (a w) H6); - change with (s + S n1 ≤ u + fst (a w1)); - rewrite < plus_n_Sm; - apply (trans_le ? (S (u + fst (a w)))); [ apply le_S_S; assumption] - rewrite > plus_n_Sm; - apply le_plus; [ apply le_n ] - apply H9]]]]] -clearbody m; unfold spec in m; clear spec; -letin find ≝ ( - let rec find i u on u : nat ≝ - match u with - [ O ⇒ (m i:nat) - | S w ⇒ match eqb (fst (a (m i))) s with - [ true ⇒ (m i:nat) - | false ⇒ find (S i) w]] - in find - : - ∀i,bound.∃j.i + bound = u → s = fst (a j)); -[1: cases (find (S n) n2); intro; change with (s = fst (a w)); - apply H6; rewrite < H7; simplify; apply plus_n_Sm; -|2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity -|3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1; - cases (m u); cases H4; clear H4; cases H5; clear H5; [assumption] - cases (not_le_Sn_n ? H4) -] -clearbody find; cases (find O u); -exists [apply w]; intros; change with (s = fst (a j)); -rewrite > (H4 ?); [2: reflexivity] -apply le_to_le_to_eq; - [ apply os_le_to_nat_le; - apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5)); - | apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);] - rewrite < (H4 ?); [2: reflexivity] apply le_n;] -qed. - -definition nat_uniform_space: uniform_space. -apply (discrete_uniform_space_of_bishop_set ℕ); -qed. - -interpretation "Uniform space N" 'nat = nat_uniform_space. - -include "ordered_uniform.ma". - -definition nat_ordered_uniform_space:ordered_uniform_space. -apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ))); -simplify; intros 7; cases H3; cases H4; cases H5; clear H5 H4; -cases H (_); cases (H4 y); apply H5; clear H5 H10; cases (H4 p); -lapply (H10 H1) as H11; clear H10 H5; apply (le_le_eq); -[1: apply (le_transitive ???? H6); apply (Le≪ ? H11); assumption; -|2: apply (le_transitive ????? H7); apply (Le≫ (snd p) H11); assumption;] -qed. - -interpretation "Uniform space N" 'nat = nat_ordered_uniform_space. - -lemma nat_us_is_oc: ∀l,u:ℕ.order_continuity {[l,u]}. -intros 4; split; intros 3; cases H; cases H3; clear H3 H; -cases (H5 (a i)); -cases (H10 (sig_in ?? x1 H2)); - -exists [1,3:apply x1] -intros; apply H6; - diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma index d625d391d..23865418c 100644 --- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma +++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma @@ -49,6 +49,9 @@ apply (mk_ordered_set ? nat_excess); |2: apply nat_excess_cotransitive] qed. +notation "\naturals" non associative with precedence 90 for @{'nat}. +interpretation "ordered set N" 'nat = nat_ordered_set. + alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)". lemma os_le_to_nat_le: ∀a,b:nat_ordered_set.a ≤ b → le a b.