From 9eca05b38858f9d5b36b9a102c6c8c01632b5057 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Jan 2010 10:46:34 +0000
Subject: [PATCH] Skipfact function (a partial general recursive function)
 defined by recursion over the cover relation of an IGFT.

---
 .../matita/nlibrary/topology/igft2.ma         | 69 +++++++++++++++++++
 1 file changed, 69 insertions(+)

diff --git a/helm/software/matita/nlibrary/topology/igft2.ma b/helm/software/matita/nlibrary/topology/igft2.ma
index 90a644ce9..4529b40d5 100644
--- a/helm/software/matita/nlibrary/topology/igft2.ma
+++ b/helm/software/matita/nlibrary/topology/igft2.ma
@@ -12,6 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+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.
@@ -118,4 +126,65 @@ nlet rec cover_rect
       (* [##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.
+ #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