From 634a86f552919afdb4e9cbb211c9a5371f86f45f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 15 Jan 2010 15:55:29 +0000 Subject: [PATCH] Extending to the nAx set. --- .../matita/nlibrary/topology/igft3.ma | 255 ++++++++++++++++++ 1 file changed, 255 insertions(+) create mode 100644 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 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 -- 2.39.2