From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Jan 2010 15:55:29 +0000 (+0000)
Subject: Extending to the nAx set.
X-Git-Tag: make_still_working~3124
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=634a86f552919afdb4e9cbb211c9a5371f86f45f;p=helm.git

Extending to the nAx set.
---

diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma
new file mode 100644
index 000000000..52d07766e
--- /dev/null
+++ b/helm/software/matita/nlibrary/topology/igft3.ma
@@ -0,0 +1,255 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        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.
+
+(*<< 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.
+
+interpretation "ncovers" 'covers a U = (ncover ? U a).
+
+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 ]
+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.
+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 *)
+
+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) →
+    ◃ U ⊆ P.
+ #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 3) = "ncovers".
+nlemma cover_ind'':
+ ∀A:nAx.∀U:Ω^A.∀P:A → CProp[0].
+  (∀a. a ∈ U → P a) → (∀a:A.∀i:𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j. P (𝐝 a i j)) → P a) →
+   ∀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] ≝
+| refl1 : eq1 A A.
+
+notation "hvbox( a break ∼ b)" non associative with precedence 40
+for @{ 'eqT $a $b }.
+
+interpretation "eq between types" 'eqT a b = (eq1 a b).
+
+ninductive unit : Type[0] ≝ one : unit.
+
+ninductive option (A: Type[0]) : Type[0] ≝
+   None: option A
+ | Some: A → option A
+ | Twice: A → A → option A.
+
+nrecord uuAx : Type[1] ≝ {
+  uuS : Type[0];
+  uuC : uuS → option uuS
+}.
+
+ndefinition uuax : uuAx → nAx.
+#A; @ (uuS A)
+  [ #a; ncases (uuC … a) [ napply False | #_; napply unit | #_; #_; napply unit]
+##| #a; ncases (uuC … a); nnormalize
+     [ #H; napply (False_rect_Type1 … H)
+     | #_; #_; napply unit
+     | #_; #_; #_; napply bool ]
+##| #a; ncases (uuC … a); nnormalize
+     [ #H; napply (False_rect_Type1 … H)
+     | #b; #_; #_; napply b
+     | #b1; #b2; #_; * [ napply b1 | napply b2]##]##]
+nqed.
+
+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;
+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.
+nqed.
+
+nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
+ { decide_mem:> A → bool;
+   decide_mem_ok: ∀x. decide_mem x = true → x ∈ U;
+   decide_mem_ko: ∀x. decide_mem x = false → ¬ (x ∈ U)
+ }.
+
+(*********** 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.
+
+nlemma csc_eq_rect_CProp0_r':
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. CProp[0]. P a → P x.
+ #A; #a; #x; #p; #P; #H;
+ napply (match csc_sym_eq ??? p return λa.λ_.P a with [ refl ⇒ H ]).
+nqed.
+ 
+nlet rec cover_rect
+ (A:uuAx) (U:Ω^(uuax A)) (memdec: memdec … U) (P:uuax A → Type[0])
+  (refl: ∀a:uuax A. a ∈ U → P a)
+  (infty: ∀a:uuax A.∀i: 𝐈 a.(∀j. 𝐝 a i j ◃ U) → (∀j.P (𝐝 a i j)) → P a)
+   (b:uuax A) (p: b ◃ U) on p : P b
+≝ ?.
+ 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 ]
+    ##| #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
+          [ #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/*) ]##]
+      #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;
+      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)]##]
+      #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)]##]
+      #Hcut1;
+      nlapply (infty b); nnormalize; nrewrite > E; nnormalize; #H2;
+      napply (H2 one); #b; ncases b; nnormalize
+       [ napply Hcut
+       | napply Hcut1
+       | napply (cover_rect A U memdec P refl infty a); nauto
+       | napply (cover_rect A U memdec P refl infty a1); nauto]##]*)
+       
+   ncases daemon.
+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.
+ #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; //]
+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 ??);
+ //.
+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))));
+       nrewrite > (easy1 …); nchange in ⊢ (% → ?) with (y = two * m);
+       #E; nrewrite > E; nassumption ]##]
+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)]
+ nnormalize; //.
+nqed.
\ No newline at end of file