From 0f5ef2e0cbca8065fb3a804a27813cfecc984120 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 3 Jan 2021 19:19:20 +0900
Subject: wip62

---
 vikalpa/prelude.scm | 534 +++++++++++-----------------------------------------
 1 file changed, 107 insertions(+), 427 deletions(-)

(limited to 'vikalpa')

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 66d2b73..176983c 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -1,5 +1,5 @@
 ;;; Vikalpa --- Proof Assistant
-;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
+;;; Copyright © 2020, 2021 Masaya Tojo <masaya@tojo.tokyo>
 ;;;
 ;;; This file is part of Vikalpa.
 ;;;
@@ -48,25 +48,23 @@
     ((_ x y) (if x y #t))
     ((_ x y z ...) (if x (implies y z ...) #t))))
 
-(define-system prelude/macros ()
-  (define-syntax-rules and ()
-    ((and) '#t)
-    ((and x) x)
-    ((and x . xs) (if x (and . xs) #f)))
-  (define-syntax-rules or ()
-    ((or) '#f)
-    ((or x) x)
-    ((or x . xs) (if x x (or . xs))))
+(define-system prelude/macro ()
   (define-syntax-rules cond (else)
     ((cond (else e)) e)
     ((cond (test then) . rest)
      (if test then (cond . rest))))
+  (define-syntax-rules or ()
+    ((or) '#f)
+    ((or x) x)
+    ((or x . xs) (if x x (or . xs))))
   (define-syntax-rules implies ()
     ((implies x y) (if x y #t))
     ((implies x y z . rest)
-     (if x (implies y z . rest) #t))))
+     (if x (implies y z . rest) #t)))
+  (define-syntax-rules is-a ()
+    ((is-a x y) (implies x (equal? y #t)))))
 
-(define-system prelude/equal (prelude/macros)
+(define-system prelude/axiom/equal (prelude/macro)
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
   (define-axiom equal-swap (x y)
@@ -76,7 +74,7 @@
   (define-axiom equal-if-false (x y)
     (if x #t (equal? x #f))))
 
-(define-system prelude/if (prelude/equal)
+(define-system prelude/axiom/if (prelude/axiom/equal)
   (define-axiom if-nest (x y z)
     (if x
         (equal? (if x y z) y)
@@ -91,426 +89,108 @@
     (equal? (if (not x) y z)
             (if x z y))))
 
-(define-system prelude/integer (prelude/if)
-  (define-core-function integer? (x) exact-integer?)
-  (define-core-function positive-integer? (x) exact-positive-integer?)
-  (define-function zero? (x)
-    (equal? x 0))
+(define-system prelude/number (prelude/axiom/if)
+  (define-core-function number? (x) number?)
+  (define-axiom number-predicate (x)
+    (is-a (number? x) (number? x)))
+
+  (define-core-function real? (x) real?)
+  (define-axiom real-predicate (x)
+    (implies (real? x) (equal? (real? x) #t)))
+  (define-axiom real-is-a-numbers (x)
+    (implies (real? x) (equal? (number? x) #t)))
+
+  (define-core-function integer? (x) integer?)
+  (define-axiom integer-predicate (x)
+    (implies (integer? x) (equal? (integer? x) #t)))
+  (define-axiom integer-is-a-real (x)
+    (implies (integer? x) (equal? (number? x) #t)))
+
+  (define-core-function/guard exact? (x) (number? x) exact?)
+  (define-axiom exact-predicate (x)
+    (implies (exact? x) (equal? (exact? x) #t)))
+
+  (define-function/guard inexact? (x)
+    (number? x)
+    (not (exact? x)))
+  (define-theorem inexact-predicate (x)
+    (implies (inexact? x) (equal? (inexact? x) #t)))
+
+  (define-core-function exact-integer? (x) exact-integer?)
+  (define-axiom exact-integer-predicate (x)
+    (implies (exact-integer? x) (equal? (exact-integer? x) #t)))
+  (define-axiom exact-integer-is-a-integer (x)
+    (implies (exact-integer? x) (equal? (integer? x) #t)))
+  (define-axiom exact-integer-is-a-exact (x)
+    (implies (exact-integer? x) (equal? (exact? x) #t)))
+
+  (define-core-function/guard < (x y) (and (real? x) (real? y)) <)
+  (define-axiom less-than-predicate (x y)
+    (implies (< x y) (equal? (< x y) #t)))
+
+  (define-function/guard positive? (x)
+    (real? x)
+    (< 0 x))
+  (define-theorem positive-predicate (x)
+    (implies (positive? x) (equal? (positive? x) #t)))
+  (define-function/guard negative? (x)
+    (real? x)
+    (< x 0))
+  (define-theorem negative-predicate (x)
+    (implies (negative? x) (equal? (negative? x) #t)))
+
+  (define-function exact-positive-integer? (x)
+    (and (exact-integer? x)
+         (positive? x)))
+  (define-theorem exact-positive-integer-predicate (x)
+    (implies (exact-positive-integer? x)
+             (equal? (exact-positive-integer? x) #t)))
+
+  (define-function exact-zero? (x) (equal? x 0))
+  (define-theorem exact-zero-predicate (x)
+    (implies (exact-zero? x) (equal? (exact-zero? x) #t)))
+
   (define-function natural? (x)
-    (if (zero? x)
+    (if (exact-zero? x)
         #t
-        (positive-integer? x)))
-  (define-core-function + (x y)
-    (lambda (x y)
-      (if (number? x)
-          (if (number? y)
-              (+ x y)
-              x)
-          (if (number? y)
-              y
-              0))))
-  (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
-            (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?/true (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/pred (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)
-    (implies (natural? x) (equal? (integer? x) #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)
-            0
-            (succ (natural-induction (pred x))))
-        0))
-  (define-function integer-induction (x)
-    (if (positive-integer? x)
-        (succ (integer-induction (pred x)))
-        (if (negative-integer? x)
-            (pred (integer-induction (succ 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/integer)
-  (define-core-function pair? (x) pair?)
-  (define-core-function cons (x y) cons)
-  (define-core-function car (x)
-    (lambda (x) (if (pair? x) (car x) '())))
-  (define-core-function cdr (x)
-    (lambda (x) (if (pair? x) (cdr x) '()))))
-
-(define-system prelude/tree (prelude/pair)
-  (define-trivial-total-function size (x)
-    (if (pair? x)
-        (+ 1
-           (+ (size (car x))
-              (size (cdr x))))
-        0))
-  (define-axiom natural/size (x)
-    (equal? (natural? (size x)) #t))
-  (define-axiom size/car (x)
-    (equal? (< (size (car x)) (size x)) #t))
-  (define-axiom size/cdr (x)
-    (equal? (< (size (cdr x)) (size x)) #t))
-  (define-function tree-induction (x)
-    (if (not (pair? x))
-        x
-        (cons (tree-induction (car x))
-              (tree-induction (cdr x))))))
-
-(define-system prelude/proofs (prelude/tree)
-  (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 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)))
+        (exact-positive-integer? x)))
+  (define-theorem (predicate natural?) (x)
+    (implies (natural? x) (equal? (natural? x) #t))))
 
-  (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) if-nest)
-     ((3) if-false)
-     (() if-same)))
+(define-system prelude/measure/natural (prelude/number)
+  (set-measure-predicate natural?)
+  (set-measure-predicate <))
 
-  (define-proof zero-is-0
-    (((1) zero?)
-     ((2 1) equal-if)
-     ((2) equal?)
+(define-system prelude (prelude/measure/natural)
+  (define-proof inexact?
+    (((2) if-nest)
      (() 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?)
+  (define-proof inexact-predicate
+    (((1) inexact?)
+     (() if-not)
+     ((3 1) inexact?)
+     ((3 1 1) equal-if-false)
+     ((3) (eval))
      (() 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)
+  (define-proof positive?
+    (((2 1 1) (eval))
+     ((2 1) if-true)
+     ((2) if-nest)
      (() 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)
+  (define-proof positive-predicate
+    (((1) positive?)
+     ((2 1) positive?)
+     ((2 1) less-than-predicate)
+     ((2) (eval))
      (() if-same)))
-
-  (define-proof integer-induction
-    (abs x)
-    (((1) natural/abs)
-     (() if-true)
-     ((2) abs/pred)
-     ((3 2) abs/succ)
-     ((3) if-same)
+  (define-proof negative?
+    (((2 1) if-nest)
+     ((2 1) (eval))
+     ((2) if-true)
      (() if-same)))
-  
-  (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)
-    (((2 3 1) size/car)
-     ((2 3 2) size/cdr)
-     ((2 3) if-true)
-     ((2) if-same)
-     ((1) natural/size)
-     (() if-true))))
-
-
-(define-system prelude (prelude/proofs))
+  (define-proof negative-predicate
+    (((1) negative?)
+     ((2 1) negative?)
+     ((2 1) less-than-predicate)
+     ((2) (eval))
+     (() if-same))))
-- 
cgit v1.2.3