wip31

3 files changed, 158 insertions, 18 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index f4ef953..5be2824 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -324,7 +324,7 @@
        (eq? 'system (list-ref x 0))
        (system-definitions? (system-definitions x))
        (system-proofs? (system-proofs x))
-       ((const #t) (system-totality-claims x))))
+       ((const #t) (system-totality-claim-list x))))
 
 (define (make-system defs prfs totality-claims)
   (list 'system defs prfs totality-claims))
@@ -335,7 +335,7 @@
 (define (system-proofs sys)
   (list-ref sys 2))
 
-(define/guard (system-totality-claims (sys system?))
+(define (system-totality-claim-list sys)
   (list-ref sys 3))
 
 (define (totality-claim id nat? less-than)
@@ -628,7 +628,7 @@
   (- x 1))
 
 (define (natural->expr n)
-  (if (zero? n)
+  (if (<= n 0)
       ''0
       `(succ ,(natural->expr (pred n)))))
 
@@ -946,12 +946,12 @@
      (cond ((lookup (definition-name x) sys)
             => (lambda (d)
                  (if (equal? x d)
-                     x
+                     sys
                      (error "(vikalpa) add-definition: duplicated"
                             (definition-name d)))))
            (else (make-system (cons x (system-definitions sys))
                               (system-proofs sys)
-                              (system-totality-claims sys)))))
+                              (system-totality-claim-list sys)))))
     x))
 
 (define (add-proof x)
@@ -964,7 +964,7 @@
                      (error "add-proof: duplicated"))))
            (else (make-system (system-definitions sys)
                               (cons x (system-proofs sys))
-                              (system-totality-claims sys)))))
+                              (system-totality-claim-list sys)))))
     x))
 
 (define reserved-symbols '(quote let if error))
@@ -1026,7 +1026,7 @@
        m))))
 
 (define (find-totality-claim name sys)
-  (assoc name (system-totality-claims sys)))
+  (assoc name (system-totality-claim-list sys)))
 
 (define (add-totality-claim tc)
   (let ((sys (current-system)))
@@ -1047,14 +1047,13 @@
     (current-system
      (make-system (system-definitions sys)
                   (system-proofs sys)
-                  (cons tc (system-totality-claims sys))))
-    tc))
+                  (cons tc (system-totality-claim-list sys))))))
 
 (define-syntax-rule (define-totality-claim name nat? <)
   (add-totality-claim (totality-claim 'name 'nat? '<)))
 
 (define* (core-system #:optional (parent (make-system '() '() '())))
-  (parameterize ([current-system parent])
+  (parameterize ((current-system parent))
     (define-primitive-function not (x))
     (define-primitive-function equal? (x y))
     (define-primitive-function cons (x y))
@@ -1068,8 +1067,8 @@
   (syntax-rules ()
     ((_ name (systems ...) expr ...)
      (define* (name #:optional (parent (make-system '() '() '())))
-       (parameterize ([current-system
-                       ((compose systems ... core-system) parent)])
+       (parameterize ((current-system
+                       ((compose systems ... core-system) parent)))
          expr
          ...
          (unless (system? (current-system))
@@ -1342,7 +1341,7 @@
       (define* (next #:optional fail)
         (loop (make-system (cdr defs)
                            (system-proofs sys)
-                           (system-totality-claims sys))
+                           (system-totality-claim-list sys))
               (if fail
                   (cons fail fails)
                   fails)))
@@ -1428,3 +1427,6 @@
   (map macro-name
        (filter macro?
                (system-definitions sys))))
+
+(define/guard (system-totality-claims (sys system?))
+  (system-totality-claim-list sys))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index c55ea48..35f91dd 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -28,11 +28,6 @@
 
 (define-system prelude ()
   (define-primitive-function pair? (x y))
-  (define-primitive-function cons (x y))
-  (define-primitive-function car (x))
-  (define-primitive-function cdr (x))
-  (define-primitive-function sub1 (x))
-  (define-primitive-function add1 (x))
   (define-primitive-function < (x y))
   (define-primitive-function natural? (x))
   (define-totality-claim natural? natural? <)
@@ -40,6 +35,7 @@
   (define-syntax-rules list ()
     ((list) '())
     ((list x . y) (cons x (list . y))))
+
   (define-syntax-rules and ()
     ((and) '#t)
     ((and x) x)
diff --git a/vikalpa/the-little-prover.scm b/vikalpa/the-little-prover.scm
new file mode 100644
index 0000000..fd71082
--- /dev/null
+++ b/vikalpa/the-little-prover.scm
@@ -0,0 +1,142 @@
+;;; 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 (vikalpa the-little-prover)
+  #:export (atom? the-little-prover)
+  #:use-module (vikalpa))
+
+(define (atom? x)
+  (not (pair? x)))
+
+(define (size x)
+  (if (atom? x)
+      0
+      (+ (size (car x))
+         (size (cdr x)))))
+
+(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-totality-claim natural? natural? <)
+  
+  ;; Axioms of Equal
+  (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)
+    (if (equal? x y) (equal? x y) #t))
+
+  ;; Axioms of Cons
+  (define-axiom atom/cons (x y)
+    (equal? (atom? (cons x y)) #f))
+  (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 (atom? x)
+        #t
+        (equal? (cons (car x) (cdr x)) x)))
+
+  ;; Axioms of If
+  (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-nest-A (x y z)
+    (if x (equal? (if x y z) y) #t))
+  (define-axiom if-nest-E (x y z)
+    (if x #t (equal? (if x y z) z)))
+
+  ;; Axioms of Size
+  (define-axiom natural?/size (x)
+    (equal? (natural? (size x)) #t))
+  (define-axiom size/car (x)
+    (if (atom? x)
+        #t
+        (equal? (< (size (car x)) (size x)) #t)))
+  (define-axiom size/cdr (x)
+    (if (atom? x)
+        #t
+        (equal? (< (size (cdr x)) (size x)) #t)))
+
+  ;; Axioms of `+` and `<`
+  (define-axiom identity-+ (x)
+    (if (natural? x)
+        (equal? (+ (+ x y) z))
+        #t))
+  (define-axiom commute-+ (x y)
+    (equal? (+ x y) (+ y x)))
+  (define-axiom associate-+ (x y z)
+    (equal? (+ (+ x y) z) (+ x (+ y z))))
+  (define-axiom positive-+ (x y)
+    (if (< '0 x)
+        (if (< '0 y)
+            (equal? (< '0 (+ x y)) #t)
+            #t)
+        #t))
+  (define-axiom natural?/+ (x y)
+    (if (natural? x)
+        (if (natural? y)
+            (equal? (natural? (+ 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))
+  
+
+  ;; Prelude
+  (define-function list-induction (x)
+    (if (atom? x)
+        x
+        (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 star-induction
+    (natural? (size x))
+    (((2 3 1) size/car)
+     ((2 3 2) size/cdr)
+     ((2 3) if-true)
+     ((2) if-same)
+     (() if-same))))