From 7d3ef19190fafe50c8b5930ae53b4e9e5b7ffe1f Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 21 Nov 2020 04:34:39 +0900
Subject: wip29

---
 vikalpa/prelude.scm | 208 +++++++++++++++++++++++++++++++++++++---------------
 1 file changed, 148 insertions(+), 60 deletions(-)

(limited to 'vikalpa')

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 8816131..c55ea48 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -17,23 +17,9 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa prelude)
-  #:export (atom? size implies natural? prelude)
+  #:export (implies prelude)
   #:use-module (vikalpa))
 
-(define (atom? x)
-  (not (pair? x)))
-
-(define (natural? x)
-  (and (integer? x)
-       (not (negative? x))))
-
-(define (size x)
-  (if (pair? x)
-      (+ 1
-         (size (car x))
-         (size (cdr x)))
-      0))
-
 (define-syntax implies
   (syntax-rules ()
     ((_ x y) (if x y #t))
@@ -41,8 +27,16 @@
      (if x (implies y z rest ...) #t))))
 
 (define-system prelude ()
-  (define-function atom? (x)
-    (not (pair? x)))
+  (define-primitive-function pair? (x y))
+  (define-primitive-function cons (x y))
+  (define-primitive-function car (x))
+  (define-primitive-function cdr (x))
+  (define-primitive-function sub1 (x))
+  (define-primitive-function add1 (x))
+  (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))))
@@ -62,23 +56,23 @@
     ((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)
     (equal? (equal? x y) (equal? y x)))
   (define-axiom equal-if (x y)
     (implies (equal? x y) (equal? x y)))
-  (define-axiom atom/cons (x y)
-    (equal? (atom? (cons x y)) '#f))
+  (define-axiom pair/cons (x y)
+    (equal? (pair? (cons x y)) '#t))
   (define-axiom car/cons (x y)
     (equal? (car (cons x y)) x))
   (define-axiom cdr/cons (x y)
     (equal? (cdr (cons x y)) y))
   (define-axiom cons/car+cdr (x)
-    (if (atom? x)
-        '#t
-        (equal? (cons (car x) (cdr x)) x)))
+    (if (pair? x)
+        (equal? (cons (car x) (cdr x)) x)
+        '#t))
   (define-axiom if-nest (x y z)
     (if x
         (equal? (if x y z) y)
@@ -89,65 +83,153 @@
     (equal? (if '#f x y) y))
   (define-axiom if-same (x y)
     (equal? (if x y y) y))
-  (define-axiom natural?/size (x)
-    (equal? (natural? (size x))
-            '#t))
-  (define-axiom </size/car (x)
-    (if (atom? x)
-        '#t
-        (equal? (< (size (car x)) (size x))
-                '#t)))
-  (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)))
+
+  (define-axiom axiom-less-than (x y)
+    (implies (natural? x)
+             (natural? y)
+             (equal? (< x y)
+                     (if (equal? '0 x)
+                         (if (equal? '0 y)
+                             #f
+                             #t)
+                         (if (equal? '0 y)
+                             #f
+                             (< (sub1 x) (sub1 y)))))))
+  (define-function natural-induction (n)
+    (if (natural? n)
+        (if (equal? '0 n)
+            '0
+            (add1 (natural-induction (sub1 n))))
+        'undefined))
+
+  (define-proof natural-induction
+    (natural? n)
+    ())
+
+  (define-axiom false-if (x)
+    (if x #t (equal? #f x)))
+  
   (define-axiom sub1/add1 (x)
     (implies (natural? x)
              (equal? (sub1 (add1 x)) x)))
-  (define-axiom natural?/0 (x)
+
+  (define-axiom natural/zero ()
     (equal? (natural? '0) '#t))
-  (define-axiom natural?/add1 (x)
-    (implies (natural? x)
-             (equal? (natural? (add1 x)) '#t)))
-  (define-axiom sub1/add1 (x)
+
+  (define-axiom not/true ()
+    (equal? (not #t) #f))
+
+  (define-axiom not/false ()
+    (equal? (not #f) #t))
+
+  (define-theorem equal/zero-less-than (x)
     (implies (natural? x)
-             (equal? (sub1 (add1 x)) x)))
-  (define-axiom </sub1 (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)))
+  
+  (define-axiom natural/sub1 (x)
     (implies (natural? x)
-             (equal? (< (sub1 x) x) '#t)))
-  (define-theorem common-add1 (x y)
+             (if (equal? '0 x)
+                 '#t
+                 (equal? (natural? (sub1 x)) #t))))
+  
+;; (define-proof natural-induction
+;;     (total/natural? n)
+;;     (((2) if-nest)
+;;      ((2 3) </sub1)
+;;      ((2) if-same)
+;;      (() if-same)))
+
+(define-theorem natural/add1 (x)
     (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)
+             (equal? (natural? (add1 x)) #t)))
+
+  #;
+  (define-axiom natural/sub1 (x)
     (if (natural? x)
-        (if (equal? '0 x)
-            '#t
-            (equal? (natural? (sub1 x)) '#t))
+        (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-primitive-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)
@@ -155,9 +237,11 @@
      ((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)
@@ -165,6 +249,7 @@
             (add1 (natural-induction (sub1 n))))
         'undefined))
 
+  #;
   (define-proof natural-induction
     (total/natural? n)
     (((2) if-nest)
@@ -172,11 +257,13 @@
      ((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)
@@ -205,7 +292,8 @@
      ((2) if-same)
      ((3) if-nest)
      (() if-same)))
-  
+
+  #;
   (define-proof thm-1+1=2
     ()
     ((() if-same (set x (natural? '0)))
-- 
cgit v1.2.3