X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft2.ma;h=90a644ce92c65b8e2ad81ec9ebcc66c130a253be;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=dc78b768079ef614c53908f3b3639d815c5fbcfd;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft2.ma b/helm/software/matita/nlibrary/topology/igft2.ma
index dc78b7680..90a644ce9 100644
--- a/helm/software/matita/nlibrary/topology/igft2.ma
+++ b/helm/software/matita/nlibrary/topology/igft2.ma
@@ -12,18 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "arithmetics/nat.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; /2/;
+nnormalize; nauto;
 nqed.
 
 alias symbol "covers" = "covers set".
@@ -33,7 +25,9 @@ nlemma cover_ind':
  ∀A:Ax.∀U,P:Ω^A.
    (U ⊆ P) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → 𝐂 a j ⊆ P → a ∈ P) →
     ◃ U ⊆ P.
- #A; #U; #P; #refl; #infty; #a; #H; nelim H; /3/. 
+ #A; #U; #P; #refl; #infty; #a; #H; nelim H
+  [ nauto | (*nauto depth=4;*) #b; #j; #K1; #K2; 
+            napply infty; nauto; ##] 
 nqed.
 
 alias symbol "covers" (instance 1) = "covers".
@@ -76,7 +70,7 @@ ncoercion uuax : ∀u:uuAx. Ax ≝ uuax on _u : uuAx to Ax.
 
 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; //;
+ #A; #a; #x; #p; ncases p; nauto;
 nqed.
 
 nlemma eq_rect_Type0_r:
@@ -106,68 +100,22 @@ nlet rec cover_rect
 ≝ ?.
  nlapply (decide_mem_ok … memdec b); nlapply (decide_mem_ko … memdec b);
  ncases (decide_mem … memdec b)
-  [ #_; #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; // ]
+  [ #_; #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 ]
     ##| #a; #i; #K; #E2; nrewrite < E2 in i; nnormalize; nrewrite > E; nnormalize;
-        //]
+        nauto]
   ##| #a; #E;
       ncut (a ◃ U)
-       [ nlapply E; nlapply (H ?) [//] ncases p
+       [ nlapply E; nlapply (H ?) [nauto] ncases p
           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
         ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
-            nrewrite > E2; nnormalize; #_; //]##]
+            nrewrite > E2; nnormalize; #_; nauto]##]
       #Hcut; 
       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
       napply (H2 one); #y; #E2; nrewrite > E2 
-      (* [##2: napply cover_rect] //; *)
+      (* [##2: napply cover_rect] nauto depth=1; *)
        [ napply Hcut
-     ##| napply (cover_rect A U memdec P refl infty a); // ]##]
-nqed.
-
-(********* Esempio:
-   let rec skipfact n =
-     match n with
-      [ O ⇒ 1
-      | S m ⇒ S m * skipfact (pred m) ]
-**)
-
-ntheorem psym_plus: ∀n,m. n + m = m + n.//.
-nqed.
-
-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)) ]
-nqed.
-
-ntheorem skipfact_base_dec:
- memdec (uuax skipfact_dom) (mk_powerclass ? (λx: uuax skipfact_dom. x=O)).
- nnormalize; @ (λx. match x with [ O ⇒ true | S _ ⇒ false ]); #n; nelim n;
-  nnormalize; //; #X; ndestruct; #Y; #Z; ndestruct; #W; ndestruct.
-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))));
-       nnormalize; nrewrite < (plus_n_Sm …); nnormalize;
-       #E; nrewrite > E; napply H ]##]
-nqed.
-
-ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.
- #n; #D; napply (cover_rect … skipfact_base_dec … n D)
-  [ #a; #_; napply natone
-  | #a; ncases a
-    [ nnormalize; #i; nelim i
-    | #m; #i; nnormalize in i; #d; #H;
-      napply (S m * H (pred m) …); //]
-nqed.
-
-nlemma test: skipfact four ? = eight. ##[##2: napply (skipfact_partial two)] //.
+     ##| napply (cover_rect A U memdec P refl infty a); nauto ]##]
 nqed.
\ No newline at end of file