- ##| napply (cover_rect A U memdec P refl infty a); // ]##]
-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)] //.