From 52d0f284f3c8c26eb86c4dcd8f3f819c657e7d78 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 29 Nov 2020 02:45:39 +0900
Subject: wip36

---
 vikalpa/prelude.scm | 355 ++++++++++++++++++++++++++++------------------------
 1 file changed, 192 insertions(+), 163 deletions(-)

(limited to 'vikalpa')

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index d03df7e..1ee56af 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -27,10 +27,6 @@
      (if x (implies y z rest ...) #t))))
 
 (define-system prelude ()
-  (define-primitive-function < (x y))
-  (define-primitive-function natural? (x))
-  (define-totality-claim natural? natural? <)
-
   (define-syntax-rules list ()
     ((list) '())
     ((list x . y) (cons x (list . y))))
@@ -54,7 +50,18 @@
     ((implies x y) (if x y #t))
     ((implies x y z . rest)
      (if x (implies y z . rest) #t)))
+
+  (define-function zero? (x)
+    (equal? 0 x))
+
+  (define-function natural? (x)
+    (and (integer? x)
+         (or (equal? x 0)
+             (< x 0))))
+
+  (define-totality-claim natural? natural? <)
   
+
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
 
@@ -82,222 +89,244 @@
     (equal? (if (not x) y z)
             (if x z y)))
 
-  (define-axiom pair-cons (x y)
+  (define-axiom pair/cons (x y)
     (equal? (pair? (cons x y)) '#t))
 
-  (define-axiom car-cdr-elim (x)
-    (if (pair? x)
-        (equal? (cons (car x) (cdr x)) x)
-        '#t))
+  (define-axiom cons/car+cdr (x)
+    (implies (pair? x)
+             (equal? (cons (car x) (cdr x)) x)))
 
-  (define-axiom car-cons (x y)
+  (define-axiom car/cons (x y)
     (equal? (car (cons x y)) x))
 
-  (define-axiom cdr-cons (x y)
+  (define-axiom cdr/cons (x y)
     (equal? (cdr (cons x y)) y))
-  
-  (define-axiom car-cdr-elim (x)
-    (implies (pair? x)
-             (equal? (cons (car x) (cdr x)) x)))
 
-  (define-axiom cons-equal-car (x1 y1 x2 y2)
+  (define-axiom equal-car (x1 y1 x2 y2)
     (implies (equal? (cons x1 y1) (cons x2 y2))
              (equal? x1 x2)))
 
-  (define-axiom cons-equal-cdr (x1 y1 x2 y2)
+  (define-axiom equal-cdr (x1 y1 x2 y2)
     (implies (equal? (cons x1 y1) (cons x2 y2))
              (equal? y1 y2)))
-  
-  #;
-  (define-axiom natural?/0 ()
-    (equal? (natural? '0) '#t))
 
-  #;
-  (define-theorem equal/zero-less-than (x)
+  (define-axiom pred/succ (x)
     (implies (natural? x)
-             (equal? (not (< '0 x))
-                     (equal? x '0))))
-
-  #;
-  (define-proof equal/zero-less-than
-    (natural-induction x)
-    (((2 2) if-nest)
-     ((3) if-nest)
-     ((2 2 1) if-same (set x (natural? '0)))
-     ((2 2 1 2 1) axiom-less-than)
-     ((2 2 1 1) natural/zero)
-     ((2 2 1) if-true)
-     ((2 2 1 1 1) equal-same)
-     ((2 2 1 1) if-true)
-     ((2 2 1 1 1 2) equal-if)
-     ((2 2 1 1 1) equal-same)
-     ((2 2 1 1) if-true)
-     ((2 2 1) not/false)
-     ((2 2 2 1) equal-if)
-     ((2 2 2) equal-same)
-     ((2 2) equal-same)
-     ((2 3 2 2) if-same (set x (natural? '0)))
-     ((2 3 2 2 2 1 1) axiom-less-than)
-     ((2 3 2 2 2 1 1 1) equal-same)
-     ((2 3 2 2 2 1 1) if-true)
-     ((2 3 2 2 2 1 1) if-nest)
-     ((2 3 2 2 2 1) not/true)
-     ((2 3 2 2 2 2) equal-swap)
-     ((2 3 2 2 2 2) false-if)
-     ((2 3 2 2 2) equal-same)
-     ((2 3 2 2 1) natural/zero)
-     ((2 3 2 2) if-true)
-     ((2 3 2) if-same)
-     ((2 3) if-same)
-     ((2) if-same)
-     (() if-same)))
+             (equal? (pred (succ x)) x)))
   
-  ;; (define-axiom natural/sub1 (x)
-  ;;   (implies (natural? x)
-  ;;            (if (equal? '0 x)
-  ;;                '#t
-  ;;                (equal? (natural? (sub1 x)) #t))))
+  (define-axiom succ/pred (x)
+    (implies (natural? x)
+             (not (zero? x))
+             (equal? (succ (pred x)) x)))
+
+  (define-theorem less-than/pred-1 (x)
+    (implies (not (zero? x))
+             (natural? x)
+             (natural? (pred x))
+             (not (zero? (pred x)))
+             (equal? (< (pred (pred x)) (pred x)) '#t)
+             (equal?
+              (if (zero? (pred x))
+                  '#t
+                  (< (pred (pred x)) (pred x)))
+              '#t)))
   
-;; (define-proof natural-induction
-;;     (total/natural? n)
-;;     (((2) if-nest)
-;;      ((2 3) </sub1)
-;;      ((2) if-same)
-;;      (() if-same)))
+  (define-theorem if-implies (x y z w)
+    (equal? (if (if x y #t)
+                z
+                w)
+            (if x
+                (if y
+                    z
+                    w)
+                z)))
+
+  (define-theorem less-than/pred-2 (x)
+    (implies (not (natural? x))
+             (equal? (zero? x) #f)))
+
+  (define-primitive-function natural-induction (x)
+    (if (natural? x)
+        (if (zero? x)
+            0
+            (succ (natural-induction (pred x))))
+        #f))
 
-;; (define-theorem natural/add1 (x)
-;;     (implies (natural? x)
-;;              (equal? (natural? (add1 x)) #t)))
+  (define-theorem less-than/pred (x)
+    (implies (natural? x)
+             (not (zero? x))
+             (equal? (< (pred x) x) #t)))
+
+  ;; (define-proof if-implies
+  ;;   ()
+  ;;   (((1) if-same (set x x))
+  ;;    ((1 2 1) if-nest)
+  ;;    ((1 3 1) if-nest)
+  ;;    ((1 3) if-true)
+  ;;    (() equal-same)))
+
+  ;; (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-function + (x y)
+    (if (equal? 0 x)
+        y
+        (succ (+ (pred x) y))))
+
+  ;; (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))
+  (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)))
+  (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))
+  (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))
+  (if (natural? x)
+  (if (equal? '0 x)
+  y
+  (add1 (+ (sub1 x) y)))
+  'undefined))
 
-#;
+  #;
   (define-axiom natural/size (x)
-    (equal? (natural? (size x))
-            '#t))
+  (equal? (natural? (size x))
+  '#t))
 
   #;
   (define-axiom size/car (x)
-    (if (pair? x)
-        (equal? (< (size (car x)) (size x))
-                '#t)
-        '#t))
+  (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))
+  (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)))
+  (total/natural? x)
+  (((2) if-nest)
+  ((2 3) </sub1)
+  ((2) if-same)
+  (() if-same)))
 
   #;
   (define-theorem thm-1+1=2 ()
-    (equal? (+ 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))
+  (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)))
+  (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))
+  (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)))
+  (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-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