From: Claudio Sacerdoti Coen Date: Fri, 15 Jan 2010 17:10:07 +0000 (+0000) Subject: A slightly more complicated example. X-Git-Tag: make_still_working~3120 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=93ea58f9369e5272116b4513f6c85400332c6710;p=helm.git A slightly more complicated example. --- diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma index 3abe4af70..904a17a9e 100644 --- a/helm/software/matita/nlibrary/topology/igft3.ma +++ b/helm/software/matita/nlibrary/topology/igft3.ma @@ -194,7 +194,7 @@ nqed. | S m ⇒ match m with [ O ⇒ skipfact O - | S _ ⇒ S m * skipfact (pred m) * skipfact O ]] + | S _ ⇒ S m * skipfact (pred m) * skipfact (pred m) ]] **) ntheorem psym_plus: ∀n,m. n + m = m + n. @@ -218,7 +218,7 @@ nlemma easy1: ∀n:nat. two * (S n) = two + two * n. nqed. ndefinition skipfact_dom: uuAx. - @ nat; #n; ncases n [ napply None | #m; ncases m [ napply (Some … O) | #_; napply (Twice … (pred m) O) ] + @ nat; #n; ncases n [ napply None | #m; ncases m [ napply (Some … O) | #_; napply (Twice … (pred m) (pred m)) ] nqed. ntheorem skipfact_base_dec: @@ -237,9 +237,8 @@ ntheorem skipfact_partial: | #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 …); // - ##| /2/ ] + | #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. @@ -254,6 +253,6 @@ ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x= napply (S m * H true * H false) ] nqed. -nlemma test: skipfact four ? = eight. ##[##2: napply (skipfact_partial two)] +nlemma test: skipfact four ? = four * two * two. ##[##2: napply (skipfact_partial two)] nnormalize; //. nqed. \ No newline at end of file