X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft3.ma;h=4ab768fce53332f0d635b2e559b87c52c74e41d4;hb=1d7773584ddd6463b0941026f114b0173e3b6b72;hp=40378c07bed9c904164a78b631a1cca9fc63ebcb;hpb=4a8f4870edcc4fee7cf51744d4a731be84365ea7;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma
index 40378c07b..4ab768fce 100644
--- a/helm/software/matita/nlibrary/topology/igft3.ma
+++ b/helm/software/matita/nlibrary/topology/igft3.ma
@@ -11,23 +11,19 @@
 (*        v         GNU General Public License Version 2                  *)
 (*                                                                        *)
 (**************************************************************************)
-(*
+
 include "arithmetics/nat.ma".
-*)
 include "datatypes/bool.ma".
 
-(*
 ndefinition two ≝ S (S O).
 ndefinition natone ≝ S O.
 ndefinition four ≝ two * two.
 ndefinition eight ≝ two * four.
 ndefinition natS ≝ S.
-*)
+
 include "topology/igft.ma".
 
-nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V.
-nnormalize; nauto;
-nqed.
+nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V./2/.nqed.
 
 ninductive Sigma (A: Type[0]) (P: A → CProp[0]) : Type[0] ≝
  mk_Sigma: ∀a:A. P a → Sigma A P.
@@ -39,22 +35,22 @@ ninductive ncover (A : nAx) (U : Ω^A) : A → CProp[0] ≝
 
 interpretation "ncovers" 'covers a U = (ncover ? U a).
 
-(*XXX
 ntheorem ncover_cover_ok: ∀A:nAx.∀U.∀a:A. a ◃ U → cover (Ax_of_nAx A) U a.
  #A; #U; #a; #H; nelim H
   [ #n; #H1; @1; nassumption
   | #a; #i; #IH; #H; @2 [ napply i ]
     nnormalize; #y; *; #j; #E; nrewrite > E;
-    napply H ]
+    napply H;
+    /2/ ]
 nqed.
 
 ntheorem cover_ncover_ok: ∀A:Ax.∀U.∀a:A. a ◃ U → ncover (nAx_of_Ax A) U a.
  #A; #U; #a; #H; nelim H
   [ #n; #H1; @1; nassumption
-  | #a; #i; #IH; #H; @2 [ napply i ] #j; ncases j; #x; #K;
-    napply H; nnormalize; nassumption.
+  | #a; #i; #IH; #H; @2 [ napply i ] #y; *; #j; #E; nrewrite > E; ncases j; #x; #K;
+    napply H; nnormalize; //.
 nqed.
-*)
+
 ndefinition ncoverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
 
 interpretation "ncoverage cover" 'coverage U = (ncoverage ? U).
@@ -67,8 +63,7 @@ nlemma ncover_ind':
    (U ⊆ P) → (∀a:A.∀i:𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j. 𝐝 a i j ∈ P) → a ∈ P) →
     ◃ U ⊆ P.
  #A; #U; #P; #refl; #infty; #a; #H; nelim H
