fixed many scripts that broke for various reasons

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 685d6248059afb3e162ae4ec00ea1304f05318af..eac55537ea20e73c9d13df0dde34bf174c971e87 100644 (file)
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -41,8 +41,8 @@ nrecord magma_morphism_type (A,B: magma_type) : Type[0] ≝
 
 nrecord magma_morphism (A) (B) (Ma: magma A) (Mb: magma B) : Type[0] ≝
  { mmmcarr:> magma_morphism_type A B;
-   mmclosed: ∀x:A. x ∈ mcarr ? Ma → mmmcarr x ∈ mcarr ? Mb
- }.
+   mmclosed: ∀x:A. x ∈ mcarr ? Ma → (fun1 ?? mmmcarr x) ∈ mcarr ? Mb
+ }. (* XXX bug nelle coercions, fun1 non inserita *) 
 
 (*
 ndefinition mm_image:

diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma
index 60de71dbd7a2eb6d5fd69a6851603f2bb72dc060..6a74c20540afe66b8409f37f1db51ba6a67273eb 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -231,27 +231,25 @@ nlemma ftcoleqleft:
  #A; #F; #a; #H; ncases H; /2/.
 nqed.
 
-alias symbol "I" (instance 7) = "I".
-alias symbol "I" (instance 18) = "I".
-alias symbol "I" (instance 18) = "I".
-alias symbol "I" (instance 18) = "I".
+(* XXX: disambiguation crazy *)
+alias id "I" = "cic:/matita/ng/topology/igft/I.fix(0,0,2)".
 nlet corec ftfish_coind
  (A: Ax_pro) (F: Ω^A) (P: A → CProp[0])
- (Hcorefl: ∀a. P a → a ∈ F)
- (Hcoleqleft: ∀a. P a → ∀b. a ≤ b → P b)
- (Hcoleqinfinity: ∀a. P a → ∀b. a ≤ b → ∀i:𝐈 b. ∃x. x ∈ 𝐂 b i ↓ (singleton … a) ∧ P x)
+ (Hcorefl: ∀a:A. P a → a ∈ F)
+ (Hcoleqleft: ∀a:A. P a → ∀b:A. pre_r ? (Aleq A) a (*≤*) b → P b)
+ (Hcoleqinfinity: ∀a:A. P a → ∀b:A. pre_r ? (Aleq A) a (*≤*) b → ∀i:I A b. ∃x:A. x ∈ C A b i ↓ {(a)} ∧ P x)
 : ∀a:A. P a → a ⋉ F ≝ ?.
  #a; #H; @
   [ /2/
-  | #b; #H; napply (ftfish_coind … Hcorefl Hcoleqleft Hcoleqinfinity); /2/
+  | #b; #H; napply (ftfish_coind ??? Hcorefl Hcoleqleft Hcoleqinfinity); /2/
   | #b; #H1; #i; ncases (Hcoleqinfinity a H ? H1 i); #x; *; #H2; #H3;
-    @ x; @; //; napply (ftfish_coind … Hcorefl Hcoleqleft Hcoleqinfinity); //]
+    @ x; @; //; napply (ftfish_coind ??? Hcorefl Hcoleqleft Hcoleqinfinity); //]
 nqed.
 
-(*CSC: non serve manco questo (vedi sotto) *)
+(*CSC: non serve manco questo (vedi sotto) 
 nlemma auto_hint3: ∀A. S__o__AAx A = S (AAx A).
  #A; //.
-nqed.
+nqed.*)
 
 alias symbol "I" (instance 6) = "I".
 ntheorem ftcoinfinity: ∀A: Ax_pro. ∀F: Ω^A. ∀a. a ⋉ F → (∀i: 𝐈 a. ∃b. b ∈ 𝐂 a i ∧ b ⋉ F).
@@ -277,9 +275,9 @@ ndefinition Q_to_R: Q → Rd.
   | @ [ @ (Qminus q 1) (Qplus q 1) | ncases daemon ]
 ##| #c; #d; #Hc; #Hd; @ [ @ (Qmin (fst … c) (fst … d)) (Qmax (snd … c) (snd … d)) | ncases daemon]
 ##| #a; #H; napply (ftfish_coind Rax ? (λa. fst … a < q ∧ q < snd … a)); /2/
-    [ /5/ | #b; *; #H1; #H2; #c; *; #H3; #H4; #i; ncases i
-      [ #w; nnormalize;
-    ##| nnormalize;
-  ]
+    [ ncases daemon; ##| #b; *; #H1; #H2; #c; *; #H3; #H4; #i; ncases i
+      [ #w; nnormalize; ncases daemon;
+    ##| nnormalize; ncases daemon;
+##]
 nqed.
 

diff --git a/helm/software/matita/nlibrary/arithmetics/Z.ma b/helm/software/matita/nlibrary/arithmetics/Z.ma
index 9045a6d8ad5ce4c10731570c92b4b4a535524d84..1904f684932789508909c270f88747a801f8b1b5 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/Z.ma
+++ b/helm/software/matita/nlibrary/arithmetics/Z.ma
@@ -346,6 +346,8 @@ ncut
 ##|#Hcut;napply Hcut;napply eqZb_to_Prop]
 nqed.
 
+include "arithmetics/compare.ma".
+
 ndefinition Z_compare : Z → Z → compare ≝
 λx,y:Z.
   match x with
@@ -508,7 +510,7 @@ ntheorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).
    ##[//
    ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
    ##|//]
-##|ncases y;//
+##|ncases y;/2/;
 ##|ncases y
    ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
       nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index d4ba1135e241626f551b5bca4b55c0a43f7d01e5..9c420f9ec492e532cebae13dcd72fe76b5087c84 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -53,9 +53,10 @@ ntheorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
 ndefinition not_zero: nat → Prop ≝
  λn: nat. match n with
   [ O ⇒ False | (S p) ⇒ True ].
-
+  
 ntheorem not_eq_O_S : ∀n:nat. O ≠ S n.
-#n; napply nmk; #eqOS; nchange with (not_zero O); nrewrite > eqOS; //.
+#n; napply nmk; #eqOS; nchange with (not_zero O); 
+nrewrite > eqOS; //.
 nqed.
 
 ntheorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
@@ -488,7 +489,7 @@ nelim n;
  ##[#q; #HleO; (* applica male *) 
     napply (le_n_O_elim ? HleO);
     napply H; #p; #ltpO;
-    napply False_ind; /2/; (* 3 *)
+    napply (False_ind ??); /2/; (* 3 *)
  ##|#p; #Hind; #q; #HleS; 
     napply H; #a; #lta; napply Hind;
     napply le_S_S_to_le;/2/;

diff --git a/helm/software/matita/nlibrary/datatypes/list-theory.ma b/helm/software/matita/nlibrary/datatypes/list-theory.ma
index 14bab26e31558989a2fa8ef3075138d1bf4b8977..4957feed26ac57e4c219b740eab7dd85f79ff3d2 100644 (file)
--- a/helm/software/matita/nlibrary/datatypes/list-theory.ma
+++ b/helm/software/matita/nlibrary/datatypes/list-theory.ma
@@ -20,7 +20,7 @@ ntheorem nil_cons:
 #A;#l;#a; @; #H; ndestruct;
 nqed.
 
-ntheorem append_nil: ∀A:Type.∀l:list A.l @ □ = l.
+ntheorem append_nil: ∀A:Type.∀l:list A.l @ [ ] = l.
 #A;#l;nelim l;//;
 #a;#l1;#IH;nnormalize;//;
 nqed.

diff --git a/helm/software/matita/nlibrary/logic/cologic.ma b/helm/software/matita/nlibrary/logic/cologic.ma
index ca4921607b6b5d4d5ec1e232f63b3be1ca4a54de..8b9ed3c15d450c622d78eb42294f43a98d145922 100644 (file)
--- a/helm/software/matita/nlibrary/logic/cologic.ma
+++ b/helm/software/matita/nlibrary/logic/cologic.ma
@@ -95,7 +95,7 @@ ntheorem cand_true: ∀c1,c2. ceq c1 (certain true) → ceq (cand c1 c2) c2.
            ##[ nlapply (KK2 EE); #XX; nrewrite > (cand_truer …) in XX; #YY;
                @3;
                
-           ##[ nrewrite > (ccases (cand (maybe xx) (certain true)));
+           rewrite > (ccases (cand (maybe xx) (certain true)));
                nnormalize; @3; @2; 
 
  

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index b92fe9ab3011d9bcbcb75637b51c886c43de6d05..3eea5010166d4d61c5ff51e98646fd3c8ca94e36 100644 (file)
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -146,7 +146,7 @@ napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
         [##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; //
         | nassumption ]##]
 ##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E;
-    ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ Nat_ (s i1) → i2' ∈ Nat_ (s i1') → eq_rel (carr A) (eq A) (fi i1 i2) (fi i1' i2') → i1=i1' ∧ i2=i2');
+    ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ Nat_ (s i1) → i2' ∈ Nat_ (s i1') → eq_rel (carr A) (eq0 A) (fi i1 i2) (fi i1' i2') → i1=i1' ∧ i2=i2');
     ##[ #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
        nlapply(disjoint … P (f i1) (f i1') ???)
        [##2,3: napply f_closed; //
@@ -179,7 +179,7 @@ ndefinition partition_of_compatible_equivalence_relation:
   | napply Full_set
   | napply mk_unary_morphism1
      [ #a; napply mk_ext_powerclass
-        [ napply {x | R x a}
+        [ napply {x | rel ? R x a}
         | #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon]
    ##| #a; #a'; #H; napply conj; #x; nnormalize; #K [ nelim daemon | nelim daemon]##]
 ##| #x; #_; nnormalize; /3/

diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma
index d3dccb8ee07e66248e17e69f21536cc6fb3013fe..6a79dd2d808df2478f6a4ad25568e41e1eb68894 100644 (file)
--- a/helm/software/matita/nlibrary/topology/cantor.ma
+++ b/helm/software/matita/nlibrary/topology/cantor.ma
@@ -78,7 +78,7 @@ alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
 unification hint 0 ≔ ;
          x ≟ axs  
   (* -------------- *) ⊢
-         S x ≡ A. 
+         S (uax x) ≡ A. (* XXX: bug coercions/ disamb multipasso che ne fa 1 solo*) 
 
 ntheorem col2_4 :
   ∀A:uAx.∀a:uax A. a ◃ ∅ → ¬ a ∈ 𝐂 a one.
@@ -88,7 +88,8 @@ ntheorem col2_4 :
 ##]
 nqed.
 
-ndefinition Z : Ω^axs ≝ { x | x ◃ ∅ }.
+(* bug interpretazione non aggiunta per ∅ *)
+ndefinition Z : Ω^axs ≝ { x | x ◃ (emptyset ?) }.
 
 ntheorem cover_monotone: ∀A:Ax.∀a:A.∀U,V.U ⊆ V → a ◃ U → a ◃ V.
 #A; #a; #U; #V; #HUV; #H; nelim H; /3/; 
@@ -126,7 +127,7 @@ alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
 unification hint 0 ≔ ;
          x ≟ caxs  
   (* -------------- *) ⊢
-         S x ≡ nat. 
+         S (uax x) ≡ nat. 
 
 naxiom h : nat → nat. 
 

diff --git a/helm/software/matita/nlibrary/topology/igft-setoid.ma b/helm/software/matita/nlibrary/topology/igft-setoid.ma
index a4d833cae0007f8f7d78f3a888107357c1274292..276fa54805a117c729289f4b3e79e49869b1c9ae 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft-setoid.ma
+++ b/helm/software/matita/nlibrary/topology/igft-setoid.ma
@@ -63,6 +63,7 @@ unification hint 0 ≔ A,B ;
            (* ----------------------------------- *) ⊢              
                   unary_morphism A B ≡ carr T. 
                 
+(*                
                 
 ndefinition TYPE : setoid1.
 @ setoid; @; 
@@ -111,7 +112,7 @@ interpretation "d" 'd a i j = (nd ? a i j).
 interpretation "new I" 'I a = (nI ? a).
 
 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
-(*
+
 nlemma elim_eq_TYPE : ∀A,B:setoid.∀P:CProp[1]. A=B → ((B ⇒ A) → P) → P.
 #A; #B; #P; *; #f; *; #g; #_; #IH; napply IH; napply g;
 nqed.
@@ -140,6 +141,7 @@ nlemma foo: ∀A:setoid.∀T:unary_morphism01 A TYPE.∀P:∀x:A.∀a:T x.CProp[
 ##[ @(f e);   
 *)
 
+(*
 ndefinition image_is_ext : ∀A:nAx.∀a:A.∀i:𝐈 a.𝛀^A.
 #A; #a; #i; @ (image … i); #x; #y; #H; @;
 ##[ *; #d; #Ex; @ d; napply (.= H^-1); nassumption;
@@ -566,4 +568,4 @@ D*)
 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf 
 
 D*)
-*)
+*)*)
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma
index 3c7489ba3aa384d98f80c007253e8c8c131dfe47..4ab768fce53332f0d635b2e559b87c52c74e41d4 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft3.ma
+++ b/helm/software/matita/nlibrary/topology/igft3.ma
@@ -214,7 +214,7 @@ ntheorem skipfact_partial:
  ∀n: uuax skipfact_dom. two * n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O).
  #n; nelim n; /2/;
  #m; nelim m; nnormalize
-     [ #H; @2; nnormalize; //;
+     [ #H; @2; nnormalize; ##[//;##] (* XXX: bug auto *)
        #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; //
    ##| #p; #H1; #H2; @2; nnormalize; //;
        #y; *; #a; #E; nrewrite > E; ncases a; nnormalize;

diff --git a/helm/software/matita/nlibrary/topology/igft4.ma b/helm/software/matita/nlibrary/topology/igft4.ma
index 9dbbbcf6c3e23060b0bfc1980ce4f90bef3d3ecf..f78b46e7945ddea896b16a00fbac5c48cb4edec2 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft4.ma
+++ b/helm/software/matita/nlibrary/topology/igft4.ma
@@ -214,7 +214,7 @@ ntheorem skipfact_partial:
   [ @2; nnormalize; //; #y; *; #a; ncases a
   |
  #m; nelim m; nnormalize
-     [ #H; @2; nnormalize; //;
+     [ #H; @2; nnormalize; ##[//;##] (* XXX: bug auto *)
        #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; //
    ##| #p; #H1; #H2; @2; nnormalize; //;
        #y; *; #a; #E; nrewrite > E; ncases a; nnormalize;