wip35

2 files changed, 60 insertions, 68 deletions

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 35f91dd..d03df7e 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -17,7 +17,7 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa prelude)
-  #:export (implies prelude)
+  #:export (natural? size implies prelude)
   #:use-module (vikalpa))
 
 (define-syntax implies
@@ -27,7 +27,6 @@
      (if x (implies y z rest ...) #t))))
 
 (define-system prelude ()
-  (define-primitive-function pair? (x y))
   (define-primitive-function < (x y))
   (define-primitive-function natural? (x))
   (define-totality-claim natural? natural? <)
@@ -40,14 +39,17 @@
     ((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)
@@ -55,77 +57,68 @@
   
   (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 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 (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)
         (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 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-axiom pair-cons (x y)
+    (equal? (pair? (cons x y)) '#t))
 
-  (define-proof natural-induction
-    (natural? n)
-    ())
+  (define-axiom car-cdr-elim (x)
+    (if (pair? x)
+        (equal? (cons (car x) (cdr x)) x)
+        '#t))
 
-  (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 car-cons (x y)
+    (equal? (car (cons x y)) x))
 
-  (define-axiom natural/zero ()
-    (equal? (natural? '0) '#t))
+  (define-axiom cdr-cons (x y)
+    (equal? (cdr (cons x y)) y))
+  
+  (define-axiom car-cdr-elim (x)
+    (implies (pair? x)
+             (equal? (cons (car x) (cdr x)) x)))
 
-  (define-axiom not/true ()
-    (equal? (not #t) #f))
+  (define-axiom cons-equal-car (x1 y1 x2 y2)
+    (implies (equal? (cons x1 y1) (cons x2 y2))
+             (equal? x1 x2)))
 
-  (define-axiom not/false ()
-    (equal? (not #f) #t))
+  (define-axiom cons-equal-cdr (x1 y1 x2 y2)
+    (implies (equal? (cons x1 y1) (cons x2 y2))
+             (equal? y1 y2)))
+  
+  #;
+  (define-axiom natural?/0 ()
+    (equal? (natural? '0) '#t))
 
+  #;
   (define-theorem equal/zero-less-than (x)
     (implies (natural? x)
              (equal? (not (< '0 x))
                      (equal? x '0))))
 
+  #;
   (define-proof equal/zero-less-than
     (natural-induction x)
     (((2 2) if-nest)
@@ -159,11 +152,11 @@
      ((2) if-same)
      (() if-same)))
   
-  (define-axiom natural/sub1 (x)
-    (implies (natural? x)
-             (if (equal? '0 x)
-                 '#t
-                 (equal? (natural? (sub1 x)) #t))))
+  ;; (define-axiom natural/sub1 (x)
+  ;;   (implies (natural? x)
+  ;;            (if (equal? '0 x)
+  ;;                '#t
+  ;;                (equal? (natural? (sub1 x)) #t))))
   
 ;; (define-proof natural-induction
 ;;     (total/natural? n)
@@ -172,9 +165,9 @@
 ;;      ((2) if-same)
 ;;      (() if-same)))
 
-(define-theorem natural/add1 (x)
-    (implies (natural? x)
-             (equal? (natural? (add1 x)) #t)))
+;; (define-theorem natural/add1 (x)
+;;     (implies (natural? x)
+;;              (equal? (natural? (add1 x)) #t)))
 
   #;
   (define-axiom natural/sub1 (x)
@@ -199,14 +192,14 @@
         '#t))
 
   #;
-  (define-primitive-function + (x y)
+  (define-built-in-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))
@@ -306,4 +299,5 @@
      ((2 1) if-true)
      ((2) equal-same)
      ((1) natural?/0)
-     (() if-true))))
+  (() if-true)))
+  )
diff --git a/vikalpa/the-little-prover.scm b/vikalpa/the-little-prover.scm
index b892f7f..338843b 100644
--- a/vikalpa/the-little-prover.scm
+++ b/vikalpa/the-little-prover.scm
@@ -17,24 +17,22 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa the-little-prover)
-  #:export (atom? the-little-prover)
+  #:export (the-little-prover)
   #:use-module (vikalpa))
 
-(define (atom? x)
-  (not (pair? x)))
-
 (define (size x)
-  (if (atom? x)
-      0
+  (if (pair? x)
       (+ (size (car x))
-         (size (cdr x)))))
+         (size (cdr x)))
+      0))
 
 (define-system the-little-prover ()
-  (define-primitive-function atom? (x))
-  (define-primitive-function size (x))
-  (define-primitive-function + (x y))
-  (define-primitive-function natural? (x))
-  (define-primitive-function < (x y))
+  (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? <)
   
   ;; Axioms of Equal