From 35c4714a8cc38b2a8106b54b87684483b5a94f62 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 18 Dec 2020 09:41:23 +0900
Subject: wip58

---
 vikalpa/prelude.scm           | 220 ++++++++++++++++++++++++------------------
 vikalpa/the-little-prover.scm | 104 ++++++++++++--------
 2 files changed, 189 insertions(+), 135 deletions(-)

(limited to 'vikalpa')

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index bd8b409..125c8d6 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -20,140 +20,170 @@
   #:export (prelude)
   #:use-module (vikalpa))
 
-(define-system prelude ()
-  (define-core-function natural? (x) (lambda (x)
-                                       (and (integer? x)
-                                            (< 0 x))))
-  (define-core-function < (x y) (natural? x) (natural? y) <)
-  (define-core-function pair? (x) pair?)
-  (define-core-function cons (x y) cons)
-  (define-core-function car (x) (pair? x)
-    (lambda (x) (if (pair? x) (car x) '())))
-  (define-core-function cdr (x) (pair? x)
-    (lambda (x) (if (pair? x) (cdr x) '())))
-  (define-core-function + (x y)
-    (lambda (x y)
-      (if (number? x)
-          (if (number? y)
-              (+ x y)
-              x)
-          (if (number? y)
-              y
-              0))))
-  (set-measure-predicate natural?)
-  (set-measure-less-than <)
-  (define-trivial-total-function list-induction (x)
-    (if (not (pair? x))
-        x
-        (cons (car x)
-              (list-induction (cdr x)))))
-  (define-trivial-total-function size (x)
-    (if (not (pair? x))
-        0
-        (+ 1
-           (+ (size (car x))
-              (size (cdr x))))))
-
+(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-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-syntax-rules cond (else)
     ((cond (else e)) e)
     ((cond (test then) . rest)
      (if test then (cond . rest))))
-
   (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-system prelude/equal (prelude/macros)
+  (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-system prelude/if (prelude/equal)
   (define-axiom if-nest (x y z)
     (if x
         (equal? (if x y z) y)
         (equal? (if x y z) z)))
-
   (define-axiom if-true (x y)
     (equal? (if '#t x y) x))
-
   (define-axiom if-false (x y)
     (equal? (if '#f x y) y))
-
   (define-axiom if-same (x y)
     (equal? (if x y y) y))
-
   (define-axiom if-not (x y z)
     (equal? (if (not x) y z)
-            (if x z y)))
-
-  (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 pair/cons (x y)
-    (equal? (pair? (cons x y)) '#t))
-
-  (define-axiom cons/car+cdr (x)
-    (implies (pair? x)
-             (equal? (cons (car x) (cdr x)) x)))
+            (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-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)
+            #t
+            (equal? (< x y) (< x 0)))
+        (if (rational? y)
+            (equal? (< x y) (< 0 y))
+            (equal? (< x y) #f))))
+  (define-function natural? (x)
+    (if (integer? 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-axiom car/cons (x y)
-    (equal? (car (cons x y)) x))
+(define-system prelude/measure (prelude/number)
+  (set-measure-predicate natural?)
+  (set-measure-less-than <))
 
-  (define-axiom cdr/cons (x y)
-    (equal? (cdr (cons x y)) y))
+(define-system prelude/pair (prelude/measure)
+  (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-axiom equal-car (x1 y1 x2 y2)
-    (implies (equal? (cons x1 y1) (cons x2 y2))
-             (equal? x1 x2)))
-
-  (define-theorem caar-cons2 (x y z)
-    (equal? (car (car (cons (cons x y) z))) x))
-  
-  (define-function app (x y)
+  (define-function tree-induction (x)
     (if (not (pair? x))
-        y
-        (cons (car x)
-              (app (cdr x) y))))
+        x
+        (cons (tree-induction (car x))
+              (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-is-integer
+    ((() if-same (set x (integer? x)))
+     ((2 2 1) if-nest)
+     ((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/is natural-is-number
+    rational?
+    rational-is-number
+    natural-is-rational)
   
-  (define-theorem assoc-app (x y z)
-    (equal? (app x (app y z))
-            (app (app x y) z)))
-
-  (define-proof caar-cons2
-    (((1 1)  car/cons)
-     ((1) car/cons)
-     (() equal-same)))
-
-  (define-proof app
+  (define-proof tree-induction
     (size x)
-    (((2 3) size/cdr)
+    (((2 3 1) size/car)
+     ((2 3 2) size/cdr)
+     ((2 3) if-true)
      ((2) if-same)
      ((1) natural/size)
-     (() if-true)))
-
-  (define-proof assoc-app
-    (list-induction x)
-    ()))
-
+     (() if-true))))
 
+(define-system prelude (prelude/proofs))
diff --git a/vikalpa/the-little-prover.scm b/vikalpa/the-little-prover.scm
index 338843b..fe7735e 100644
--- a/vikalpa/the-little-prover.scm
+++ b/vikalpa/the-little-prover.scm
@@ -17,24 +17,53 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa the-little-prover)
-  #:export (the-little-prover)
+  #:export (atom? nat? the-little-prover)
   #:use-module (vikalpa))
 
-(define (size x)
-  (if (pair? x)
-      (+ (size (car x))
-         (size (cdr x)))
-      0))
+(define (atom? x)
+  (not (pair? x)))
+
+(define (nat? x)
+  (and (integer? x)
+       (<= 0 x)))
 
 (define-system the-little-prover ()
-  (define-function atom? (x)
-    (not (pair? x)))
-  (define-builtin-function size (x))
-  (define-builtin-function + (x y))
-  (define-builtin-function natural? (x))
-  (define-builtin-function < (x y))
-  (define-totality-claim natural? natural? <)
-  
+  (define-core-function atom? (x) atom?)
+  (define-core-function nat? (x) nat?)
+  (define-core-function < (x y)
+    (lambda (x y)
+      (if (number? x)
+          (if (number? y)
+              (< x y)
+              (< x 0))
+          (if (number? y)
+              (< 0 y)
+              #f))))
+  (set-measure-predicate nat?)
+  (set-measure-less-than <)
+  (define-core-function + (x y)
+    (lambda (x y)
+      (if (number? x)
+          (if (number? y)
+              (+ x y)
+              x)
+          (if (number? y)
+              y
+              0))))
+  (define-core-function cons (x y) cons)
+  (define-core-function car (x)
+    (lambda (x)
+      (if (atom? x) '() (car x))))
+  (define-core-function cdr (x)
+    (lambda (x)
+      (if (atom? x) '() (cdr x))))
+  (define-trivial-total-function size (x)
+    (if (atom? x)
+        0
+        (+ 1
+           (+ (size (car x))
+              (size (cdr x))))))
+
   ;; Axioms of Equal
   (define-axiom equal-same (x)
     (equal? (equal? x x) #t))
@@ -68,8 +97,8 @@
     (if x #t (equal? (if x y z) z)))
 
   ;; Axioms of Size
-  (define-axiom natural?/size (x)
-    (equal? (natural? (size x)) #t))
+  (define-axiom nat/size (x)
+    (equal? (nat? (size x)) #t))
   (define-axiom size/car (x)
     (if (atom? x)
         #t
@@ -81,8 +110,8 @@
 
   ;; Axioms of `+` and `<`
   (define-axiom identity-+ (x)
-    (if (natural? x)
-        (equal? (+ (+ x y) z))
+    (if (nat? x)
+        (equal? (+ 0 x) x)
         #t))
   (define-axiom commute-+ (x y)
     (equal? (+ x y) (+ y x)))
@@ -94,23 +123,16 @@
             (equal? (< '0 (+ x y)) #t)
             #t)
         #t))
-  (define-axiom natural?/+ (x y)
-    (if (natural? x)
-        (if (natural? y)
-            (equal? (natural? (+ x y)) #t)
+  (define-axiom nat/+ (x y)
+    (if (nat? x)
+        (if (nat? y)
+            (equal? (nat? (+ x y)) #t)
             #t)
         #t))
   (define-axiom common-addends-< (x y z)
-    (equal? (< (+ x z) (+ y z) (< x y))))
-
-  ;; Axioms for Vikalpa
-  (define-axiom natural?/0 ()
-    (equal? (natural? '0) #t))
-  (define-axiom natural?/succ (x)
-    (if (natural? x)
-        (equal? (natural? (succ x)) #t)
-        #t))
-
+    (equal? (< (+ x z) (+ y z))
+            (< x y)))
+  
   ;; Prelude
   (define-function list-induction (x)
     (if (atom? x)
@@ -118,22 +140,24 @@
         (cons (car x)
               (list-induction (cdr x)))))
 
-  (define-proof list-induction
-    (natural? (size x))
-    (((2 3) size/cdr)
-     ((2) if-same)
-     (() if-same)))
-  
   (define-function star-induction (x)
     (if (atom? x)
         x
         (cons (star-induction (car x))
               (star-induction (cdr x)))))
 
+  (define-proof list-induction
+    (size x)
+    (((2 3) size/cdr)
+     ((2) if-same)
+     ((1) nat/size)
+     (() if-true)))
+
   (define-proof star-induction
-    (natural? (size x))
+    (size x)
     (((2 3 1) size/car)
      ((2 3 2) size/cdr)
      ((2 3) if-true)
      ((2) if-same)
-     (() if-same))))
+     ((1) nat/size)
+     (() if-true))))
-- 
cgit v1.2.3