-  [ nauto | (*nauto depth=4;*) #b; #j; #K1; #K2; 
-            napply infty; nauto; ##] 
+  [ // | #b; #j; #K1; #K2; napply infty; //; ##] 
 nqed.
 
 alias symbol "covers" (instance 3) = "ncovers".
@@ -118,12 +113,12 @@ ncoercion uuax : ∀u:uuAx. nAx ≝ uuax on _u : uuAx to nAx.
 
 nlemma eq_rect_Type0_r':
  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
- #A; #a; #x; #p; ncases p; nauto;
+ #A; #a; #x; #p; ncases p; //;
 nqed.
 
 nlemma eq_rect_Type0_r:
  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); //.
 nqed.
 
 nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
@@ -134,8 +129,6 @@ nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
 
 (*********** end from Cantor ********)
 
-naxiom daemon: False.
-
 nlemma csc_sym_eq: ∀A,x,y. eq A x y → eq A y x.
  #A; #x; #y; #H; ncases H; @1.
 nqed.
@@ -154,15 +147,15 @@ nlet rec cover_rect
 ≝ ?.
  nlapply (decide_mem_ok … memdec b); nlapply (decide_mem_ko … memdec b);
  ncases (decide_mem … memdec b)
-  [ #_; #H; napply refl; nauto
-  | #H; #_; ncut (uuC … b=uuC … b) [nauto] ncases (uuC … b) in ⊢ (???% → ?)
-    [ #E; napply False_rect_Type0; ncut (b=b) [nauto] ncases p in ⊢ (???% → ?)
-      [ #a; #K; #E2; napply H [ nauto | nrewrite > E2; nauto ]
+  [ #_; #H; napply refl; /2/
+  | #H; #_; ncut (uuC … b=uuC … b) [//] ncases (uuC … b) in ⊢ (???% → ?)
+    [ #E; napply False_rect_Type0; ncut (b=b); //; ncases p in ⊢ (???% → ?)
+      [ #a; #K; #E2; napply H; //; nrewrite > E2; //
     ##| #a; #i; #K; #E2; nrewrite < E2 in i; nnormalize; nrewrite > E; nnormalize;
-        nauto]
+        //]
   ##| #a; #E;
       ncut (a ◃ U)
-       [ nlapply E; nlapply (H ?) [nauto] ncases p
+       [ nlapply E; nlapply (H ?) [//] ncases p
           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
             nrewrite > E2; nnormalize; /2/ ]##]
@@ -170,16 +163,16 @@ nlet rec cover_rect
       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
       napply (H2 one); #y
        [ napply Hcut
-     ##| napply (cover_rect A U memdec P refl infty a); nauto ]
+     ##| napply (cover_rect A U memdec P refl infty a); // ]
   ##| #a; #a1; #E;
       ncut (a ◃ U)
-       [ nlapply E; nlapply (H ?) [nauto] ncases p
+       [ nlapply E; nlapply (H ?) [//] ncases p
           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
             nrewrite > E2; nnormalize; #_; @1 (true); /2/ ]##]
       #Hcut;
       ncut (a1 ◃ U)
-       [ nlapply E; nlapply (H ?) [nauto] ncases p
+       [ nlapply E; nlapply (H ?) [//] ncases p
           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
             nrewrite > E2; nnormalize; #_; @1 (false); /2/ ]##]
@@ -187,39 +180,28 @@ nlet rec cover_rect
       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
       napply (H2 one); #y; ncases y; nnormalize
        [##1,2: nassumption
-       | napply (cover_rect A U memdec P refl infty a); nauto
-       | napply (cover_rect A U memdec P refl infty a1); nauto]
+       | napply (cover_rect A U memdec P refl infty a); //
+       | napply (cover_rect A U memdec P refl infty a1); //]
 nqed.
 
 (********* Esempio:
-   let rec skipfact n =
+   let rec skip n =
      match n with
       [ O ⇒ 1
-      | S m ⇒ S m * skipfact (pred m) ]
+      | S m ⇒
+         match m with
+          [ O ⇒ skipfact O
+          | S _ ⇒ S m * skipfact (pred m) * skipfact (pred m) ]]
 **)
 
-ntheorem psym_plus: ∀n,m. n + m = m + n.
- #n; nelim n
-  [ #m; nelim m; //; #n0; #H;
-    nchange with (natS n0 = natS (n0 + O));
-    nrewrite < H; //
-  | #n0; #H; #m; nchange with (S (n0 + m) = m + S n0);
-    nrewrite > (H …);
-    nelim m; //;
-    #n1; #E; nrewrite > E; //]
+ntheorem psym_plus: ∀n,m. n + m = m + n.//.
 nqed.
 
-nlemma easy1: ∀n:nat. two * (S n) = two + two * n.
- #n; nelim n;//;
- #n0; #H; nnormalize;
- nrewrite > (psym_plus ??);
- nrewrite > H; nnormalize;
- nrewrite > (psym_plus ??);
- //.
+nlemma easy1: ∀n:nat. two * (S n) = two + two * n.//.
 nqed.
 
 ndefinition skipfact_dom: uuAx.
- @ nat; #n; ncases n [ napply None | #m; napply (Some … (pred m)) ]
+ @ nat; #n; ncases n [ napply None | #m; ncases m [ napply (Some … O) | #_; napply (Twice … (pred m) (pred m)) ]
 nqed.
 
 ntheorem skipfact_base_dec:
@@ -230,13 +212,13 @@ nqed.
 
 ntheorem skipfact_partial:
  ∀n: uuax skipfact_dom. two * n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O).
- #n; nelim n
-  [ @1; nnormalize; @1
-  | #m; #H; @2
-     [ nnormalize; @1
-     | nnormalize; #y; nchange in ⊢ (% → ?) with (y = pred (pred (two * (natone + m))));
-       nrewrite > (easy1 …); nchange in ⊢ (% → ?) with (y = two * m);
-       #E; nrewrite > E; nassumption ]##]
+ #n; nelim n; /2/;
+ #m; nelim m; 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;
+       nrewrite < (plus_n_Sm …); // ]
 nqed.
 
 ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.
@@ -244,10 +226,12 @@ ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=
   [ #a; #_; napply natone
   | #a; ncases a
     [ nnormalize; #i; nelim i
-    | #m; #i; nnormalize in i; #d; #H;
-      napply (S m * H (pred m) …); //]
+    | #m; ncases m
+       [ nnormalize; #_; #_; #H; napply H; @1
+       | #p; #i; nnormalize in i; #K;
+         #H; nnormalize in H;
+         napply (S m * H true * H false) ]
 nqed.
 
-nlemma test: skipfact four ? = eight. ##[##2: napply (skipfact_partial two)]
- nnormalize; //.
+nlemma test: skipfact four ? = four * two * two. ##[##2: napply (skipfact_partial two)]//.
 nqed.
\ No newline at end of file