From 60a1d48a4afdb139caa9936895b3f1833d6a7926 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Wed, 25 Nov 2020 09:29:38 +0900
Subject: wip35

---
 Makefile.am                   |  10 ++--
 tests/test-vikalpa.scm        |  44 ++++++++++++++++++
 vikalpa.scm                   |  58 ++++++++++++++---------
 vikalpa/prelude.scm           | 106 ++++++++++++++++++++----------------------
 vikalpa/the-little-prover.scm |  22 ++++-----
 5 files changed, 146 insertions(+), 94 deletions(-)
 create mode 100644 tests/test-vikalpa.scm

diff --git a/Makefile.am b/Makefile.am
index 33ca8b7..e17dad2 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -41,10 +41,14 @@ godir=$(libdir)/guile/$(GUILE_EFFECTIVE_VERSION)/site-ccache
 
 bin_SCRIPTS =
 
-SOURCES =                \
-  vikalpa.scm
+SOURCES =                       \
+  vikalpa.scm                   \
+  vikalpa/prelude.scm           \
+  vikalpa/the-little-prover.scm
 
-TESTS =
+
+TESTS =                  \
+  tests/test-vikalpa.scm
 
 TEST_EXTENSIONS = .scm
 
diff --git a/tests/test-vikalpa.scm b/tests/test-vikalpa.scm
new file mode 100644
index 0000000..90b776c
--- /dev/null
+++ b/tests/test-vikalpa.scm
@@ -0,0 +1,44 @@
+;;; Vikalpa --- Proof Assistant
+;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
+;;;
+;;; This file is part of Vikalpa.
+;;;
+;;; Vikalpa is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or
+;;; (at your option) any later version.
+;;;
+;;; Vikalpa is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+;;; General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (tests test-the-little-prover)
+  #:use-module (srfi srfi-64)
+  #:use-module (vikalpa)
+  #:use-module (vikalpa the-little-prover))
+
+(test-begin "test-the-little-prover-1")
+
+(test-equal ''ham (rewrite (the-little-prover)
+                           '(car (cons 'ham '(eggs)))
+                           '((() car/cons))))
+
+(test-equal ''#t (rewrite (the-little-prover)
+                          '(atom? '())
+                          '((() atom?)
+                            ((1) pair?)
+                            (() not))))
+
+(test-equal ''#t (rewrite (the-little-prover)
+                          '(atom? '())
+                          '((() atom?)
+                            ((1) pair?)
+                            (() not))))
+
+
+(test-end "test-the-little-prover-1")
+
diff --git a/vikalpa.scm b/vikalpa.scm
index f45a571..671082a 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -280,17 +280,16 @@
         (mat-preconds
          (cdr rlps)
          (let search ((ps preconds))
-           (when (equal? rl '(rule (x y) ((natural? y) (natural? x)) (quote #t) (natural? (+ x y))))
-             (format #t "search~% rl: ~s~% rlps: ~s~% ps: ~s~% env: ~s~%" rl rlps ps (cdr k+env)))
            (if (null? ps)
-               ((car k+env) #f)
+               (shift k ((car k+env) #f))
                (let ((env (mat-begin (car rlps) (car ps) (cdr k+env))))
                  (cond
                   ((mat-begin (car rlps) (car ps) (cdr k+env))
                    => (lambda (env)
                         (shift k0
-                               (reset (or (shift k (k0 (cons k env)))
-                                          (k0 (search (cdr ps))))))))
+                               (reset
+                                (or (shift k (k0 (cons k env)))
+                                    (k0 (search (cdr ps))))))))
                   (else (search (cdr ps))))))))))
   (define (valid? env expr)
     (cond ((expr-quoted? expr) #t)
@@ -847,7 +846,6 @@
      (else
       (fail 'apply-theorem cmd expr)))))
 
-;; (rewrite system? rewriter? expression? procedure?) -> expr
 (define (rewrite1 sys expr fail r)
   (let* ((cmd (rewriter-command r))
          (cmd/name (command-name cmd)))
@@ -861,7 +859,19 @@
            (('equal? `(quote ,x) `(quote ,y))
             (expr-quote (equal? x y)))
            (else
-            (fail 'equal? 'extracted-expr))))
+            (fail 'equal? extracted-expr))))
+        ((eq? 'pair? cmd/name)
+         (match extracted-expr
+           (('pair? `(quote ,x))
+            (expr-quote (pair? x)))
+           (else
+            (fail 'pair? extracted-expr))))
+        ((eq? 'not cmd/name)
+         (match extracted-expr
+           (('not `(quote ,x))
+            (expr-quote (not x)))
+           (else
+            (fail 'not extracted-expr))))
         ((eq? 'error cmd/name) (fail extracted-expr))
         ((and (symbol? cmd/name)
               (lookup cmd/name sys))
@@ -879,21 +889,19 @@
                 (fail 'invalid-command cmd extracted-expr)))))
         (else (fail 'command-not-found cmd extracted-expr)))))))
 
-(define/guard (rewrite (sys system?) (expr expression?) (seq sequence?))
-  (debug "rewrite ~y~%" expr)
-  (let loop ((expr expr)
-             (seq seq))
-    (debug "~y~%" expr)
-    #;(format #t "~y~%" expr)
-    (reset
-     (if (null? seq)
-         expr
-         (loop (rewrite1 sys
-                         expr
-                         (lambda args
-                           (shift k (cons 'error args)))
-                         (car seq))
-               (cdr seq))))))
+(define/guard (rewrite (sys system?) (expr (const #t)) (seq sequence?))
+  (let ((expr (convert-to-expression expr)))
+    (let loop ((expr expr)
+               (seq seq))
+      (reset
+       (if (null? seq)
+           expr
+           (loop (rewrite1 sys
+                           expr
+                           (lambda args
+                             (shift k (cons 'error args)))
+                           (car seq))
+                 (cdr seq)))))))
 
 (define (expr-not x)
   (list 'not x))
@@ -928,7 +936,10 @@
               (expression->rules vars
                                  (cons (prop-not (if-form-test expr))
                                        preconds)
-                                 (if-form-else expr)))
+                                 (if-form-else expr))
+              (expression->rules vars
+                                 preconds
+                                 (if-form-test expr)))
       (if (expr-equal? expr)
           (list (rule vars
                       preconds
@@ -1063,6 +1074,7 @@
   (parameterize ((current-system parent))
     (define-primitive-function not (x))
     (define-primitive-function equal? (x y))
+    (define-primitive-function pair? (x y))
     (define-primitive-function cons (x y))
     (define-primitive-function car (x))
     (define-primitive-function cdr (x))
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
-- 
cgit v1.2.3