From 7deb4b1f322850b8ff03d5626f7828736d074ec8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 20 Oct 2008 20:12:12 +0000 Subject: [PATCH] nat model ported to the dualized version, but not itself dualized dedekind-sig-compl missing --- .../contribs/dama/dama/bishop_set_rewrite.ma | 14 +++++----- .../dama/dama/models/discrete_uniformity.ma | 2 +- .../models/nat_dedekind_sigma_complete.ma | 27 ++++++++++++++----- .../dama/dama/models/nat_order_continuous.ma | 4 +-- .../dama/dama/models/nat_ordered_uniform.ma | 4 +-- 5 files changed, 32 insertions(+), 19 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma index 27bb10f5a..ff063e29a 100644 --- a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma +++ b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma @@ -14,7 +14,7 @@ include "bishop_set.ma". -coercion cic:/matita/dama/bishop_set/eq_sym.con. +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. @@ -25,12 +25,12 @@ notation > "'Eq'≈" non associative with precedence 50 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); +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); +intros (E z y x Exy Lxz); apply (le_transitive ??? Lxz); intro Xyz; apply Exy; left; assumption; qed. @@ -55,12 +55,12 @@ 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 (hos_cotransitive ??? x Ayz); [2:assumption] +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 (hos_cotransitive ???x Azy); [assumption] +intros (A x z y Exy Azy); cases (exc_cotransitive ??x Azy); [assumption] cases (Exy); left; assumption; qed. @@ -69,7 +69,7 @@ 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; @@ -84,4 +84,4 @@ 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/contribs/dama/dama/models/discrete_uniformity.ma b/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma index 01890a416..76461f3f4 100644 --- a/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma +++ b/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma @@ -21,7 +21,7 @@ intro C; apply (mk_uniform_space C); alias symbol "pi2" = "pair pi2". alias symbol "pi1" = "pair pi1". alias symbol "and" = "logical and". - apply (∃d:unit.∀n:C square.(\fst n ≈ \snd n → P n) ∧ (P n → \fst n ≈ \snd n)); + 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); 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 index 5cf875f80..9681b4d93 100644 --- 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 @@ -17,16 +17,22 @@ include "supremum.ma". include "nat/le_arith.ma". include "russell_support.ma". +lemma hint1: + ∀l,u.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set l u)) + → sequence (hos_carr (os_l (segment_ordered_set nat_ordered_set l u))). +intros; assumption; +qed. + +coercion hint1 nocomposites. + alias symbol "pi1" = "exT \fst". -alias symbol "leq" = "natural 'less or equal to'". +alias symbol "N" = "ordered set N". 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; -alias symbol "plus" = "natural plus". -alias symbol "N" = "Uniform space N". -alias symbol "and" = "logical and". +alias symbol "N" = "Natural numbers". 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 ? ( @@ -109,14 +115,21 @@ 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)); + 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'". +lemma hint2: + ∀l,u.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set l u)) + → sequence (hos_carr (os_r (segment_ordered_set nat_ordered_set l u))). +intros; assumption; +qed. + +coercion hint2 nocomposites. + alias symbol "N" = "ordered set N". 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_order_continuous.ma b/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma index b8e23cc38..7949ba2d2 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 @@ -25,7 +25,7 @@ intros 4; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H; 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; + apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space)); |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); @@ -34,6 +34,6 @@ intros 4; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H; 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;] + apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space));] 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 index 17fef4165..82eedb35a 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma @@ -21,8 +21,8 @@ definition nat_ordered_uniform_space:ordered_uniform_space. 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;] +[1: apply (le_transitive ??? H4); apply (Le≪ ? H13); assumption; +|2: apply (le_transitive ???? H5); apply (Le≫ ? (eq_sym ??? H13)); assumption;] qed. interpretation "Ordered uniform space N" 'N = nat_ordered_uniform_space. -- 2.39.2