From 0029f0e5eb02144133f6e005faccd09be8f9428c Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 20 Dec 2020 05:12:02 +0900
Subject: wip60

---
 vikalpa/prelude.scm | 459 +++++++++++++++++++++++++++++++++++++++++++---------
 1 file changed, 386 insertions(+), 73 deletions(-)

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 125c8d6..9fb7571 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -17,16 +17,41 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa prelude)
-  #:export (prelude)
+  #:export (exact-positive-integer?
+            exact-negative-integer?
+            succ pred
+            implies
+            negate
+            prelude)
   #:use-module (vikalpa))
 
-(define-syntax-rule (define-proof/is name p t1 t2)
-  (define-proof name
-    (((2) if-same (set x (p x)))
-     ((2 2 1) t1)
-     ((2 2) equal-same)
-     ((2) t2)
-     (() if-same))))
+(define (exact-positive-integer? x)
+  (and (exact-integer? x)
+       (positive? x)))
+
+(define (exact-negative-integer? x)
+  (and (exact-integer? x)
+       (negative? x)))
+
+(define (succ x)
+  (if (number? x)
+      (+ x 1)
+      1))
+
+(define (pred x)
+  (if (number? x)
+      (- x 1)
+      -1))
+
+(define (negate x)
+  (if (exact-integer? x)
+      (- x)
+      0))
+
+(define-syntax implies
+  (syntax-rules ()
+    ((_ x y) (if x y #t))
+    ((_ x y z ...) (if x (implies y z ...) #t))))
 
 (define-system prelude/macros ()
   (define-syntax-rules and ()
@@ -52,7 +77,9 @@
   (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))))
+    (implies (equal? x y) (equal? x y)))
+  (define-axiom equal-if-false (x y)
+    (if x #t (equal? x #f))))
 
 (define-system prelude/if (prelude/equal)
   (define-axiom if-nest (x y z)
@@ -70,61 +97,159 @@
             (if x z y))))
 
 (define-system prelude/number (prelude/if)
-  (define-core-function number? (x) number?)
-  (define-core-function rational? (x) rational?)
-  (define-core-function integer? (x) integer?)
+  (define-core-function integer? (x) exact-integer?)
+  (define-core-function positive-integer? (x) exact-positive-integer?)
+  (define-core-function negative-integer? (x) exact-negative-integer?)
+  (define-core-function negate (x) negate)
+  (define-function natural? (x)
+    (if (integer? x)
+        (not (negative-integer? x))
+        #f))
   (define-function zero? (x)
     (equal? x 0))
-  (define-core-function < (x y)
-    (lambda (x y)
-      (if (rational? x)
-          (if (rational? y)
-              (< x y)
-              (< x 0))
-          (if (rational? y)
-              (< 0 y)
-              #f))))
-  (define-axiom axiom-< (x y)
-    (if (rational? x)
-        (if (rational? y)
+  (define-core-function succ (x) succ)
+  (define-core-function pred (x) pred)
+  (define-axiom succ/pred (x)
+    (implies (integer? x)
+             (equal? (succ (pred x)) x)))
+  (define-trivial-total-function < (x y)
+    (if (positive-integer? x)
+        (if (positive-integer? y)
+            (< (pred x) (pred y))
+            #f)
+        (if (positive-integer? y)
             #t
-            (equal? (< x y) (< x 0)))
-        (if (rational? y)
-            (equal? (< x y) (< 0 y))
-            (equal? (< x y) #f))))
-  (define-function natural? (x)
+            (if (negative-integer? x)
+                (if (negative-integer? y)
+                    (< (succ x) (succ y))
+                    #t)
+                #f))))
+  (set-measure-predicate natural?)
+  (set-measure-less-than <)
+  (define-axiom integer?-is-predicate (x)
+    (implies (integer? x)
+             (equal? (integer? x) #t)))
+  (define-axiom integer/pred (x)
+    (implies (integer? x)
+             (equal? (integer? (pred x)) #t)))
+  (define-axiom integer/succ (x)
+    (implies (integer? x)
+             (equal? (integer? (pred x)) #t)))
+  (define-axiom positive-integer?-is-predicate (x)
+    (implies (positive-integer? x)
+             (equal? (positive-integer? x) #t)))
+  (define-axiom negative-integer?-is-predicate (x)
+    (implies (negative-integer? x)
+             (equal? (negative-integer? x) #t)))
+  (define-axiom natural/pred (x)
+    (implies (positive-integer? x)
+             (equal? (natural? (pred x)) #t)))
+  (define-axiom positive-integer/succ (x)
+    (implies (natural? x)
+             (equal? (positive-integer? (pred x)) #t)))
+  (define-axiom positive-integer-is-integer (x)
+    (implies (positive-integer? x)
+             (equal? (integer? x) #t)))
+  (define-axiom negative-integer-is-integer (x)
+    (implies (negative-integer? x)
+             (equal? (integer? x) #t)))
+  (define-axiom axiom-zero (x)
+    (if (integer? x)
+        (if (positive-integer? x)
+            (equal? (zero? x) #f)
+            (if (negative-integer? x)
+                (equal? (zero? x) #f)
+                (equal? (zero? x) #t)))
+        (equal? (zero? x) #f)))
+  (define-axiom axiom-positive-integer (x)
     (if (integer? x)
+        (if (negative-integer? x)
+            (equal? (positive-integer? x) #f)
+            (if (zero? x)
+                (equal? (positive-integer? x) #f)
+                (equal? (positive-integer? x) #t)))
+        (equal? (positive-integer? x) #f)))
+  (define-axiom axiom-negative-integer (x)
+    (if (integer? x)
+        (if (positive-integer? x)
+            (equal? (negative-integer? x) #f)
+            (if (zero? x)
+                (equal? (negative-integer? x) #f)
+                (equal? (negative-integer? x) #t)))
+        (equal? (negative-integer? x) #f)))
+  (define-axiom integer/negate (x)
+    (implies (integer? x)
+             (equal? (integer? (negate x)) #t)))
+  (define-axiom positive-integer/negate (x)
+    (if (negative-integer? x)
+        (equal? (positive-integer? (negate x)) #t)
+        (implies (integer? x)
+                 (equal? (positive-integer? (negate x)) #f))))
+  (define-axiom negative-integer/negate (x)
+    (if (positive-integer? x)
+        (equal? (negative-integer? (negate x)) #t)
+        (implies (integer? x)
+                 (equal? (negative-integer? (negate x)) #f))))
+  (define-axiom zero/negate (x)
+    (implies (zero? x)
+             (equal? (zero? (negate x)) #t)))
+  (define-function abs (x)
+    (if (integer? x)
+        (if (negative-integer? x)
+            (negate x)
+            x)
+        0))
+  (define-theorem natural-is-integer (x)
+    (if (natural? x)
+        (equal? (integer? x) #t)
+        #t))
+  (define-theorem natural/abs (x)
+    (equal? (natural? (abs x)) #t))
+  (define-theorem zero-is-0 (x)
+    (implies (zero? x)
+             (equal? x 0)))
+  (define-theorem not-natural-implies-not-positive-integer (x)
+    (implies (not (natural? x))
+             (equal? (positive-integer? x) #f)))
+  (define-theorem natural-and-not-zero-implies-positive-integer (x)
+    (implies (natural? x)
+             (not (zero? x))
+             (equal? (positive-integer? x) #t)))
+  (define-theorem %abs/pred--zero/pred (x)
+    (implies (integer? x)
+             (not (positive-integer? x))
+             (natural? x)
+             (equal? (zero? x) #t)))
+  (define-theorem %abs/pred--x-is-1 (x)
+    (implies (positive-integer? x)
+             (not (positive-integer? (pred x)))
+             (equal? x 1)))
+  (define-theorem %abs/pred-1 (x)
+    (implies (positive-integer? x)
+             (positive-integer? (pred x))
+             (equal? (< (pred x) x) #t)))
+  (define-theorem abs/pred (x)
+    (if (positive-integer? x)
+        (equal? (< (abs (pred x)) (abs x)) #t)
+        #t))
+  (define-theorem abs/succ (x)
+    (if (negative-integer? x)
+        (equal? (< (abs (succ x)) (abs x)) #t)
+        #t))
+  (define-function natural-induction (x)
+    (if (natural? x)
         (if (zero? x)
-            #t
-            (< 0 x))
-        #f))
-  (define-axiom rational-is-number (x y z)
-    (implies (rational? x) (equal? (if (number? x) y z) y)))
-  (define-axiom integer-is-rational (x y z)
-    (implies (integer? x) (equal? (if (rational? x) y z) y)))
-  (define-theorem integer-is-number (x y z)
-    (implies (integer? x) (equal? (if (number? x) y z) y)))
-  (define-theorem natural-is-integer (x y z)
-    (implies (natural? x) (equal? (if (integer? x) y z) y)))
-  (define-theorem natural-is-rational (x y z)
-    (implies (natural? x) (equal? (if (rational? x) y z) y)))
-  (define-theorem natural-is-number (x y z)
-    (implies (natural? x) (equal? (if (number? x) y z) y)))
-  (define-core-function + (x y)
-    (lambda (x y)
-      (if (number? x)
-          (if (number? y)
-              (+ x y)
-              (+ x 0))
-          (if (number? y)
-              (+ 0 y)
-              0)))))
-
-(define-system prelude/measure (prelude/number)
-  (set-measure-predicate natural?)
-  (set-measure-less-than <))
+            0
+            (succ (natural-induction (pred x))))
+        0))
+  (define-function + (x y)
+    (if (positive-integer? x)
+        (succ (+ (pred x) y))
+        (if (negative-integer? x)
+            (pred (+ (succ x) y))
+            y))))
 
-(define-system prelude/pair (prelude/measure)
+(define-system prelude/pair (prelude/number)
   (define-core-function pair? (x) pair?)
   (define-core-function cons (x y) cons)
   (define-core-function car (x)
@@ -152,30 +277,217 @@
               (tree-induction (cdr x))))))
 
 (define-system prelude/proofs (prelude/tree)
-  (define-proof/is integer-is-number
-    rational?
-    rational-is-number
-    integer-is-rational)
+  (define-proof natural/abs
+    (((1) natural?)
+     ((1 1 1) abs)
+     ((1 1) if-same (set x (integer? x)))
+     ((1 1 3 1) if-nest)
+     ((1 1 3) integer?)
+     ((1 1 2 1) if-nest)
+     ((1 1 2) if-same (set x (negative-integer? x)))
+     ((1 1 2 2 1) if-nest)
+     ((1 1 2 2) integer/negate)
+     ((1 1 2 3 1) if-nest)
+     ((1) if-same (set x (integer? x)))
+     ((1 3 1) if-nest)
+     ((1 3) if-true)
+     ((1 3 1 1) abs)
+     ((1 3 1 1) if-nest)
+     ((1 3 1) negative-integer?)
+     ((1 3) not)
+     ((1 2 1) if-nest)
+     ((1 2 1 3) integer?-is-predicate)
+     ((1 2 1) if-same)
+     ((1 2) if-true)
+     ((1 2 1 1) abs)
+     ((1 2 1 1) if-nest)
+     ((1 2) if-same (set x (negative-integer? x)))
+     ((1 2 2 1 1) if-nest)
+     ((1 2 3 1 1) if-nest)
+     ((1 2 3 1) equal-if-false)
+     ((1 2 3) not)
+     ((1 2 2) if-same (set x (positive-integer? x)))
+     ((1 2 2 2 1) negative-integer/negate)
+     ((1 2 2 2) not)
+     ((1 2 2 3 1) negative-integer/negate)
+     ((1 2 2 3) not)
+     ((1 2 2 1) axiom-positive-integer)
+     ((1 2 2) if-false)
+     ((1 2) if-same)
+     ((1) if-same)
+     (() equal?)))
 
-  (define-proof natural-is-integer
-    ((() if-same (set x (integer? x)))
+  (define-proof abs/pred
+    (((2 1 1) abs)
+     ((2 1) if-same (set x (positive-integer? (pred x))))
+     ((2 1 2 1 2 1) axiom-negative-integer)
+     ((2 1 2 1 2) if-false)
+     ((2 1 2 1 1) positive-integer-is-integer)
+     ((2 1 2 1) if-true)
+     ((2 1 2 2) abs)
+     ((2 1 2 2 1) positive-integer-is-integer)
+     ((2 1 2 2) if-true)
+     ((2 1 2 2) if-same (set x (integer? x)))
+     ((2 1 2 2 2 1) axiom-negative-integer)
+     ((2 1 2 2 2) if-false)
+     ((2 1 2 2 3 1) axiom-negative-integer)
+     ((2 1 2 2 3) if-false)
+     ((2 1 2 2) if-same)
+     ((2 1 2) %abs/pred-1)
+     ((2 1 3) if-same (set x (integer? (pred x))))
+     ((2 1 3 2 1) if-nest)
+     ((2 1 3 3 1) if-nest)
+     ((2 1 3 2) if-same (set x (negative-integer? (pred x))))
+     ((2 1 3 2 2 1) if-nest)
+     ((2 1 3 2 3 1) if-nest)
+     ((2 1 3 1 1 1) %abs/pred--x-is-1)
+     ((2 1 3 2 1 1 1) %abs/pred--x-is-1)
+     ((2 1 3 2 2 1 1 1) %abs/pred--x-is-1)
+     ((2 1 3 2 2 2 1) %abs/pred--x-is-1)
+     ((2 1 3 2 3 1 1) %abs/pred--x-is-1)
+     ((2 1 3 2 3 2 1) %abs/pred--x-is-1)
+     ((2 1 3 3 2 1) %abs/pred--x-is-1)
+     ((2 1 3) (eval))
+     ((2 1) if-same)
+     ((2) equal-same)
+     (() if-same)))
+
+  (define-proof %abs/pred-1
+    (natural-induction x)
+    (((2 2 1 1) zero-is-0)
+     ((2 2 1) positive-integer?)
+     ((2 2) if-false)
+     ((2 3) if-same (set x (positive-integer? (pred x))))
+     ((2 3 2 1) if-nest)
+     ((2 3 3 1) if-nest)
+     ((2 3 3) if-true)
+     ((2 3 2 2 2) if-nest)
+     ((2 3 2 2 1) natural-and-not-zero-implies-positive-integer)
+     ((2 3 2 2) if-true)
+     ((2 3 2) if-same (set x (positive-integer? (pred (pred x)))))
+     ((2 3 2 2 1) if-nest)
+     ((2 3 2 3 1) if-nest)
+     ((2 3 2 3) if-true)
+     ((2 3 2 2 2 1) <)
+     ((2 3 2 2 2 1) if-nest)
+     ((2 3 2 2 2 1 1) natural-and-not-zero-implies-positive-integer)
+     ((2 3 2 2 2 1) if-true)
+     ((2 3 2 2 2 1) equal-if)
+     ((2 3 2 2 2) equal?)
+     ((2 3 2 2) if-same)
+     ((2 3 2 3 1) <)
+     ((2 3 2 3 1) if-nest)
+     ((2 3 2 3 1 1) natural-and-not-zero-implies-positive-integer)
+     ((2 3 2 3 1) if-true)
+     ((2 3 2 3 1 1 1) %abs/pred--x-is-1)
+     ((2 3 2 3 1 2) %abs/pred--x-is-1)
+     ((2 3 2 3) (eval))
+     ((2 3 2) if-same)
+     ((2 3 3 2) if-nest)
+     ((2 3 3) if-same)
+     ((2 3) if-same)
+     ((2) if-same)
+     ((3 1) not-natural-implies-not-positive-integer)
+     ((3) if-false)
+     (() if-same)))
+
+  (define-proof %abs/pred--x-is-1
+    (((2 2) if-same (set x (zero? (pred x))))
+     ((2 2 2) if-same (set x (integer? x)))
+     ((2 2 2 2 1) succ/pred)
+     ((2 2 2 2 1 1) zero-is-0)
+     ((2 2 2 2) (eval))
+     ((2 2 2 1) positive-integer-is-integer)
+     ((2 2 2) if-true)
+     ((2 2) if-same (set x (natural? (pred x))))
+     ((2 2 2) if-same (set x (integer? (pred x))))
+     ((2 2 2 2 1) %abs/pred--zero/pred)
+     ((2 2 2 2) if-true)
+     ((2 2 2 1) natural-is-integer)
+     ((2 2 2) if-true)
+     ((2 2 1) natural/pred)
+     ((2 2) if-true)
+     ((2) if-same)
+     (() if-same)))
+
+  (define-proof %abs/pred--zero/pred
+    (((2 2 1) natural?)
      ((2 2 1) if-nest)
+     ((2 2 2) if-same (set x (zero? x)))
+     ((2 2 2 2 1 1) zero-is-0)
+     ((2 2 2 2) (eval))
+     ((2 2 2 1) axiom-zero)
+     ((2 2 2) if-true)
+     ((2 2) if-same)
+     ((2) if-same)
+     (() if-same)))
+
+  (define-proof natural-is-integer
+    (((1) natural?)
+     (() if-same (set x (integer? x)))
+     ((2 2 1) integer?-is-predicate)
      ((2 2) equal-same)
      ((2) if-same)
-     ((3 1) natural?)
      ((3 1) if-nest)
      ((3) if-false)
      (() if-same)))
 
-  (define-proof/is natural-is-rational
-    integer?
-    integer-is-rational
-    natural-is-integer)
+  (define-proof zero-is-0
+    (((1) zero?)
+     ((2 1) equal-if)
+     ((2) equal?)
+     (() if-same)))
+  
+  (define-proof not-natural-implies-not-positive-integer
+    (((1 1) natural?)
+     (() if-same (set x (integer? x)))
+     ((2 1 1) if-nest)
+     ((2) if-not)
+     ((2) if-not)
+     ((2 2) if-same (set x (positive-integer? x)))
+     ((2 2 3 1) equal-if-false)
+     ((2 2 3) equal?)
+     ((2 2 1) axiom-positive-integer)
+     ((2 2) if-false)
+     ((2) if-same)
+     ((3 1 1) if-nest)
+     ((3 1) not)
+     ((3) if-true)
+     ((3 1) axiom-positive-integer)
+     ((3) equal?)
+     (() if-same)))
+
+  (define-proof natural-and-not-zero-implies-positive-integer
+    (((1) natural?)
+     (() if-same (set x (integer? x)))
+     ((2 1) if-nest)
+     ((2 2 2 1) axiom-positive-integer)
+     ((2 2 2) equal?)
+     ((2 2) if-same)
+     ((2) if-same)
+     ((3 1) if-nest)
+     ((3) if-false)
+     (() if-same)))
+  
+  (define-proof natural-induction
+    (abs x)
+    (((1) natural/abs)
+     (() if-true)
+     ((2 3) if-same (set x (positive-integer? x)))
+     ((2 3 2) abs/pred)
+     ((2 3 1) natural-and-not-zero-implies-positive-integer)
+     ((2 3) if-true)
+     ((2) if-same)
+     (() if-same)))
 
-  (define-proof/is natural-is-number
-    rational?
-    rational-is-number
-    natural-is-rational)
+  (define-proof +
+    (abs x)
+    (((1) natural/abs)
+     (() if-true)
+     ((2) abs/pred)
+     ((3 2) abs/succ)
+     ((3) if-same)
+     (() if-same)))
   
   (define-proof tree-induction
     (size x)
@@ -186,4 +498,5 @@
      ((1) natural/size)
      (() if-true))))
 
+
 (define-system prelude (prelude/proofs))
-- 
cgit v1.2.3