(* 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.
+nlemma hint_auto2 : ∀T.∀U,V:Ω^T.(∀x.x ∈ U → x ∈ V) → U ⊆ V./2/.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).
[ #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.
(*>> 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) →
◃ U ⊆ P.
#A; #U; #P; #refl; #infty; #a; #H; nelim H
- [ nauto | (*nauto depth=4;*) #b; #j; #K1; #K2;
- napply infty; nauto; ##]
+ [ // | #b; #j; #K1; #K2; napply infty; //; ##]
nqed.
alias symbol "covers" (instance 3) = "ncovers".
∀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] ≝
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;
+ #A; #a; #x; #p; ncases p; //;
nqed.
nlemma eq_rect_Type0_r:
(*********** 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.
≝ ?.
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 ]
+ [ #_; #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; // ]
##| #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
+ [ nlapply E; nlapply (H ?) [//] 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); // ]
+ ##| #a; #a1; #E;
ncut (a ◃ U)
- [ nlapply E; nlapply (H ?) [nauto] ncases p
+ [ nlapply E; nlapply (H ?) [//] 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
+ [ nlapply E; nlapply (H ?) [//] 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 (cover_rect A U memdec P refl infty a); nauto
- | napply (cover_rect A U memdec P refl infty a1); nauto]##]*)
-
- ncases daemon.
+ napply (H2 one); #y; ncases y; nnormalize
+ [##1,2: nassumption
+ | napply (cover_rect A U memdec P refl infty a); //
+ | napply (cover_rect A U memdec P refl infty a1); //]
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 (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; //]
+ntheorem psym_plus: ∀n,m. n + m = m + n.//.
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 ??);
- //.
+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) (pred m)) ]
nqed.
ntheorem skipfact_base_dec:
∀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 …); // ]##]
nqed.
ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.
[ #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)]
- nnormalize; //.
+nlemma test: skipfact four ? = four * two * two. ##[##2: napply (skipfact_partial two)]//.
nqed.
\ No newline at end of file
projects / helm.git / blobdiff