From 7955016f0c6908c9d2e0578d75d4b2104f97e0a2 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 29 Nov 2020 10:26:40 +0900
Subject: wip41

---
 vikalpa/prelude.scm | 65 ++++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 49 insertions(+), 16 deletions(-)

(limited to 'vikalpa')

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 5b70a72..c7ab89e 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -51,16 +51,6 @@
     ((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 (zero? x)
-             (< 0 x))))
-
-  (define-totality-claim natural? natural? <)
-
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
 
@@ -109,10 +99,19 @@
     (implies (equal? (cons x1 y1) (cons x2 y2))
              (equal? y1 y2)))
 
+  (define-function zero? (x)
+    (equal? 0 x))
+
+  (define-function natural? (x)
+    (and (integer? x)
+         (or (zero? x)
+             (< 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))
@@ -121,16 +120,51 @@
   (define-axiom less/pred (x)
     (implies (natural? x)
              (equal? (< (pred x) x) #t)))
+  
+  (define-totality-claim natural? natural? <)
 
+  
   (define-function + (x y)
-    (if (natural? x)
-        (if (zero? x)
-            y
-            (succ (+ (pred x) y)))
-        'undeifned<+>))
+    (natural? x)
+    (natural? y)
+    (if (zero? x)
+        y
+        (succ (+ (pred x) y))))
+
+  (define-proof zero?
+    ()
+    ())
+
+  (define-proof natural?
+    ()
+    ())
+  (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)
@@ -142,7 +176,6 @@
   ;;    ((1 2 1) if-nest)
   ;;    ((1 3 1) if-nest)
   ;;    ((1 3) if-true)
-  ;;    (() equal-same)))
 
   ;; (define-proof less-than/pred
   ;;   (natural-induction x)
-- 
cgit v1.2.3