Finished!

[helm.git] / helm / software / matita / nlibrary / topology / igft3.ma

diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma
index 40378c07bed9c904164a78b631a1cca9fc63ebcb..3abe4af70c4de56aa70c988362f759ba3fd2185d 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft3.ma
+++ b/helm/software/matita/nlibrary/topology/igft3.ma
@@ -11,18 +11,16 @@
 (*        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.
@@ -39,22 +37,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;
+  | #a; #i; #IH; #H; @2 [ napply i ] #y; *; #j; #E; nrewrite > E; ncases j; #x; #K;
     napply H; nnormalize; nassumption.
 nqed.
-*)
+
 ndefinition ncoverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
 
 interpretation "ncoverage cover" 'coverage U = (ncoverage ? U).
@@ -134,8 +132,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.
@@ -192,10 +188,13 @@ nlet rec cover_rect
 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 O ]]
 **)
 
 ntheorem psym_plus: ∀n,m. n + m = m + n.
@@ -219,7 +218,7 @@ 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) O) ]
 nqed.
 
 ntheorem skipfact_base_dec:
@@ -232,11 +231,15 @@ 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 ]##]
+  | #m; nelim m; nnormalize
+     [ #H; @2; nnormalize
+       [ //
+       | #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 …); //
+        ##| /2/ ]
 nqed.
 
 ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.
@@ -244,8 +247,11 @@ 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)]