From 616391177e0dbdaff8be7fb73d4ce14f9e97eb70 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 4 Dec 2020 04:12:22 +0900
Subject: wip43

---
 vikalpa/prelude.scm | 243 ++++------------------------------------------------
 1 file changed, 15 insertions(+), 228 deletions(-)

(limited to 'vikalpa')

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index c61e459..f37bdd0 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -17,16 +17,24 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa prelude)
-  #:export (natural? size implies prelude)
+  #:export (prelude)
   #:use-module (vikalpa))
 
-(define-syntax implies
-  (syntax-rules ()
-    ((_ x y) (if x y #t))
-    ((_ x y z rest ...)
-     (if x (implies y z rest ...) #t))))
-
 (define-system prelude ()
+  (define-function natural? (x)
+    (if (integer? x)
+        (< 0 x)
+        #f))
+
+  (define-syntax-rules + ()
+    ((+ x . xs) (binary-+ x (+ . xs)))
+    ((+ x) x)
+    ((+) '0))
+
+  (define-syntax-rules - ()
+    ((- x . xs) (binary-+ x (- . xs)))
+    ((- x) (unary-- x)))
+  
   (define-syntax-rules list ()
     ((list) '())
     ((list x . y) (cons x (list . y))))
@@ -102,226 +110,5 @@
   (define-function zero? (x)
     (equal? 0 x))
 
-  (define-axiom pred/succ (x)
-    (implies (natural? x)
-             (equal? (pred (succ x)) x)))
-
-
-  (define-axiom succ/pred (x)
-    (implies (natural? x)
-             (not (zero? x))
-             (equal? (succ (pred x)) x)))
-
-  (define-axiom less/pred (x)
-    (implies (natural? x)
-             (equal? (< (pred x) x) #t)))
-  
   (define-totality-claim natural? natural? <)
-  (define-function + (x y)
-    (natural? x)
-    (natural? y)
-    (if (zero? x)
-        y
-        (succ (+ (pred x) y))))
-
-  (define-proof +
-    (natural? x)
-    ())
-  
-  #;
-  (define-proof natural?
-    ()
-    (((1 2 3 1) (eval))
-     ((1 2 3) if-true)
-     (() if-same (set x (zero? x)))
-     ((2 1 2) if-nest)
-     ((2 1) if-same)
-     ((2) if-true)
-     ((3 1 2) if-nest)
-     ((3) if-same (set x (integer? x)))
-     ((3 2 1) if-nest)
-     ((3 2) if-nest)
-     ((3 3 1) if-nest)
-     ((3 3) if-true)
-     ((3) if-same)
-     (() if-same)))
-
-  #;
-  (define-proof +
-    (natural? x)
-    ()
-    #;
-    (((2) if-nest)
-     ((2 3) less/pred)
-     ((2) if-same)
-     (() if-same)))
-  
-  ;; (define-proof if-implies
-  ;;   ()
-  ;;   (((1) if-same (set x x))
-  ;;    ((1 2 1) if-nest)
-  ;;    ((1 3 1) if-nest)
-  ;;    ((1 3) if-true)
-
-  ;; (define-proof less-than/pred
-  ;;   (natural-induction x)
-  ;;   (((2 2) if-nest)
-  ;;    ((2 2) if-not)
-  ;;    ((2 2) if-nest)
-  ;;    ((2 3 2) if-nest)
-  ;;    ((2 3 2) if-nest)
-  ;;    ((2 3) if-implies)
-  ;;    ((2 3 2) if-implies)
-     
-  ;;    (() error)
-  ;;    (() error)))
-
-  ;; (define-proof less-than/pred-1
-  ;;   ()
-  ;;   (((2 2) if-same (set x (natural? (pred x))))
-  ;;    ((2 2 2) if-same (set x (not (zero? (pred x)))))
-  ;;    ((2 2 2) if-same (set x (not (zero? (pred x)))))
-  ;;    ;; ((2 2 3 1 1) zero?)
-  ;;    ;; ((2 2 3 1 1) if-nest)
-  ;;    ;; ((2 2 3 1) if-false)
-  ;;    ;; ((2 2 3 1) if-false)
-  ;;    ))
-  
-
-
-  ;; (define-theorem natural/add1 (x)
-  ;;     (implies (natural? x)
-  ;;              (equal? (natural? (add1 x)) #t)))
-
-  #;
-  (define-axiom natural/sub1 (x)
-  (if (natural? x)
-  (if (< '0 x)
-  (equal? (natural? (sub1 x)) '#t)
-  '#t)
-  '#t))
-
-  #;
-  (define-theorem less-than/sub1 (x)
-  (implies (natural? x)
-  (< '0 x)
-  (equal? (< (sub1 x) x) '#t)))
-
-  #;
-  (define-axiom add1/sub1 (x)
-  (if (natural? x)
-  (if (equal? '0 x)
-  '#t
-  (equal? (add1 (sub1 x)) x))
-  '#t))
-
-  #;
-  (define-built-in-function + (x y)
-  (if (natural? x)
-  (if (equal? '0 x)
-  y
-  (add1 (+ (sub1 x) y)))
-  'undefined))
-
-  #;
-  (define-axiom natural/size (x)
-  (equal? (natural? (size x))
-  '#t))
-
-  #;
-  (define-axiom size/car (x)
-  (if (pair? x)
-  (equal? (< (size (car x)) (size x))
-  '#t)
-  '#t))
-
-  #;
-  (define-axiom size/cdr (x)
-  (if (pair? x)
-  (equal? (< (size (cdr x)) (size x))
-  '#t)
-  '#t))
-  
-  #;
-  (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