nat model ported to the dualized version, but not itself dualized dedekind-sig-compl...

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 27bb10f5a858a971721740b297c77bd5f879998e..ff063e29a0adaaeed17bb1f6d9ad0404970a082b 100644 (file)
--- 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 01890a416346c9afa546d5c9d7020fa4569f1234..76461f3f46222f911f4a366a90d8360cfd9ca426 100644 (file)
--- 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 5cf875f80a1455fb3cc4aebac6838a3d5e195b83..9681b4d93618b6fc4ef7a66dd21796b2fe5d0b3e 100644 (file)
--- 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 b8e23cc38beaf9f6a3e2f936fc5d806676582476..7949ba2d28714d077a1f5976b58af8b73f351276 100644 (file)
--- 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 17fef4165e4637d680c2c50d01736a3c72f39dae..82eedb35a39bb883e8682793b0b814614da1c41d 100644 (file)
--- 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.