From d75c913a514c3a4299502a93d3025b03d2320109 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 20 Nov 2020 13:33:07 +0900
Subject: wip27

---
 vikalpa/prelude.scm | 145 +++++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 127 insertions(+), 18 deletions(-)

(limited to 'vikalpa')

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 874614d..264773d 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -17,7 +17,7 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa prelude)
-  #:export (atom? natural? size implies prelude)
+  #:export (atom? size implies natural? prelude)
   #:use-module (vikalpa))
 
 (define (atom? x)
@@ -41,17 +41,8 @@
      (if x (implies y z rest ...) #t))))
 
 (define-system prelude ()
-  (define-primitive-function natural? (x))
-  (define-primitive-function equal? (x y))
-  (define-primitive-function atom? (x))
-  (define-primitive-function cons (x y))
-  (define-primitive-function car (x))
-
-  (define-primitive-function cdr (x))
-  (define-primitive-function size (x))
-  (define-primitive-function not (x))
-  (define-primitive-function < (x y))
-
+  (define-function atom? (x)
+    (not (pair? x)))
   (define-syntax-rules list ()
     ((list) '())
     ((list x . y) (cons x (list . y))))
@@ -71,7 +62,7 @@
     ((implies x y) (if x y #t))
     ((implies x y z . rest)
      (if x (implies y z . rest) #t)))
-  
+
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
   (define-axiom equal-swap (x y)
@@ -93,24 +84,142 @@
         (equal? (if x y z) y)
         (equal? (if x y z) z)))
   (define-axiom if-true (x y)
-    (equal? (if '#f x y) y))
+    (equal? (if '#t x y) x))
   (define-axiom if-false (x y)
     (equal? (if '#f x y) y))
   (define-axiom if-same (x y)
     (equal? (if x y y) y))
-  (define-axiom natural/size (x)
+  (define-axiom natural?/size (x)
     (equal? (natural? (size x))
             '#t))
-  (define-axiom size/car (x)
+  (define-axiom </size/car (x)
     (if (atom? x)
         '#t
         (equal? (< (size (car x)) (size x))
                 '#t)))
-  (define-axiom size/cdr (x)
+  (define-axiom </size/cdr (x)
     (if (atom? x)
         '#t
         (equal? (< (size (cdr x)) (size x))
                 '#t)))
   (define-axiom if-not (x y z)
     (equal? (if (not x) y z)
-            (if x z y))))
+            (if x z y)))
+  (define-axiom sub1/add1 (x)
+    (implies (natural? x)
+             (equal? (sub1 (add1 x)) x)))
+  (define-axiom natural?/0 (x)
+    (equal? (natural? '0) '#t))
+  (define-axiom natural?/add1 (x)
+    (implies (natural? x)
+             (equal? (natural? (add1 x)) '#t)))
+  (define-axiom sub1/add1 (x)
+    (implies (natural? x)
+             (equal? (sub1 (add1 x)) x)))
+  (define-axiom </sub1 (x)
+    (implies (natural? x)
+             (equal? (< (sub1 x) x) '#t)))
+  (define-axiom common-add1 (x y)
+    (implies (natural? x)
+             (natural? y)
+             (equal? (equal? (add1 x) (add1 y))
+                     (equal? x y))))
+  (define-axiom false-if (x)
+    (if x '#t (equal? x '#f)))
+  (define-axiom equal?/01 (x)
+    (equal? (equal? '0 '1) #f))
+  (define-axiom natural?/sub1 (x)
+    (if (natural? x)
+        (if (equal? '0 x)
+            '#t
+            (equal? (natural? (sub1 x)) '#t))
+        '#t))
+  (define-axiom add1/sub1 (x)
+    (if (natural? x)
+        (if (equal? '0 x)
+            '#t
+            (equal? (add1 (sub1 x)) x))
+        '#t))
+  
+  (define-primitive-function + (x y)
+    (if (natural? x)
+        (if (equal? '0 x)
+            y
+            (add1 (+ (sub1 x) y)))
+        'undefined))
+
+  (define-proof +
+    (total/natural? x)
+    (((2) if-nest)
+     ((2 3) </sub1)
+     ((2) if-same)
+     (() if-same)))
+
+  (define-theorem thm-1+1=2 ()
+    (equal? (+ 1 1) 2))
+  
+  (define-function natural-induction (n)
+    (if (natural? n)
+        (if (equal? '0 n)
+            '0
+            (add1 (natural-induction (sub1 n))))
+        'undefined))
+
+  (define-proof natural-induction
+    (total/natural? n)
+    (((2) if-nest)
+     ((2 3) </sub1)
+     ((2) if-same)
+     (() if-same)))
+
+  (define-theorem equal?/add1 (n)
+    (if (natural? n)
+        (equal? (equal? n (add1 n)) #f)
+        #t))
+  
+  (define-proof equal?/add1
+    (induction (natural-induction n))
+    (((2 2 2 1 1) equal-if)
+     ((2 2 2 1 2 1) equal-if)
+     ((2 2 2 1) equal?/01)
+     ((2 2 2) equal-same)
+     ((2 2) if-same)
+     ((2 3 1 1) natural?/sub1)
+     ((2 3 1) if-true)
+     ((2 3 2 2 1 1) add1/sub1)
+     ((2 3 2 2 1 2 1) add1/sub1)
+     ((2 3 2 2) if-same (set x (natural? (add1 (sub1 n)))))
+     ((2 3 2 2) if-same (set x (natural? (sub1 n))))
+     ((2 3 2 2 2 2 1) common-add1
+      ;; ルール探索のアルゴリズムにバグがある
+      (set x (sub1 n))
+      (set y (add1 (sub1 n))))
+     ((2 3 2 2 2 2 1) equal-if)
+     ((2 3 2 2 2 2) equal-same)
+     ((2 3 2 2 2 1) natural?/add1)
+     ((2 3 2 2 2) if-true)
+     ((2 3 2 2 1) natural?/sub1)
+     ((2 3 2 2) if-true)
+     ((2 3 2) if-same)
+     ((2 3) if-same)
+     ((2) if-same)
+     ((3) if-nest)
+     (() if-same)))
+  
+  (define-proof thm-1+1=2
+    ()
+    ((() if-same (set x (natural? '0)))
+     ((2 1) +)
+     ((2 1 2 2 1) equal-if)
+     ((2 1 2 3 1 1) sub1/add1)
+     ((2 1 2 3 1) +)
+     ((2 1 2 3 1 2 1) equal-same)
+     ((2 1 2 3 1 2) if-true)
+     ((2 1 2 3 1 1) natural?/0)
+     ((2 1 2 3 1) if-true)
+     ((2 1 2) if-same)
+     ((2 1 1) natural?/add1)
+     ((2 1) if-true)
+     ((2) equal-same)
+     ((1) natural?/0)
+     (() if-true))))
-- 
cgit v1.2.3