1 files changed, 421 insertions, 0 deletions
diff --git a/tests/test-vikalpa.scm b/tests/test-vikalpa.scm
new file mode 100644
index 0000000..91e11f6
--- /dev/null
+++ b/tests/test-vikalpa.scm
@@ -0,0 +1,421 @@
+;;; Vikalpa --- Proof Assistant
+;;; Copyright © 2020, 2021 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 vikalpa)
+  #:use-module (srfi srfi-64)
+  #:use-module (vikalpa))
+
+(define-system test/defs ()
+  (define-syntax-rules implies ()
+    ((implies x y) (if x y #t))
+    ((implies x y z . rest)
+     (if x (implies y z . rest) #t)))
+  (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 equal-if-false (x y)
+    (if x #t (equal? x #f)))
+  (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-core-function/guard + (x y)
+    (and (natural? x) (natural? y))
+    +)
+  (define-core-function natural? (x)
+    (lambda (x)
+      (and (exact-integer? x)
+           (<= 0 x))))
+  (define-core-function/guard < (x y)
+    (and (natural? x) (natural? y))
+    <)
+  (set-measure-predicate natural?)
+  (set-measure-less-than <)
+  (define-core-function pair? (x) pair?)
+  (define-core-function cons (x y) cons)
+  (define-core-function/guard car (x) (pair? x) car)
+  (define-core-function/guard cdr (x) (pair? x) cdr)
+  (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 (pair? cons) (x y)
+    (equal? (pair? (cons x y)) #t))
+  (define-axiom (eliminate cons) (x)
+    (implies (pair? x)
+             (equal? (cons (car x) (cdr x)) x)))
+  (define-axiom (predicate pair?) (x)
+    (implies (pair? x) (equal? (pair? x) #t)))
+
+  (define-function size (x)
+    (if (pair? x)
+        (+ (size (car x))
+           (size (cdr x)))
+        1))
+  (admit size)
+  (define-axiom (natural? size) (x)
+    (equal? (natural? (size x)) #t))
+  (define-axiom (< size car) (x)
+    (implies (natural? x)
+             (equal? (< (size (car x)) (size x)) #t)))
+  (define-axiom (< size cdr) (x)
+    (implies (pair? x)
+             (equal? (< (size (cdr x)) (size x)) #t)))
+  (define-guard-theorem size)
+
+  (define-function null? (x)
+    (equal? x '()))
+  (define-theorem (predicate null?) (x)
+    (implies (null? x) (equal? (null? x) #t)))
+  (define-theorem (substitute null?) (x)
+    (implies (null? x) (equal? x '())))
+
+  (define-function cdr-induction (x)
+    (if (pair? x)
+        (cons (car x) (cdr-induction (cdr x)))
+        '()))
+  (define-guard-theorem cdr-induction)
+
+  (define-function list? (x)
+    (if (null? x)
+        #t
+        (if (pair? x)
+            (list? (cdr x))
+            #f)))
+  (define-guard-theorem list?)
+
+  (define-theorem (predicate list?) (x)
+    (implies (list? x) (equal? (list? x) #t)))
+  (define-theorem (is null? list?) (x)
+    (implies (null? x) (equal? (list? x) #t)))
+  (define-theorem (is pair? (o list? cdr) list?) (x)
+    (implies (pair? x)
+             (list? (cdr x))
+             (equal? (list? x) #t)))
+  (define-theorem (is list? (o not null?) pair?) (x)
+    (implies (list? x)
+             (not (null? x))
+             (equal? (pair? x) #t)))
+
+  (define-theorem (is-not pair? null?) (x)
+    (implies (pair? x)
+             (equal? (null? x) #f)))
+
+  (define-theorem (is list? pair? (o list? cdr)) (x)
+    (implies (list? x)
+             (pair? x)
+             (equal? (list? (cdr x)) #t)))
+
+  (define-theorem (is list? (o not pair?) null?) (x)
+    (implies (list? x)
+             (not (pair? x))
+             (equal? (null? x) #t)))
+
+  (define-function/guard append (x y)
+    (and (list? x) (list? y))
+    (if (null? x)
+        y
+        (cons (car x) (append (cdr x) y))))
+  (define-guard-theorem append)
+
+  (define-theorem (substitute (append null? _)) (x)
+    (equal? (append '() x) x))
+
+  (define-theorem (associative append) (x y z)
+    (implies (list? x)
+             (list? y)
+             (list? z)
+             (equal? (append (append x y) z)
+                     (append x (append y z))))))
+
+(define-system test/proofs (test/defs)
+  (define-proof (predicate null?)
+    ((rewrite (1) null?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2 1))
+     (rewrite (2) equal-same)
+     (rewrite () if-same)))
+
+  (define-proof (guard size)
+    ((rewrite (2 1) (natural? size))
+     (rewrite (2 2 1) (natural? size))
+     (rewrite (2 2 2 1) (predicate pair?))
+     (rewrite (2 2 2 2) (predicate pair?))
+     (eval (2))
+     (rewrite () if-same)))
+
+  (define-proof (guard cdr-induction)
+    ((rewrite (2) if-nest)
+     (rewrite (2) (predicate pair?))
+     (rewrite () if-same)))
+
+  (define-proof list?
+    (size x)
+    ((rewrite (1) (natural? size))
+     (rewrite () if-true)
+     (rewrite (3 2) (< size cdr))
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (guard list?)
+    ((rewrite (3 2) (predicate pair?))
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (substitute null?)
+    ((rewrite (1) null?)
+     (rewrite (2 1) equal-if)
+     (eval (2))
+     (rewrite () if-same)))
+
+  (define-proof (predicate list?)
+    (cdr-induction x)
+    ((rewrite (2) if-same (set x (list? (cdr x))))
+     (rewrite (2 2 1) if-nest)
+     (rewrite (2 2 2 2 1) list?)
+     (rewrite (2 2 2 2 1 3 2) equal-if)
+     (rewrite (2 2 2 2 1 3) if-nest)
+     (rewrite (2 2 2 2 1) if-same)
+     (rewrite (2 2 2 2) equal-same)
+     (rewrite (2 2 2) if-same)
+     (rewrite (2 2) if-same)
+     (rewrite (2 3 1) if-nest)
+     (rewrite (2 3) if-true)
+     (rewrite (2 3 1) list?)
+     (rewrite (2 3 1 3) if-nest)
+     (rewrite (2 3) if-same (set x (null? x)))
+     (rewrite (2 3 2 1) if-nest)
+     (rewrite (2 3 2) if-true)
+     (rewrite (2 3 2 1 1) (substitute null?))
+     (eval (2 3 2))
+     (rewrite (2 3 3 1) if-nest)
+     (rewrite (2 3 3) if-nest)
+     (rewrite (2 3) if-same)
+     (rewrite (2) if-same)
+     (rewrite (3 1) list?)
+     (rewrite (3) if-same (set x (null? x)))
+     (rewrite (3 2 1) if-nest)
+     (rewrite (3 2) if-true)
+     (rewrite (3 2 1 1) (substitute null?))
+     (eval (3 2))
+     (rewrite (3 3 1) if-nest)
+     (rewrite (3 3 1) if-nest)
+     (rewrite (3 3) if-false)
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (is null? list?)
+    ((rewrite (1) null?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2))
+     (rewrite () if-same)))
+
+  (define-proof (is pair? (o list? cdr) list?)
+    ((rewrite (2 2 1) list?)
+     (rewrite (2 2 1 3 2) (predicate list?))
+     (rewrite (2 2 1 3) if-nest)
+     (rewrite (2 2 1) if-same)
+     (rewrite (2 2) equal-same)
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+
+  (define-proof cdr-induction
+    (size x)
+    ((rewrite (1) (natural? size))
+     (rewrite () if-true)
+     (rewrite (2) (< size cdr))
+     (rewrite () if-same)))
+
+  (define-proof (is list? (o not null?) pair?)
+    ((rewrite (2) if-not)
+     (rewrite (1) list?)
+     (rewrite () if-same (set x (null? x)))
+     (rewrite (2 1) if-nest)
+     (rewrite (2) if-true)
+     (rewrite (2) if-nest)
+     (rewrite (3 1) if-nest)
+     (rewrite (3) if-same (set x (pair? x)))
+     (rewrite (3 2 1) if-nest)
+     (rewrite (3 2 2 3 1) (predicate pair?))
+     (rewrite (3 2 2 3) equal-same)
+     (rewrite (3 2 2) if-same)
+     (rewrite (3 2) if-same)
+     (rewrite (3 3 1) if-nest)
+     (rewrite (3 3) if-false)
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (is-not pair? null?)
+    ((rewrite () if-same (set x (null? x)))
+     (rewrite (2 1 1) (substitute null?))
+     (eval (2 1))
+     (rewrite (2) if-false)
+     (rewrite (3 2 1) equal-if-false)
+     (rewrite (3 2) equal-same)
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (is list? pair? (o list? cdr))
+    ((rewrite () if-same (set x (pair? x)))
+     (rewrite (2 2) if-nest)
+     (rewrite (3 2) if-nest)
+     (rewrite (3) if-same)
+     (rewrite (2 1) list?)
+     (rewrite (2 1 1) (is-not pair? null?))
+     (rewrite (2 1) if-false)
+     (rewrite (2 1) if-nest)
+     (rewrite (2 2 1) (predicate list?))
+     (eval (2 2))
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+
+  (define-proof append
+    (size x)
+    ((rewrite (2 2 1) (natural? size))
+     (rewrite (2 2) if-true)
+     (rewrite (2 2 3) if-same (set x (pair? x)))
+     (rewrite (2 2 3 2) (< size cdr))
+     (rewrite (2 2 3 1) (is list? (o not null?) pair?))
+     (rewrite (2 2 3) if-true)
+     (rewrite (2 2) if-same)
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (guard append)
+    ((rewrite (2 2 3 2 2 2) (predicate pair?))
+     (rewrite (2 2 3 2 2) if-nest)
+     (rewrite (2 2 3 2 1) (is list? pair? (o list? cdr)))
+     (rewrite (2 2 3 2) if-true)
+     (rewrite (2 2 3 1) (is list? (o not null?) pair?))
+     (rewrite (2 2 3) if-true)
+     (rewrite (2 2) if-same)
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (is list? (o not pair?) null?)
+    ((rewrite (2) if-not)
+     (rewrite () if-same (set x (pair? x)))
+     (rewrite (2 2) if-nest)
+     (rewrite (2) if-same)
+     (rewrite (3 2) if-nest)
+     (rewrite (3 1) list?)
+     (rewrite (3) if-same (set x (null? x)))
+     (rewrite (3 2 1) if-nest)
+     (rewrite (3 2) if-true)
+     (rewrite (3 2 1) (predicate null?))
+     (eval (3 2))
+     (rewrite (3 3 1) if-nest)
+     (rewrite (3 3 1) if-nest)
+     (rewrite (3 3) if-false)
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (substitute (append null? _))
+    ((rewrite (1) append)
+     (eval (1 1))
+     (rewrite (1) if-true)
+     (rewrite () equal-same)))
+
+  (define-proof (associative append)
+    (cdr-induction x)
+    ((rewrite (3 2 2 2) if-same (set x (null? x)))
+     (rewrite (3 2 2 2 2 1 1 1) (substitute null?))
+     (rewrite (3 2 2 2 2 2 1) (substitute null?))
+     (rewrite (3 2 2 2 1) (is list? (o not pair?) null?))
+     (rewrite (3 2 2 2) if-true)
+     (rewrite (3 2 2 2 1 1) (substitute (append null? _)))
+     (rewrite (3 2 2 2 2) (substitute (append null? _)))
+     (rewrite (3 2 2 2) equal-same)
+     (rewrite (3 2 2) if-same)
+     (rewrite (3 2) if-same)
+     (rewrite (3) if-same)
+     (rewrite (2) if-same (set x (list? y)))
+     (rewrite (2 2 1 2) if-nest)
+     (rewrite (2 2 2 2) if-nest)
+     (rewrite (2 3 1 2) if-nest)
+     (rewrite (2 3 2 2) if-nest)
+     (rewrite (2 3 1) if-same)
+     (rewrite (2 3) if-true)
+     (rewrite (2 3) if-same)
+     (rewrite (2 2) if-same (set x (list? z)))
+     (rewrite (2 2 2 1 2) if-nest)
+     (rewrite (2 2 2 2 2) if-nest)
+     (rewrite (2 2 3 1 2) if-nest)
+     (rewrite (2 2 3 2 2) if-nest)
+     (rewrite (2 2 3 1) if-same)
+     (rewrite (2 2 3) if-true)
+     (rewrite (2 2 3) if-same)
+     (rewrite (2 2 2) if-same (set x (list? (cdr x))))
+     (rewrite (2 2 2 2 1) if-nest)
+     (rewrite (2 2 2 3 1) if-nest)
+     (rewrite (2 2 2 3) if-true)
+     (rewrite (2 2 2 2 2 2 2) append)
+     (rewrite (2 2 2 2 2 2 2 1) (is-not pair? null?))
+     (rewrite (2 2 2 2 2 2 2) if-false)
+     (rewrite (2 2 2 2 2 2 2 2) equal-if)
+     (rewrite (2 2 2 2 2 2 1 1) append)
+     (rewrite (2 2 2 2 2 2 1 1 1) (is-not pair? null?))
+     (rewrite (2 2 2 2 2 2 1 1) if-false)
+     (rewrite (2 2 2 2 2 2 1) append)
+     (rewrite (2 2 2 2 2 2 1) if-same
+              (set x (pair? (cons (car x) (append (cdr x) y)))))
+     (rewrite (2 2 2 2 2 2 1 2 1) (is-not pair? null?))
+     (rewrite (2 2 2 2 2 2 1 1) (pair? cons))
+     (rewrite (2 2 2 2 2 2 1) if-true)
+     (rewrite (2 2 2 2 2 2 1) if-false)
+     (rewrite (2 2 2 2 2 2 1 1) (car cons))
+     (rewrite (2 2 2 2 2 2 1 2 1) (cdr cons))
+     (rewrite (2 2 2 2 2 2) equal-same)
+     (rewrite (2 2 2 2 2) if-same)
+     (rewrite (2 2 2 2) if-same)
+     (rewrite (2 2 2) if-same (set x (list? x)))
+     (rewrite (2 2 2 2 1) (is list? pair? (o list? cdr)))
+     (rewrite (2 2 2 2) if-true)
+     (rewrite (2 2 2 3 3) if-nest)
+     (rewrite (2 2 2 3) if-same)
+     (rewrite (2 2 2) if-same)
+     (rewrite (2 2) if-same)
+     (rewrite (2) if-same)
+     (rewrite () if-same))))
+
+(define-system test (test/proofs))
+
+(test-begin "test-vikalpa")
+
+(test-equal '(result/expr b)
+  (system-rewrite (test)
+                  '(car (cdr (cons a (cons b c))))
+                  '((rewrite (1) (cdr cons))
+                    (rewrite () (car cons)))))
+
+(test-equal '()
+  (system-check (test)))
+
+(test-end "test-vikalpa")