From: Enrico Tassi Date: Wed, 19 Nov 2008 12:19:26 +0000 (+0000) Subject: renaming X-Git-Tag: make_still_working~4534 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a6f88a0acfcb5c5284b7b3781e313cc0f76bb76d;p=helm.git renaming --- diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index 1d54328f5..7e0d8968e 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,26 +1,27 @@ 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 -property_sigma.ma ordered_uniform.ma russell_support.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 -ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma -models/q_bars.ma logic/cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma russell_support.ma -models/list_support.ma list/list.ma logic/cprop_connectives.ma nat/le_arith.ma nat/minus.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 -lebesgue.ma property_exhaustivity.ma sandwich.ma -models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.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_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma -uniform.ma supremum.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 diff --git a/helm/software/matita/contribs/dama/dama/depends.png b/helm/software/matita/contribs/dama/dama/depends.png index 8cbedcae0..1c10c2366 100644 Binary files a/helm/software/matita/contribs/dama/dama/depends.png and b/helm/software/matita/contribs/dama/dama/depends.png differ diff --git a/helm/software/matita/contribs/dama/dama/models/increasing_supremum_stabilizes.ma b/helm/software/matita/contribs/dama/dama/models/increasing_supremum_stabilizes.ma new file mode 100644 index 000000000..9a43d186d --- /dev/null +++ b/helm/software/matita/contribs/dama/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/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma deleted file mode 100644 index 9a43d186d..000000000 --- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma +++ /dev/null @@ -1,138 +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 "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/contribs/dama/dama/models/nat_lebesgue.ma b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma index fd1d8dbcb..d5e65215e 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma @@ -1,4 +1,4 @@ -(**************************************************************************) + (**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) 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 index 0b4c92e3e..5f00dc338 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -include "models/nat_dedekind_sigma_complete.ma". +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 (nat_dedekind_sigma_complete s a H1 ? H2); +[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); @@ -26,7 +26,7 @@ intros 3; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H; 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 (nat_dedekind_sigma_complete_r s a H1 ? H2); +|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);