(* *)
(**************************************************************************)
+include "arithmetics/nat.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.
napply infty; nauto; ##]
nqed.
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
+alias symbol "covers" (instance 1) = "covers".
nlemma cover_ind'':
∀A:Ax.∀U:Ω^A.∀P:A → CProp[0].
(∀a. a ∈ U → P a) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → (∀b. b ∈ 𝐂 a j → P b) → P a) →
∀b. b ◃ U → P b.
-
#A; #U; #P; nletin V ≝ {x | P x}; napply (cover_ind' … V).
nqed.
(*********** end from Cantor ********)
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers set".
+alias symbol "covers" (instance 9) = "covers".
+alias symbol "covers" (instance 8) = "covers".
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)
(* [##2: napply cover_rect] nauto depth=1; *)
[ napply Hcut
##| napply (cover_rect A U memdec P refl infty a); nauto ]##]
+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.//.
+nqed.
+
+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)) ]
+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))));
+ nnormalize; nrewrite < (plus_n_Sm …); nnormalize;
+ #E; nrewrite > E; napply H ]##]
+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