1 files changed, 171 insertions, 0 deletions
diff --git a/vikalpa/the-little-prover.scm b/vikalpa/the-little-prover.scm
new file mode 100644
index 0000000..5f70f24
--- /dev/null
+++ b/vikalpa/the-little-prover.scm
@@ -0,0 +1,171 @@
+;;; Vikalpa --- Proof Assistant
+;;; Copyright © 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 (vikalpa the-little-prover)
+  #:export (prelude)
+  #:use-module (vikalpa))
+
+(define (bool->t-nil x)
+  (if x
+      't
+      'nil))
+
+(define (size x)
+  (if (pair? x)
+      (+ (size (car x))
+         (size (cdr x)))
+      1))
+
+(define-system axioms-of-equal (core-system/equal-t-nil)
+  (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)))
+
+(define-system axioms-of-cons (axioms-of-equal)
+  (define-core-function atom (x) (lambda (x) (bool->t-nil (not (pair? x)))))
+  (define-core-function cons (x y) cons)
+  (define-core-function car (x) (lambda (x) (if (not (pair? x)) '() (car x))))
+  (define-core-function cdr (x) (lambda (x) (if (not (pair? x)) '() (cdr x))))
+
+  (define-axiom atom/cons (x y)
+    (equal (atom (cons x y)) 'nil))
+  (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))))
+
+(define-system axioms-of-if (axioms-of-cons)
+  (define-axiom if-true (x y)
+    (equal (if 't x y) x))
+  (define-axiom if-false (x y)
+    (equal (if 'nil 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))))
+
+(define-system definitions-of-measure (axioms-of-if)
+  (define-core-function natp (x)
+    (lambda (x)
+      (bool->t-nil
+       (and (exact-integer? x)
+            (<= 0 x)))))
+  (set-measure-predicate natp)
+
+  (define-core-function < (x y)
+    (lambda (x y)
+      (bool->t-nil
+       (and (exact-integer? x)
+            (exact-integer? y)
+            (< x y)))))
+  (set-measure-less-than <))
+
+(define-system axioms-of-size (definitions-of-measure)
+  (define-core-function + (x y)
+    (lambda (x y)
+      (if (and (exact-integer? x)
+               (exact-integer? y))
+          (+ x y)
+          0)))
+  (define-core-function size (x) size)
+
+  (define-axiom natp/size (x)
+    (equal (natp (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))))
+
+(define-system axioms-of-+-and-< (axioms-of-size)
+  (define-axiom identity-+ (x)
+    (if (natp x)
+        (equal (+ 0 x) x)
+        '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 positives-+ (x y)
+    (if (< 0 x)
+        (if (< 0 x)
+            (equal (< 0 (+ x y)) 't)
+            't)
+        't))
+  (define-axiom natp/+ (x y)
+    (if (natp x)
+        (if (natp y)
+            (equal (natp (+ x y)) 't)
+            't)
+        't))
+  (define-axiom common-addends-< (x y z)
+    (equal (< (+ x z) (+ y z))
+           (< x y))))
+
+(define-system inductions (axioms-of-+-and-<)
+  (define-function list-induction (x)
+    (if (atom x)
+        't
+        (list-induction (cdr x))))
+
+  (define-function star-induction (x)
+    (if (atom x)
+        't
+        (cons (star-induction (car x))
+              (star-induction (cdr x)))))
+
+  (define-proof list-induction
+    (size x)
+    ((rewrite (1) natp/size)
+     (rewrite () if-true)
+     (rewrite (3) size/cdr)
+     (rewrite () if-same)))
+
+  (define-proof star-induction
+    (size x)
+     ((rewrite (1) natp/size)
+      (rewrite () if-true)
+      (rewrite (3 1) size/car)
+      (rewrite (3 2) size/cdr)
+      (eval (3))
+      (rewrite () if-same))))
+
+(define-system prelude (inductions))