From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Jan 2010 16:12:43 +0000 (+0000)
Subject: Urrah!
X-Git-Tag: make_still_working~3123
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4a8f4870edcc4fee7cf51744d4a731be84365ea7;p=helm.git

Urrah!
---

diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma
index 52d07766e..40378c07b 100644
--- a/helm/software/matita/nlibrary/topology/igft3.ma
+++ b/helm/software/matita/nlibrary/topology/igft3.ma
@@ -29,13 +29,17 @@ nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V.
 nnormalize; nauto;
 nqed.
 
+ninductive Sigma (A: Type[0]) (P: A → CProp[0]) : Type[0] ≝
+ mk_Sigma: ∀a:A. P a → Sigma A P.
+
 (*<< To be moved in igft.ma *)
 ninductive ncover (A : nAx) (U : Ω^A) : A → CProp[0] ≝
 | ncreflexivity : ∀a. a ∈ U → ncover A U a
-| ncinfinity    : ∀a. ∀i. (∀j. ncover A U (𝐝 a i j)) → ncover A U a.
+| ncinfinity    : ∀a. ∀i. (∀y.Sigma ? (λj.y = 𝐝 a i j) → ncover A U y) → ncover A U a.
 
 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
@@ -50,13 +54,14 @@ ntheorem cover_ncover_ok: ∀A:Ax.∀U.∀a:A. a ◃ U → ncover (nAx_of_Ax A)
   | #a; #i; #IH; #H; @2 [ napply i ] #j; 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).
 
 (*>> To be moved in igft.ma *)
 
+(*XXX
 nlemma ncover_ind':
  ∀A:nAx.∀U,P:Ω^A.
    (U ⊆ P) → (∀a:A.∀i:𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j. 𝐝 a i j ∈ P) → a ∈ P) →
@@ -73,6 +78,7 @@ nlemma cover_ind'':
    ∀b. b ◃ U → P b.
  #A; #U; #P; nletin V ≝ {x | P x}; napply (ncover_ind' … V).
 nqed.
+*)
 
 (*********** from Cantor **********)
 ninductive eq1 (A : Type[0]) : Type[0] → CProp[0] ≝
@@ -158,39 +164,31 @@ nlet rec cover_rect
       ncut (a ◃ U)
        [ nlapply E; nlapply (H ?) [nauto] ncases p
           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
-        ##| #x; #i; #Hx; #K1; #E2; napply Hx;
-            nlapply Hx; nlapply i; nnormalize;
-            napply (csc_eq_rect_CProp0_r' ??? E2 ??); nnormalize;
-            #_; #X; napply X; ncases daemon (*@1*)
-            (* /2/*) ]##]
+        ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
+            nrewrite > E2; nnormalize; /2/ ]##]
       #Hcut;
       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
       napply (H2 one); #y
        [ napply Hcut
-     ##| #j; #W; nrewrite > W; napply (cover_rect A U memdec P refl infty a); nauto ]
-  ##| (* #a; #a1; #E;
+     ##| napply (cover_rect A U memdec P refl infty a); nauto ]
+  ##| #a; #a1; #E;
       ncut (a ◃ U)
        [ nlapply E; nlapply (H ?) [nauto] ncases p
           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
-        ##| #x; #i; #Hx; #K1; #E2; nnormalize in Hx;
-            nrewrite > E2 in Hx; nnormalize; #Hx;
-            napply (Hx true)]##]
+        ##| #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
           [ #x; #Hx; #K1; #_; ncases (K1 Hx)
-        ##| #x; #i; #Hx; #K1; #E2; nnormalize in Hx;
-            nrewrite > E2 in Hx; nnormalize; #Hx;
-            napply (Hx false)]##]
+        ##| #x; #i; #Hx; #K1; #E2; napply Hx; ngeneralize in match i; nnormalize;
+            nrewrite > E2; nnormalize; #_; @1 (false); /2/ ]##]
       #Hcut1;
       nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
-      napply (H2 one); #b; ncases b; nnormalize
-       [ napply Hcut
-       | napply Hcut1
+      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]##]*)
-       
-   ncases daemon.
+       | napply (cover_rect A U memdec P refl infty a1); nauto]
 nqed.
 
 (********* Esempio: