wipdevelop

10 files changed, 2100 insertions, 51 deletions

diff --git a/Makefile.am b/Makefile.am
index 921ba1e..e17dad2 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -1,20 +1,20 @@
-## Rabbit Prover --- Prove S-expression
+## Vikalpa --- Proof Assistant
 ## Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
 ##
-## This file is part of Rabbit Prover.
+## This file is part of Vikalpa.
 ##
-## Rabbit Prover is free software; you can redistribute it and/or modify it
+## 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.
 ##
-## Rabbit Prover is distributed in the hope that it will be useful, but
+## 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 Rabbit Prover.  If not, see <http://www.gnu.org/licenses/>.
+## along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 GOBJECTS = $(SOURCES:%.scm=%.go)
 
@@ -41,10 +41,14 @@ godir=$(libdir)/guile/$(GUILE_EFFECTIVE_VERSION)/site-ccache
 
 bin_SCRIPTS =
 
-SOURCES =                \
-  rabbit-prover.scm
+SOURCES =                       \
+  vikalpa.scm                   \
+  vikalpa/prelude.scm           \
+  vikalpa/the-little-prover.scm
 
-TESTS =
+
+TESTS =                  \
+  tests/test-vikalpa.scm
 
 TEST_EXTENSIONS = .scm
 
diff --git a/README.org b/README.org
index 6b33a7f..96d66fb 100644
--- a/README.org
+++ b/README.org
@@ -1,3 +1,3 @@
-* rabbit-prover
+* vikalpa
 
-Rabbit Prover is Prove S-expression.
+Vikalpa is Proof Assistant.
diff --git a/configure.ac b/configure.ac
index fdfce62..8e5a1f2 100644
--- a/configure.ac
+++ b/configure.ac
@@ -1,5 +1,5 @@
-AC_INIT([rabbit-prover], [0.0.0])
-AC_CONFIG_SRCDIR([rabbit-prover.scm])
+AC_INIT([vikalpa], [0.1.0])
+AC_CONFIG_SRCDIR([vikalpa.scm])
 AC_CONFIG_AUX_DIR([build-aux])
 AM_INIT_AUTOMAKE([-Wall -Werror foreign])
 AM_SILENT_RULES([yes])
diff --git a/examples/prelude.scm b/examples/prelude.scm
new file mode 100644
index 0000000..077b90d
--- /dev/null
+++ b/examples/prelude.scm
@@ -0,0 +1,411 @@
+;;; 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 (vikalpa prelude)
+  #:export (prelude)
+  #:use-module (vikalpa))
+
+(define-syntax-rule (define-axiom/is p1 p2)
+  (define-axiom (is p1 p2) (x) (is (p1 x) (p2 x))))
+
+(define-syntax-rule (define-theorem/is p1 p2)
+  (define-theorem (is p1 p2) (x) (is (p1 x) (p2 x))))
+
+(define-syntax-rule (define-proof/is p1 p2 pc)
+  (define-proof (is p1 p2)
+    ((rewrite (2) if-same (set x (pc x)))
+     (rewrite (2 2 1) (is pc p2))
+     (eval (2 2))
+     (rewrite (2 1) (is p1 pc))
+     (rewrite (2) if-true)
+     (rewrite () if-same))))
+
+(define-syntax implies
+  (syntax-rules ()
+    ((_ x y) (if x y #t))
+    ((_ x y z ...) (if x (implies y z ...) #t))))
+
+(define-system prelude/macro ()
+  (define-syntax-rules cond (else)
+    ((cond (else e)) e)
+    ((cond (test then) . rest)
+     (if test then (cond . rest))))
+  (define-syntax-rules or ()
+    ((or) '#f)
+    ((or x) x)
+    ((or x . xs) (if x x (or . xs))))
+  (define-syntax-rules implies ()
+    ((implies x y) (if x y #t))
+    ((implies x y z . rest)
+     (if x (implies y z . rest) #t)))
+  (define-syntax-rules predicate ()
+    ((predicate x) (implies x (equal? x #t))))
+  (define-syntax-rules is ()
+    ((is x y) (implies x (equal? y #t)))
+    ((is x y . ys) (implies x (is y . ys)))))
+
+(define-system prelude/axiom/equal (prelude/macro)
+  (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-system prelude/axiom/if (prelude/axiom/equal)
+  (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-system prelude/number (prelude/axiom/if)
+  (define-core-function number? (x) number?)
+  (define-axiom (predicate number?) (x) (predicate (number? x)))
+
+  (define-core-function real? (x) real?)
+  (define-axiom (predicate real?) (x) (predicate (real? x)))
+  (define-axiom/is real? number?)
+
+  (define-core-function integer? (x) integer?)
+  (define-axiom (predicate integer?) (x) (predicate (integer? x)))
+  (define-axiom/is integer? real?)
+  (define-theorem/is integer? number?)
+  (define-proof/is integer? number? real?)
+
+  (define-core-function/guard exact? (x) (number? x) exact?)
+  (define-axiom (predicate exact?) (x) (predicate (exact? x)))
+  (define-function/guard inexact? (x)
+    (number? x)
+    (not (exact? x)))
+  (define-theorem (predicate inexact?) (x) (predicate (inexact? x)))
+
+  (define-core-function exact-integer? (x) exact-integer?)
+  (define-axiom (predicate exact-integer?) (x) (predicate (exact-integer? x)))
+  (define-axiom/is exact-integer? integer?)
+  (define-axiom/is exact-integer? exact?)
+  (define-theorem/is exact-integer? real?)
+  (define-proof/is exact-integer? real? integer?)
+  (define-theorem/is exact-integer? number?)
+  (define-proof/is exact-integer? number? real?)
+  (define-core-function/guard < (x y) (and (real? x) (real? y)) <)
+  (define-axiom (predicate <) (x y) (predicate (< x y)))
+
+  (define-function/guard positive? (x)
+    (real? x)
+    (< 0 x))
+  (define-theorem (predicate positive?) (x) (predicate (positive? x)))
+  (define-function/guard negative? (x)
+    (real? x)
+    (< x 0))
+  (define-theorem (predicate negative?) (x) (predicate (negative? x)))
+  (define-function exact-positive-integer? (x)
+    (and (exact-integer? x)
+         (positive? x)))
+  (define-theorem (predicate exact-positive-integer?) (x)
+    (predicate (exact-positive-integer? x)))
+  (define-theorem/is exact-positive-integer? exact-integer?)
+  (define-theorem/is exact-positive-integer? exact?)
+  (define-proof/is exact-positive-integer? exact? exact-integer?)
+  (define-theorem/is exact-positive-integer? integer?)
+  (define-proof/is exact-positive-integer? integer? exact-integer?)
+  (define-theorem/is exact-positive-integer? real?)
+  (define-proof/is exact-positive-integer? real? exact-integer?)
+  (define-theorem/is exact-positive-integer? number?)
+  (define-proof/is exact-positive-integer? number? exact-integer?)
+
+  (define-function exact-zero? (x) (equal? x 0))
+  (define-theorem (predicate exact-zero?) (x)
+    (predicate (exact-zero? x)))
+  (define-theorem/is exact-zero? exact-integer?)
+  (define-theorem/is exact-zero? integer?)
+  (define-proof/is exact-zero? integer? exact-integer?)
+  (define-theorem/is exact-zero? exact?)
+  (define-proof/is exact-zero? exact? exact-integer?)
+  (define-theorem/is exact-zero? real?)
+  (define-proof/is exact-zero? real? exact-integer?)
+  (define-theorem/is exact-zero? number?)
+  (define-proof/is exact-zero? number? real?)
+
+  (define-function natural? (x)
+    (if (exact-zero? x)
+        #t
+        (exact-positive-integer? x)))
+
+  (define-theorem (predicate natural?) (x)
+    (predicate (natural? x)))
+  (define-theorem/is natural? exact-integer?)
+  (define-theorem/is natural? integer?)
+  (define-proof/is natural? integer? exact-integer?)
+  (define-theorem/is natural? exact?)
+  (define-proof/is natural? exact? exact-integer?)
+  (define-theorem/is natural? real?)
+  (define-proof/is natural? real? exact-integer?)
+  (define-theorem/is natural? number?)
+  (define-proof/is natural? number? real?)
+
+  (define-theorem/is exact-zero? natural?)
+  (define-theorem/is exact-positive-integer? natural?)
+  (set-measure-predicate natural?)
+  (set-measure-less-than <)
+
+(define-core-function/guard + (x y) (and (number? x) (number? y)) +)
+  (define-core-function/guard - (x y) (and (number? x) (number? y)) -)
+  (define-function/guard succ (x) (natural? x) (+ x 1))
+  (define-function/guard pred (x) (exact-positive-integer? x) (- x 1))
+  (define-function/guard natural-induction (x)
+    (natural? x)
+    (if (exact-zero? x)
+        #t
+        (succ (natural-induction (pred x)))))
+  (admit natural-induction)
+
+  (define-axiom (+ natural? natural?) (x y)
+    (implies (natural? x)
+             (natural? y)
+             (equal? (+ x y)
+                     (if (exact-zero? x)
+                         y
+                         (succ (+ (pred x) y))))))
+  (define-axiom pred/succ (x)
+    (implies (natural? x)
+             (equal? (pred (succ x)) x)))
+  (define-theorem succ/pred (x)
+    (implies (exact-positive-integer? x)
+             (equal? (succ (pred x)) x)))
+  (define-theorem (is natural? (o natural? succ)) (x)
+    (is (natural? x) (natural? (succ x))))
+
+  (define-theorem (is (o natural? pred) natural?) (x)
+    (is (natural? (pred x))
+        (natural? x)))
+
+  (define-axiom pred/zero (x)
+    (equal? (natural? (pred 0)) #f))
+
+  (define-theorem (is (o not natural?) (o not natural? pred)) (x)
+    (is (not (natural? x))
+        (not (natural? (pred x)))))
+
+  (define-theorem (is (o natural?)
+                      (o not exact-zero?)
+                      exact-positive-integer?)
+    (x)
+    (is (not (natural? x))
+        (not (exact-zero? x))
+        (exact-positive-integer? x)))
+
+  (define-function/guard natural-induction-+ (x y)
+    (and (natural? x) (natural? y))
+    (if (exact-zero? x)
+        y
+        (succ (natural-induction-+ (pred x) y))))
+  (admit natural-induction-+)
+
+  (define-theorem (is natural? (o not exact-zero?) exact-positive-integer?) (x)
+    (is (natural? x)
+        (not (exact-zero? x))
+        (exact-positive-integer? x)))
+
+  (define-theorem (implies natural?
+                           (equal? (o natural? pred)
+                                   exact-positive-integer?))
+    (x)
+    (implies (natural? x)
+             (equal? (natural? (pred x))
+                     (exact-positive-integer? x))))
+
+  (define-theorem (+ (-> natural? natural? natural?)) (x y)
+    (implies (natural? x)
+             (natural? y)
+             (natural? (+ x y)))))
+
+(define-system prelude/measure/natural (prelude/number)
+  (set-measure-predicate natural?)
+  (set-measure-predicate <))
+
+(define-system prelude/pair (prelude/measure/natural)
+  (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-function size (x)
+    (if (pair? x)
+        (+ (size (car x))
+           (size (cdr x)))
+        1))
+  (admit size))
+
+
+(define-system prelude (prelude/pair)
+  (define-proof inexact?
+    ((rewrite (2) if-nest)
+     (rewrite () if-same)))
+  (define-proof (predicate inexact?)
+    ((rewrite (1) inexact?)
+     (rewrite () if-not)
+     (rewrite (3 1) inexact?)
+     (rewrite (3 1 1) equal-if-false)
+     (eval (3))
+     (rewrite () if-same)))
+  (define-proof positive?
+    ((eval (2 1 1))
+     (rewrite (2 1) if-true)
+     (rewrite (2) if-nest)
+     (rewrite () if-same)))
+  (define-proof (predicate positive?)
+    ((rewrite (1) positive?)
+     (rewrite (2 1) positive?)
+     (rewrite (2 1) (predicate <))
+     (eval (2))
+     (rewrite () if-same)))
+  (define-proof negative?
+    ((rewrite (2 1) if-nest)
+     (eval (2 1))
+     (rewrite (2) if-true)
+     (rewrite () if-same)))
+  (define-proof (predicate negative?)
+    ((rewrite (1) negative?)
+     (rewrite (2 1) negative?)
+     (rewrite (2 1) (predicate <))
+     (eval (2))
+     (rewrite () if-same)))
+  (define-proof exact-positive-integer?
+    ((rewrite (1 2) (is exact-integer? real?))
+     (rewrite (1) if-same)
+     (eval ())))
+  (define-proof (predicate exact-positive-integer?)
+    ((rewrite (1) exact-positive-integer?)
+     (rewrite () if-same (set x (exact-integer? x)))
+     (rewrite (3 1) if-nest)
+     (rewrite (3) if-false)
+     (rewrite (2 1) if-nest)
+     (rewrite (2 2 1) exact-positive-integer?)
+     (rewrite (2 2 1 1) (predicate exact-integer?))
+     (rewrite (2 2 1 2) (predicate positive?))
+     (eval (2 2))
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+  (define-proof (predicate exact-zero?)
+    ((rewrite (1) exact-zero?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2))
+     (rewrite () if-same)))
+  (define-proof (predicate natural?)
+    ((rewrite (1) natural?)
+     (rewrite () if-same (set x (exact-zero? x)))
+     (rewrite (2 1) if-nest)
+     (rewrite (2) if-true)
+     (rewrite (3 1) if-nest)
+     (rewrite (1) exact-zero?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2))
+     (rewrite (1) exact-zero?)
+     (rewrite (3 2 1) natural?)
+     (rewrite (3 2 1) if-nest)
+     (rewrite (3 2 1) (predicate exact-positive-integer?))
+     (eval (3 2))
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+  (define-proof (is exact-positive-integer? exact-integer?)
+    ((rewrite (1) exact-positive-integer?)
+     (rewrite () if-same (set x (exact-integer? x)))
+     (rewrite (3 1) if-nest)
+     (rewrite (2 1) if-nest)
+     (rewrite (2 2 1) (predicate exact-integer?))
+     (eval (2 2))
+     (rewrite (2) if-same)
+     (rewrite (3) if-false)
+     (rewrite ()  if-same)))
+  (define-proof (is exact-zero? exact-integer?)
+    ((rewrite (1) exact-zero?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2))
+     (rewrite () if-same)))
+  (define-proof (is natural? exact-integer?)
+    ((rewrite (1) natural?)
+     (rewrite () if-same (set x (exact-zero? x)))
+     (rewrite (2 1) if-nest)
+     (rewrite (2) if-true)
+     (rewrite (2 1) (is exact-zero? exact-integer?))
+     (eval (2))
+     (rewrite (3 1) if-nest)
+     (rewrite (3 2 1) (is exact-positive-integer? exact-integer?))
+     (eval (3 2))
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+  (define-proof succ
+    ((rewrite (2 1 1) (is natural? number?))
+     (eval (2))
+     (rewrite ()  if-same)))
+  (define-proof pred
+    ((rewrite (2 1 1) (is exact-positive-integer? number?))
+     (eval (2))
+     (rewrite () if-same)))
+
+  (define-proof (+ (-> natural? natural? natural?))
+    ((induction (2 2) (natural-induction-+ x y))
+     (rewrite (2 2 2 1) (+ natural? natural?))
+     (rewrite (2 2 2 1) if-nest)
+     (rewrite (2 2 2) (predicate natural?))
+     (rewrite (2 2 3 2) if-same (set x (natural? (pred x))))
+     (rewrite (2 2 3 2 2 1) (+ natural? natural?))
+     (rewrite (2 2 3 2 2 1) if-nest)
+     (rewrite (2 2 3 2 2) (is natural? (o natural? succ)))
+     (rewrite (2 2 3 2 1) (implies natural?
+                                   (equal? (o natural? pred)
+                                           exact-positive-integer?)))
+     (rewrite (2 2 3 2 1) (is natural? (o not exact-zero?)
+                              exact-positive-integer?))
+     (rewrite (2 2 3 2) if-true)
+     (rewrite (2 2 3) if-same)
+     (rewrite (2 2) if-same)
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (is exact-zero? natural?)
+    ((rewrite (1) exact-zero?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2))
+     (rewrite () if-same)))
+
+  (define-proof (is exact-positive-integer? natural?)
+    ((rewrite (2 1) natural?)
+     (rewrite (2 1 3) (predicate exact-positive-integer?))
+     (rewrite (2 1) if-same)
+     (eval (2))
+     (rewrite () if-same)))
+
+  (define-proof (is (o natural? pred) natural?)
+    ((rewrite () if-same (set x (natural? x)))
+     (rewrite (2 2 1) (predicate natural?))
+     (eval (2 2))
+     (rewrite (3 2 1) equal-if-false)
+     (eval (3 2))
+     (rewrite (2) if-same)))
+  (admit (is natural? (o natural? succ))))
diff --git a/examples/the-little-prover.scm b/examples/the-little-prover.scm
new file mode 100644
index 0000000..0a0303e
--- /dev/null
+++ b/examples/the-little-prover.scm
@@ -0,0 +1,5 @@
+(use-modules (vikalpa)
+             (vikalpa the-little-prover))
+
+(define-system the-little-prover-0 (the-little-prover)
+  )
diff --git a/guix.scm b/guix.scm
index 92731d5..21460c6 100644
--- a/guix.scm
+++ b/guix.scm
@@ -1,20 +1,20 @@
-;;; Rabbit Prover --- Prove S-expression
-;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
+;;; Vikalpa --- Proof Assistant
+;;; Copyright © 2020, 2021 Masaya Tojo <masaya@tojo.tokyo>
 ;;;
-;;; This file is part of Rabbit Prover.
+;;; This file is part of Vikalpa.
 ;;;
-;;; Rabbit Prover is free software; you can redistribute it and/or modify it
+;;; 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.
 ;;;
-;;; Rabbit Prover is distributed in the hope that it will be useful, but
+;;; 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 Rabbit Prover.  If not, see <http://www.gnu.org/licenses/>.
+;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (use-modules (guix packages)
              ((guix licenses) #:prefix license:)
@@ -26,11 +26,11 @@
              (gnu packages pkg-config)
              (gnu packages texinfo))
 
-(define guile-rabbit-prover
+(define guile-vikalpa
   (package
-    (name "guile-rabbit-prover")
-    (version "0.0.0")
-    (source (string-append (getcwd) "/rabbit-prover-" version ".tar.gz"))
+    (name "guile-vikalpa")
+    (version "0.1.0")
+    (source (string-append (getcwd) "/vikalpa-" version ".tar.gz"))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
@@ -39,9 +39,9 @@
        ("texinfo" ,texinfo)))
     (inputs
      `(("guile" ,guile-3.0)))
-    (synopsis "Prove S-expression")
-    (description "Rabbit Prover is Prove S-expression.")
-    (home-page "https://gitlab.com/tojoqk/rabbit-prover")
+    (synopsis "Proof Assistant")
+    (description "Vikalpa is Proof Assistant.")
+    (home-page "https://gitlab.com/tojoqk/vikalpa")
     (license license:gpl3+)))
 
-guile-rabbit-prover
+guile-vikalpa
diff --git a/pre-inst-env.in b/pre-inst-env.in
index 42c7ec7..25ecd03 100644
--- a/pre-inst-env.in
+++ b/pre-inst-env.in
@@ -1,22 +1,22 @@
 #!/bin/sh
 
-# Rabbit Prover --- Prove S-expression
+# Vikalpa --- Proof Assistant
 # Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
 #
-# This file is part of Rabbit Prover.
+# This file is part of Vikalpa.
 #
-# Rabbit Prover is free software; you can redistribute it and/or modify it
+# 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.
 #
-# Rabbit Prover is distributed in the hope that it will be useful, but WITHOUT
+# 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 Rabbit Prover.  If not, see <http://www.gnu.org/licenses/>.
+# along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 abs_top_srcdir="`cd "@abs_top_srcdir@" > /dev/null; pwd`"
 abs_top_builddir="`cd "@abs_top_builddir@" > /dev/null; pwd`"
diff --git a/rabbit-prover.scm b/rabbit-prover.scm
deleted file mode 100644
index e661db2..0000000
--- a/rabbit-prover.scm
+++ /dev/null
@@ -1,20 +0,0 @@
-;;; Rabbit Prover --- Prove S-expression
-;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
-;;;
-;;; This file is part of Rabbit Prover.
-;;;
-;;; Rabbit Prover 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.
-;;;
-;;; Rabbit Prover 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 Rabbit Prover.  If not, see <http://www.gnu.org/licenses/>.
-
-(define-module (rabbit-prover)
-  #:export ())
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
new file mode 100644
index 0000000..3d269f8
--- /dev/null
+++ b/vikalpa.scm
@@ -0,0 +1,1605 @@
+;;; 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 (vikalpa)
+  #:export (system?
+            system-rewrite
+            system-check
+            system-apropos
+            system-eval
+            system-lookup
+            set-measure-predicate
+            set-measure-less-than
+            define-system
+            define-proof
+            define-core-function
+            define-core-function/guard
+            define-function
+            define-function
+            define-function/guard
+            define-axiom-function
+            define-axiom-function/guard
+            define-syntax-rules
+            define-axiom
+            define-theorem
+            admit)
+  #:use-module (ice-9 match)
+  #:use-module (ice-9 format)
+  #:use-module (ice-9 control)
+  #:use-module (ice-9 exceptions)
+  #:use-module (ice-9 regex)
+  #:use-module ((srfi srfi-1)
+                #:select (every any lset-union fold append-map find
+                                filter-map))
+  #:use-module (srfi srfi-8)
+  #:use-module (srfi srfi-11)
+  #:use-module (srfi srfi-26)
+  #:use-module (oop goops))
+
+(define-class <system> ()
+  (definitions
+    #:getter get-definitions
+    #:init-keyword #:definitions
+    #:init-value '())
+  (measure-predicate #:getter get-measure-predicate
+                     #:init-value #f)
+  (measure-less-than #:getter get-measure-less-than
+                     #:init-value #f))
+
+(define-class <definition> ()
+  (name #:getter get-name
+        #:init-keyword #:name)
+  (variables #:getter get-variables
+             #:init-keyword #:variables
+             #:init-value '()))
+
+(define-class <provable> ())
+
+(define-class <proved> (<provable>)
+  (claim #:getter get-claim #:init-keyword #:claim)
+  (proof #:getter get-proof #:init-keyword #:proof))
+
+(define-class <admitted> ())
+
+(define-class <theorem*> (<definition>)
+  (expression #:getter get-expression #:init-keyword #:expression))
+
+(define-class <conjecture> (<theorem*> <provable>))
+(define-class <theorem> (<theorem*> <proved>))
+(define-class <axiom> (<theorem*>))
+(define-class <admitted-theorem> (<theorem*> <proved> <admitted>))
+
+(define-class <function*> (<definition>)
+  (guards #:getter get-guards #:init-keyword #:guards))
+(define-class <core-function> (<function*>)
+  (procedure #:getter get-procedure #:init-keyword #:procedure))
+(define-class <expandable-function> (<function*>)
+  (expression #:getter get-expression #:init-keyword #:expression)
+  (code #:getter get-code #:init-keyword #:code))
+(define-class <function> (<expandable-function> <provable>))
+(define-class <total-function> (<expandable-function> <proved>))
+(define-class <admitted-function> (<expandable-function> <proved> <admitted>))
+
+(define-class <macro> (<definition>)
+  (mrules #:getter macro-mrules #:init-keyword #:mrules)
+  (literals #:getter macro-literals #:init-keyword #:literals))
+
+(define (write-definition sym d port)
+  (format port "#<~a: ~s>"
+          sym (cons (get-name d) (get-variables d))))
+
+(define-method (display (s <system>) port)
+  (format port "#<system: function: ~a theorem: ~a macro: ~a>"
+          (length (filter (cut is-a? <> <function*>)
+                          (get-definitions s)))
+          (length (filter (cut is-a? <> <theorem*>)
+                          (get-definitions s)))
+          (length (filter (cut is-a? <> <macro>)
+                          (get-definitions s)))))
+
+(define-method (write (s <system>) port)
+  (format port "#<system: function: ~a theorem: ~a macro: ~a>"
+          (length (filter (cut is-a? <> <function*>)
+                          (get-definitions s)))
+          (length (filter (cut is-a? <> <theorem*>)
+                          (get-definitions s)))
+          (length (filter (cut is-a? <> <macro>)
+                          (get-definitions s)))))
+
+(define-method (lookup name (s <system>))
+  (find (lambda (x)
+          (equal? name (get-name x)))
+        (get-definitions s)))
+
+(define-method (update-measure-predicate (s <symbol>) (sys <system>))
+  (let ((new (shallow-clone sys)))
+    (slot-set! new 'measure-predicate s)
+    new))
+
+(define-method (update-measure-less-than (s <symbol>) (sys <system>))
+  (let ((new (shallow-clone sys)))
+    (slot-set! new 'measure-less-than s)
+    new))
+
+(define-method (update-definition (d <definition>) (sys <system>))
+  (define (update d defs)
+    (if (null? defs)
+        (raise-exception
+         (make-exception
+          (make-exception-with-origin 'update-definition)
+          (make-exception-with-message "not found")
+          (make-exception-with-irritants (list d defs))))
+        (if (equal? (get-name d) (get-name (car defs)))
+            (cons d (cdr defs))
+            (cons (car defs) (update d (cdr defs))))))
+  (let ((new (shallow-clone sys)))
+    (slot-set! new 'definitions
+               (update d (get-definitions sys)))
+    new))
+
+(define-method (remove-first-definition (sys <system>))
+  (let ((new (shallow-clone sys)))
+    (slot-set! new 'definitions
+               (cdr (get-definitions sys)))
+    new))
+
+(define-method (first-definition (sys <system>))
+  (car (get-definitions sys)))
+
+(define-method (system-empty? (sys <system>))
+  (null? (get-definitions sys)))
+
+(define-method (add-definition (d <definition>) (s <system>))
+  (if (lookup (get-name d) s)
+      (raise-exception
+       (make-exception
+        (make-exception-with-origin 'add-definition)
+        (make-exception-with-message "duplicated definition")
+        (make-exception-with-irritants (get-name d))))
+      (if (reserved? (get-name d))
+          (raise-exception
+           (make-exception
+            (make-exception-with-origin 'add-definition)
+            (make-exception-with-message "reserved name")
+            (make-exception-with-irritants (get-name d))))
+          (let ((new (shallow-clone s)))
+            (slot-set! new 'definitions
+                       (cons d (get-definitions s)))
+            new))))
+
+(define-method (validate (d <definition>))
+  (let* ((vars (get-variables d))
+         (name (get-name d)))
+    (validate-vars (format #f "~a" name) vars)))
+
+(define-method (validate (d <expandable-function>))
+  (let* ((vars (get-variables d))
+         (name (get-name d))
+         (expr (get-expression d)))
+    (validate-expression (current-system) name vars expr)
+    (next-method)))
+
+(define-method (validate (d <theorem*>))
+  (let* ((vars (get-variables d))
+         (name (get-name d))
+         (expr (get-expression d)))
+    (validate-expression (current-system) name vars expr)
+    (next-method)))
+
+(define-syntax-rule (define/guard (name (var p?) ...) b b* ...)
+  (define (name var ...)
+    (unless (p? var)
+      (error (format #f
+                     "~a:~%  expected:  ~a~%  given: "
+                     'name
+                     'p?)
+             var))
+    ...
+    b b* ...))
+
+(define (natural? x)
+  (and (exact-integer? x)
+       (not (negative? x))))
+
+(define (option p?)
+  (lambda (x)
+    (or (p? x) (not x))))
+
+(define (list-of p?)
+  (lambda (x)
+    (and (list? x)
+         (every p? x))))
+
+(define (expression? expr)
+  (cond ((expr-quoted? expr) #t)
+        ((if-form? expr)
+         (and (expression? (if-form-test expr))
+              (expression? (if-form-then expr))
+              (expression? (if-form-else expr))))
+        ((app-form? expr)
+         (and (symbol? (car expr))
+              (list? (cdr expr))
+              (every expression? (cdr expr))))
+        ((variable? expr) #t)
+        (else #f)))
+
+(define (app-form? expr)
+  (and (pair? expr)
+       (not (eq? (car expr) 'quote))
+       (not (eq? (car expr) 'if))))
+
+(define (app-form name args)
+  (cons name args))
+
+(define (app-form-name expr)
+  (car expr))
+
+(define (app-form-args expr)
+  (cdr expr))
+
+(define (if-form test then else)
+  (list 'if test then else))
+
+(define (if-form? x)
+  (and (pair? x)
+       (eq? (car x) 'if)))
+
+(define (if-form-test expr)
+  (list-ref expr 1))
+
+(define (if-form-then expr)
+  (list-ref expr 2))
+
+(define (if-form-else expr)
+  (list-ref expr 3))
+
+(define (expression-app-forms expr)
+  (cond
+   ((if-form? expr)
+    (append-map expression-app-forms
+                (list (if-form-test expr)
+                      (if-form-then expr)
+                      (if-form-else expr))))
+   ((app-form? expr)
+    (cons expr
+          (append-map expression-app-forms
+                      (app-form-args expr))))
+   (else '())))
+
+(define (expression-functions expr)
+  (cond
+   ((if-form? expr)
+    (apply lset-union
+           eq?
+           (map expression-functions
+                (list (if-form-test expr)
+                      (if-form-then expr)
+                      (if-form-else expr)))))
+   ((app-form? expr)
+    (cons (app-form-name expr)
+          (apply lset-union
+                 eq?
+                 (map expression-functions (app-form-args expr)))))
+   (else '())))
+
+(define (expression-vars expr)
+  (cond
+   ((expr-quoted? expr) '())
+   ((if-form? expr)
+    (lset-union eq?
+                (expression-vars (if-form-test expr))
+                (expression-vars (if-form-then expr))
+                (expression-vars (if-form-else expr))))
+   ((app-form? expr)
+    (apply lset-union
+           eq?
+           (map expression-vars (app-form-args expr))))
+   ((variable? expr) (list expr))
+   (else '())))
+
+(define (expr-quoted? expr)
+  (and (pair? expr)
+       (eq? 'quote (car expr))
+       (pair? (cdr expr))
+       ((const #t) (car (cdr expr)))
+       (null? (cdr (cdr expr)))))
+
+(define (expr-unquote expr)
+  (car (cdr expr)))
+
+(define (expr-quote expr)
+  (list 'quote expr))
+
+(define (variable? x)
+  (symbol? x))
+
+(define (variable=? v1 v2)
+  (eq? v1 v2))
+
+(define-class <rule> ()
+  (vars #:getter rule-vars #:init-keyword #:vars)
+  (preconds #:getter rule-preconds #:init-keyword #:preconds)
+  (lhs #:getter rule-lhs #:init-keyword #:lhs)
+  (rhs #:getter rule-rhs #:init-keyword #:rhs))
+
+(define (rule var preconds lhs rhs)
+  (make <rule>
+    #:vars var
+    #:preconds preconds
+    #:lhs lhs
+    #:rhs rhs))
+
+(define (rule? x)
+  (is-a? x <rule>))
+
+(define (binding? x)
+  (and (pair? x)
+       (symbol? (car x))
+       (expression? (cdr x))))
+
+(define (env? x)
+  ((list-of binding?) x))
+
+(define/guard (substitute (env env?) (expr (const #t)))
+  (cond ((expr-quoted? expr) expr)
+        ((pair? expr)
+         (cons (substitute env (car expr))
+               (substitute env (cdr expr))))
+        ((assoc expr env) => cdr)
+        (else expr)))
+
+(define (match-rule preconds rl expr env)
+  (define (fail)
+    (shift k #f))
+  (define (var? v)
+    (and (member v (rule-vars rl))
+         #t))
+  (define (add-env var expr env)
+    (cond
+     ((assoc var env)
+      => (match-lambda
+           ((env-var . env-expr)
+            (if (equal? env-expr expr)
+                env
+                (fail)))))
+     (else
+      (cons (cons var expr)
+            env))))
+  (define (mat-fold lhss exprs env)
+    (cond ((and (pair? lhss) (pair? exprs))
+           (mat-fold (cdr lhss)
+                     (cdr exprs)
+                     (mat (car lhss)
+                          (car exprs)
+                          env)))
+          ((and (null? lhss) (null? exprs)) env)
+          (else (fail))))
+  (define (mat-begin lhs expr env)
+    (reset (mat lhs expr env)))
+  (define (mat lhs expr env)
+    (cond ((expr-quoted? lhs)
+           (if (expr-quoted? expr)
+               (if (equal? lhs expr)
+                   env
+                   (fail))
+               (fail)))
+          ((and (if-form? lhs)
+                (if-form? expr))
+           (mat-fold (list (if-form-test lhs)
+                           (if-form-then lhs)
+                           (if-form-else lhs))
+                     (list (if-form-test expr)
+                           (if-form-then expr)
+                           (if-form-else expr))
+                     env))
+          ((app-form? lhs)
+           (if (and (app-form? expr)
+                    (symbol? (app-form-name lhs))
+                    (eqv? (app-form-name lhs) (app-form-name expr)))
+               (mat-fold (app-form-args lhs) (app-form-args expr) env)
+               (fail)))
+          ((var? lhs) (add-env lhs expr env))
+          (else (fail))))
+  (define (mat-preconds rlps k+env)
+    (if (null? rlps)
+        k+env
+        (mat-preconds
+         (cdr rlps)
+         (let search ((ps preconds))
+           (if (null? ps)
+               (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))))))))
+                  (else (search (cdr ps))))))))))
+  (define (valid? env expr)
+    (cond ((expr-quoted? expr) #t)
+          ((pair? expr)
+           (and (valid? env (car expr))
+                (valid? env (cdr expr))))
+          ((var? expr)
+           (cond ((assoc expr env) => (const #t))
+                 (else #f)))
+          (else #t)))
+  (reset
+   (shift k0
+          (match (mat-preconds (rule-preconds rl) (cons k0 env))
+            ((k . env)
+             (cond
+              ((mat-begin (rule-lhs rl) expr env)
+               => (lambda (env)
+                    (if (valid? env (rule-rhs rl))
+                        env
+                        (k #f))))
+              (else (k #f))))
+            (else #f)))))
+
+(define (apply-rule preconds rl expr env)
+  (cond
+   ((match-rule preconds rl expr env)
+    => (cut substitute <> (rule-rhs rl)))
+   (else #f)))
+
+(define (code x)
+  (list 'code x))
+
+(define (code-expr x)
+  (cadr x))
+
+(define-class <mrule> ()
+  (lhs #:getter mrule-lhs #:init-keyword #:lhs)
+  (rhs #:getter mrule-rhs #:init-keyword #:rhs))
+
+(define (mrule lhs rhs)
+  (make <mrule> #:lhs lhs #:rhs rhs))
+
+(define (mrule-vars mrl)
+  (define (all-vars x)
+    (cond ((expr-quoted? x) '())
+          ((pair? x)
+           (append (all-vars (car x))
+                   (all-vars (cdr x))))
+          ((variable? x) (list x))
+          (else '())))
+  (all-vars (mrule-lhs mrl)))
+
+(define (macro name mrules literals)
+  (make <macro>
+    #:name name
+    #:variables '()
+    #:mrules mrules
+    #:literals literals))
+
+(define (apply-mrule rl ls expr)
+  (define (literal? x)
+    (member x ls))
+  (define (var? v)
+    (and (member v (mrule-vars rl))
+         #t))
+  (call/cc
+   (lambda (k)
+     (define (mat-map lhs-tree expr-tree env)
+       (cond ((and (pair? lhs-tree)
+                   (pair? expr-tree))
+              (mat-map (car lhs-tree)
+                       (car expr-tree)
+                       (mat-map (cdr lhs-tree)
+                                (cdr expr-tree)
+                                env)))
+             (else (mat lhs-tree expr-tree env))))
+     (define (mat lhs expr env)
+       (cond ((expr-quoted? lhs)
+              (if (expr-quoted? expr)
+                  (if (equal? lhs expr)
+                      env
+                      (k #f))
+                  (k #f)))
+             ((and (pair? lhs) (pair? expr))
+              (mat-map lhs expr env))
+             ((literal? lhs)
+              (if (eq? lhs expr)
+                  env
+                  (k #f)))
+             ((var? lhs)
+              (cond
+               ((assoc lhs env)
+                => (match-lambda
+                     ((env-var . env-expr)
+                      (if (equal? env-expr expr)
+                          env
+                          (k #f)))))
+               (else
+                (cons (cons lhs expr)
+                      env))))
+             ((eqv? lhs expr) env)
+             (else (k #f))))
+     (define (mrule-substitute env expr)
+       (cond ((expr-quoted? expr) expr)
+             ((pair? expr)
+              (cons (mrule-substitute env (car expr))
+                    (mrule-substitute env (cdr expr))))
+             ((literal? expr) expr)
+             ((and (variable? expr) (assoc expr env)) => cdr)
+             (else expr)))
+     (mrule-substitute (mat (mrule-lhs rl)
+                            expr
+                            '())
+                       (mrule-rhs rl)))))
+
+(define (apply-macro m expr)
+  (cond ((and (pair? expr)
+              (eq? (get-name m) (car expr)))
+         (let loop ((rs (macro-mrules m)))
+           (cond ((null? rs)
+                  (error "(vikalpa) macro fail" m expr))
+                 ((apply-mrule (car rs) (macro-literals m) expr) => identity)
+                 (else (loop (cdr rs))))))
+        (else #f)))
+
+(define (expand ms expr)
+  (let loop ((ms ms)
+             (expr expr))
+    (cond
+     ((null? ms) expr)
+     (else
+      (expand (cdr ms)
+              (cond
+               ((apply-macro (car ms) expr) => identity)
+               (else expr)))))))
+
+(define (expand* ms expr)
+  (let loop ((ms ms)
+             (expr expr))
+    (let ((new-expr (expand ms expr)))
+      (if (equal? expr new-expr)
+          (if (pair? new-expr)
+              (cons (expand* ms (car new-expr))
+                    (expand* ms (cdr new-expr)))
+              new-expr)
+          (expand* ms new-expr)))))
+
+(define (quote-all x)
+  (cond
+   ((null? x) x)
+   ((expr-quoted? x) x)
+   ((pair? x)
+    (cons (quote-all (car x))
+          (quote-all (cdr x))))
+   ((symbol? x) x)
+   (else `',x)))
+
+(define (let? x)
+  (and (list? x)
+       (= 3 (length x))
+       (eq? 'let (list-ref x 0))
+       ((list-of (lambda (x)
+                   (and (list? x)
+                        (= 2 (length x))
+                        (symbol? (car x)))))
+        (list-ref x 1))))
+
+(define (expand-let x)
+  (define (let-substitute env expr)
+    (cond ((expr-quoted? expr) expr)
+          ((let? expr)
+           (let-substitute
+            (append (map (lambda (binding)
+                           (cons (car binding)
+                                 (let-substitute env
+                                                 (cadr binding))))
+                         (list-ref expr 1))
+                    env)
+            (list-ref expr 2)))
+          ((pair? expr)
+           (cons (let-substitute env (car expr))
+                 (let-substitute env (cdr expr))))
+          ((assoc expr env) => cdr)
+          (else expr)))
+  (cond
+   ((expr-quoted? x) x)
+   ((let? x)
+    (expand-let
+     (let-substitute (map (lambda (binding) (cons (car binding)
+                                                  (cadr binding)))
+                          (list-ref x 1))
+                     (list-ref x 2))))
+   ((pair? x)
+    (cons (expand-let (car x))
+          (expand-let (cdr x))))
+   (else x)))
+
+(define (convert-to-expression x)
+  (quote-all
+   (expand* (filter (cut is-a? <> <macro>)
+                    (get-definitions (current-system)))
+            (expand-let x))))
+
+(define (vars? x)
+  (and (list? x)
+       (every variable? x)))
+
+(define (theorem-rules x)
+  (expression->rules (get-variables x)
+                     '()
+                     (get-expression x)))
+
+(define (result? x)
+  (or (result/error? x)
+      (result/expr? x)))
+
+(define (result/error? x)
+  (and (pair? x)
+       (eq? 'result/error (car x))))
+
+(define (result/error . args)
+  (cons* 'result/error args))
+
+(define (result/expr? x)
+  (and (list? x)
+       (= 2 (length x))
+       (eq? 'result/expr (car x))
+       (expression? (cadr x))))
+
+(define (result/expr x)
+  (list 'result/expr x))
+
+(define/guard (result/expr-expr (x result/expr?))
+  (cadr x))
+
+(define (rewrite/eval expr sys)
+  (let eval ((result (result/expr expr)))
+    (cond
+     ((result/error? result) result)
+     ((result/expr? result)
+      (let ((expr (result/expr-expr result)))
+        (cond
+         ((expr-quoted? expr) (result/expr expr))
+         ((app-form? expr)
+          (let ((args/result (map (compose eval result/expr)
+                                  (app-form-args expr)))
+                (name (app-form-name expr)))
+            (cond
+             ((find error? args/result) => identity)
+             ((lookup name sys)
+              => (lambda (f)
+                   (let ((args (map result/expr-expr args/result))
+                         (gs (get-guards f))
+                         (vars (get-variables f))
+                         (form (defined-function-app-form f)))
+                     (define (guard-ok? vars form g)
+                       (let ((result (eval (apply-rule '()
+                                                       (rule vars '() form g)
+                                                       `(,name ,@args)
+                                                       '()))))
+                         (if (result/error? result)
+                             result
+                             (expr-unquote (result/expr-expr result)))))
+                     (if (every (lambda (g) (guard-ok? vars form g)) gs)
+                         (eval (rewrite1 sys
+                                         `(,name ,@args)
+                                         `(rewrite () ,name)))
+                         (result/error 'guard-error `(,name ,@args) `(and ,@gs))))))
+             (else (result/error 'function-not-found name)))))
+         ((if-form? expr)
+          (let ((test/result (eval (result/expr (if-form-test expr)))))
+            (if (result/error? test/result)
+                test/result
+                (if (expr-unquote (result/expr-expr test/result))
+                    (eval (result/expr (if-form-then expr)))
+                    (eval (result/expr (if-form-else expr)))))))
+         ((variable? expr)
+          (result/error 'eval 'variable-found expr))
+         (else
+          (result/error 'eval 'invalid-expression expr)))))
+     (else (result/error 'eval 'invalid-result result)))))
+
+(define (rewriter? x)
+  (match x
+    (('rewrite path command-name command-ops ...)
+     (and (path? path)
+          (command-name? command-name)
+          (every command-option? command-ops)))
+    (('eval path) (path? path))
+    (('induction path (fname vars ...))
+     (and (path? path)
+          (symbol? fname)
+          (every variable? vars)))
+    (else #f)))
+
+(define (sequence? x)
+  (and (list? x)
+       (every rewriter? x)))
+
+(define (path? x)
+  (and (list? x)
+       (every natural? x)))
+
+(define (command-name? x) #t)
+
+(define (command-option? x)
+  (and (pair? x)
+       (case (car x)
+         ((set) (and (list? x)
+                     (= 3 (length x))
+                     (variable? (list-ref x 1))
+                     (expression? (list-ref x 2))))
+         (else #f))))
+
+(define (command-name x)
+  (car x))
+
+(define (command-options x)
+  (cdr x))
+
+(define/guard (system-eval (sys system?) (expr (const #t)))
+  (rewrite/eval (parameterize ((current-system sys))
+                  (convert-to-expression expr))
+                sys))
+
+(define (extract path expr fail)
+  (if (null? path)
+      (values expr '() identity)
+      (let ((i (car path)))
+        (cond
+         ((if-form? expr)
+          (let ((precond (if-form-test expr)))
+            (receive (extracted-expr preconds builder)
+                (extract (cdr path) (list-ref expr i) fail)
+              (values extracted-expr
+                      (case i
+                        ((1) preconds)
+                        ((2) (cons (prop-not (prop-not precond))
+                                   preconds))
+                        ((3) (cons (prop-not precond) preconds))
+                        (else (fail 'if-invaild-path path)))
+                      (lambda (x)
+                        (append (list-head expr i)
+                                (list (builder x))
+                                (list-tail expr (+ i 1))))))))
+         ((< i (length expr))
+          (receive (extracted-expr preconds builder)
+              (extract (cdr path) (list-ref expr i) fail)
+            (values extracted-expr
+                    preconds
+                    (lambda (x)
+                      (append (list-head expr i)
+                              (list (builder x))
+                              (list-tail expr (+ i 1)))))))
+         (else
+          (fail 'invalid-path path))))))
+
+(define (function->rules x)
+  (list (rule (get-variables x)
+              (list)
+              (defined-function-app-form x)
+              (get-expression x))
+        (rule (get-variables x)
+              (list)
+              (get-expression x)
+              (defined-function-app-form x))))
+
+(define (apply-function f args)
+  (apply-rule '()
+              (rule (get-variables f)
+                    '()
+                    (defined-function-app-form f)
+                    (get-expression f))
+              (app-form (get-name f) args)
+              '()))
+
+(define (parse-options/theorem ops fail)
+  (if (null? ops)
+      (values '())
+      (receive (env)
+          (parse-options/theorem (cdr ops) fail)
+        (case (caar ops)
+          ((set)
+           (let ((op (car ops)))
+             (cons (cons (list-ref op 1)
+                         (list-ref op 2))
+                   env)))
+          (else
+           (fail 'invalid-option (car ops)))))))
+
+(define (rewrite/theorem cmd-name cmd-ops b thm preconds expr)
+  (call/cc
+   (lambda (k)
+     (define (fail . args)
+       (k (apply result/error args)))
+     (receive (env)
+         (parse-options/theorem cmd-ops fail)
+       (cond
+        ((any (cut apply-rule preconds <> expr env)
+              (theorem-rules thm)) => result/expr)
+        (else
+         (result/error 'apply-theorem cmd-name expr)))))))
+
+(define (rewrite/core-function sys f expr)
+  (if (and (app-form? expr)
+           (eq? (get-name f) (app-form-name expr))
+           (= (length (get-variables f)) (length (app-form-args expr)))
+           (every expr-quoted? (app-form-args expr)))
+      (result/expr
+       (expr-quote (apply (get-procedure f)
+                          (map expr-unquote (app-form-args expr)))))
+      (result/error 'apply-core-function (get-name f) expr)))
+
+(define (rewrite/function sys fname f expr)
+  (cond
+   ((any (cut apply-rule '() <> expr '())
+         (function->rules f))
+    => result/expr)
+   (else
+    (result/error 'apply-function fname expr))))
+
+(define (rewrite/induction sys fname vars ps expr)
+  (cond
+   ((lookup fname sys)
+    => (lambda (f)
+         (cond
+          ((not (is-a? f <expandable-function>))
+           (result/error 'induction 'not-expandable-function fname expr))
+          ((apply-rule ps
+                       (make-induction-rule f vars expr)
+                       expr
+                       '())
+           => result/expr)
+          (else
+           (result/error 'induction 'error fname expr)))))
+   (else (result/error 'induction 'not-found fname expr))))
+
+(define (rewrite1 sys expr r)
+  (call/cc
+   (lambda (k)
+     (define (fail . args)
+       (k (apply result/error args)))
+     (define (result->expr x)
+       (cond
+        ((result/error? x) (fail (cdr x)))
+        (else
+         (result/expr-expr x))))
+     (match r
+       (('eval path)
+        (receive (extracted-expr preconds builder)
+            (extract path expr fail)
+          (result/expr
+           (builder
+            (result->expr (rewrite/eval extracted-expr sys))))))
+       (('induction path (fname vars ...))
+        (receive (extracted-expr preconds builder)
+            (extract path expr fail)
+          (result/expr
+           (builder
+            (result->expr
+             (rewrite/induction sys fname vars preconds extracted-expr))))))
+       (('rewrite path cmd-name cmd-ops ...)
+        (receive (extracted-expr preconds builder)
+            (extract path expr fail)
+          (result/expr
+           (builder
+            (result->expr
+             (cond
+              ((lookup cmd-name sys)
+               => (lambda (x)
+                    (cond
+                     ((is-a? x <core-function>)
+                      (rewrite/core-function sys x extracted-expr))
+                     ((is-a? x <theorem*>)
+                      (rewrite/theorem cmd-name cmd-ops sys x preconds extracted-expr))
+                     ((is-a? x <expandable-function>)
+                      (rewrite/function sys cmd-name x extracted-expr))
+                     (else
+                      (result/error 'invalid-command cmd-name extracted-expr)))))
+              (else (result/error 'command-not-found cmd-name extracted-expr))))))))))))
+
+(define (rewrite sys expr seq)
+  (let loop ((result (result/expr expr))
+             (seq seq))
+    (cond
+     ((result/error? result) result)
+     ((result/expr? result)
+      (if (null? seq)
+          result
+          (loop (rewrite1 sys
+                          (result/expr-expr result)
+                          (car seq))
+                (cdr seq))))
+     (else (result/error 'invalid-result result)))))
+
+(define (expr-not x)
+  (list 'not x))
+
+(define (prop-not x)
+  (match x
+    (('not ('not expr)) (prop-not expr))
+    (('not expr) expr)
+    (expr (expr-not expr))))
+
+(define (expr-equal? x)
+  (and (list? x)
+       (= 3 (length x))
+       (eq? 'equal? (list-ref x 0))
+       (expression? (list-ref x 1))
+       (expression? (list-ref x 2))))
+
+(define (expr-equal-lhs x)
+  (list-ref x 1))
+
+(define (expr-equal-rhs x)
+  (list-ref x 2))
+
+(define (expression->rules vars preconds expr)
+  (if (if-form? expr)
+      (append (expression->rules vars
+                                 (cons (prop-not
+                                        (prop-not
+                                         (if-form-test expr)))
+                                       preconds)
+                                 (if-form-then expr))
+              (expression->rules vars
+                                 (cons (prop-not (if-form-test expr))
+                                       preconds)
+                                 (if-form-else expr))
+              (expression->rules vars
+                                 preconds
+                                 (if-form-test expr)))
+      (if (expr-equal? expr)
+          (list (rule vars
+                      preconds
+                      (expr-equal-lhs expr)
+                      (expr-equal-rhs expr))
+                (rule vars
+                      preconds
+                      (expr-equal-rhs expr)
+                      (expr-equal-lhs expr)))
+          '())))
+
+(define (theorem->rules def)
+  (expression->rules (get-variables def)
+                     '()
+                     (get-expression def)))
+
+(define current-system (make-parameter (make <system>)))
+(define reserved-symbols '(quote let if error))
+(define (reserved? x)
+  (member x reserved-symbols))
+
+(define-syntax define-axiom
+  (syntax-rules ()
+    ((_ name (var ...) expr)
+     (let ((t (make <axiom>
+                #:name 'name
+                #:variables '(var ...)
+                #:expression (convert-to-expression 'expr))))
+       (current-system (add-definition t (current-system)))
+       (validate t)
+       t))))
+
+(define-syntax define-theorem
+  (syntax-rules ()
+    ((_ name (var ...) expr)
+     (let ((t (make <conjecture>
+                #:name 'name
+                #:variables '(var ...)
+                #:expression (convert-to-expression 'expr))))
+       (current-system (add-definition t (current-system)))
+       (validate t)
+       t))))
+
+(define-syntax define-core-function/guard
+  (syntax-rules (and)
+    ((_ name (var ...) (and guard ...) proc)
+     (let ((f (make <core-function>
+                #:name 'name
+                #:variables '(var ...)
+                #:guards (map convert-to-expression (list 'guard ...))
+                #:procedure proc)))
+       (current-system (add-definition f (current-system)))
+       (validate f)
+       f))
+    ((_ name (var ...) guard proc)
+     (define-core-function/guard name (var ...) (and guard) proc))))
+
+(define-syntax define-core-function
+  (syntax-rules ()
+    ((_ name (var ...) proc)
+     (define-core-function/guard name (var ...) (and) proc))))
+
+(define (recursive? f)
+  (member (get-name f) (expression-functions (get-expression f))))
+
+(define (has-guard-claim? f sys)
+  (let ((claim (make-guard-claim (get-expression f) sys)))
+    (not (equal? ''#t claim))))
+
+(define-syntax define-function/guard
+  (syntax-rules (and)
+    ((_ name (var ...) (and guard ...) expr)
+     (let* ((expression (convert-to-expression 'expr))
+            (guard-expressions (map convert-to-expression
+                                    (list 'guard ...)))
+            (f (make <function>
+                 #:name 'name
+                 #:variables '(var ...)
+                 #:guards guard-expressions
+                 #:expression expression
+                 #:code (code 'expr))))
+       (current-system (add-definition f (current-system)))
+       (validate f)
+       (when (and (not (recursive? f))
+                  (not (has-guard-claim? f (current-system))))
+         (let ((g (make <total-function>
+                    #:name (get-name f)
+                    #:variables (get-variables f)
+                    #:guards (get-guards f)
+                    #:expression (get-expression f)
+                    #:code (get-code f)
+                    #:claim ''#t
+                    #:proof '())))
+           (current-system (update-definition g (current-system)))
+           (validate g)))))
+    ((_ name (var ...) guard expr)
+     (define-function/guard name (var ...) (and guard) expr))))
+
+(define-syntax define-function
+  (syntax-rules ()
+    ((_ name (var ...) expr)
+     (define-function/guard name (var ...) (and) expr))))
+
+(define-syntax define-syntax-rules
+  (syntax-rules ()
+    ((_ name (l ...) ((lhs1 . lhs2) rhs) ...)
+     (let ((m (macro 'name
+                (list (mrule '(lhs1 . lhs2) 'rhs)
+                      ...)
+                '(l ...))))
+       (current-system (add-definition m (current-system)))
+       m))))
+
+(define-syntax admit
+  (syntax-rules (and)
+    ((_ name)
+     (cond
+      ((lookup 'name (current-system))
+       => (lambda (d)
+            (unless (or (is-a? d <conjecture>)
+                        (is-a? d <function>))
+              (raise-exception
+               (make-exception
+                (make-exception-with-origin 'name)
+                (make-exception-with-message "not provable definition")
+                (make-exception-with-irritants 'name))))
+            (let ((g (if (is-a? d <conjecture>)
+                         (make <admitted-theorem>
+                           #:name (get-name d)
+                           #:variables (get-variables d)
+                           #:expression (get-expression d)
+                           #:claim ''#t
+                           #:proof '())
+                         (make <admitted-function>
+                           #:name (get-name d)
+                           #:variables (get-variables d)
+                           #:guards (get-guards d)
+                           #:expression (get-expression d)
+                           #:code (get-code d)
+                           #:claim ''#t
+                           #:proof '()))))
+              (validate g)
+              (current-system (update-definition g (current-system))))))
+      (else
+       (raise-exception
+        (make-exception
+         (make-exception-with-origin 'name)
+         (make-exception-with-message "not found")
+         (make-exception-with-irritants 'name))))))))
+
+(define* (core-system #:optional (parent (make <system>)))
+  (parameterize ((current-system parent))
+    (define-syntax-rules and ()
+      ((and) '#t)
+      ((and x) x)
+      ((and x . xs) (if x (and . xs) #f)))
+    (define-core-function not (x) not)
+    (define-core-function equal? (x y) equal?)
+    (current-system)))
+
+(define-syntax define-system
+  (syntax-rules ()
+    ((_ name (systems ...) expr ...)
+     (define* (name #:optional (parent (core-system)))
+       (when (member 'name (list 'systems ...))
+         (raise-exception
+          (make-exception
+           (make-exception-with-origin 'name)
+           (make-exception-with-message "recursive system")
+           (make-exception-with-irritants '(systems ...)))))
+       (parameterize ((current-system
+                       ((compose systems ... identity) parent)))
+         expr
+         ...
+         (current-system))))))
+
+(define (validate-function-name desc name)
+  (define (err)
+    (raise-exception
+     (make-exception
+      (make-exception-with-origin 'desc)
+      (make-exception-with-message "unbound function")
+      (make-exception-with-irritants name))))
+  (cond
+   ((lookup name (current-system))
+    => (lambda (f)
+         (if (is-a? f <function*>)
+             name
+             (err))))
+   (else (err))))
+
+(define-syntax set-measure-predicate
+  (syntax-rules ()
+    ((_ name)
+     (begin
+       (validate-function-name 'set-measure-predicate 'name)
+       (current-system (update-measure-predicate 'name (current-system)))))))
+
+(define-syntax set-measure-less-than
+  (syntax-rules ()
+    ((_ name)
+     (begin
+       (validate-function-name 'set-measure-less-than 'name)
+       (current-system
+        (update-measure-less-than 'name (current-system)))))))
+
+(define (defined-function-app-form f)
+  (app-form (get-name f) (get-variables f)))
+
+(define (single? x)
+  (and (pair? x)
+       (null? (cdr x))))
+
+(define (smart-if x y z)
+  (cond
+   ((equal? y z) y)
+   ((equal? x ''#t) y)
+   ((equal? x ''#f) z)
+   (else `(if ,x ,y ,z))))
+
+(define (smart-and . args)
+  (cond
+   ((null? args) ''#t)
+   ((equal? ''#t (car args)) (apply smart-and (cdr args)))
+   (else
+    (let ((rest (apply smart-and (cdr args))))
+      (if (equal? ''#t rest)
+          (car args)
+          (smart-if (car args)
+                    rest
+                    ''#f))))))
+
+(define (smart-implies x y)
+  (cond
+   ((equal? ''#f x) ''#t)
+   ((equal? ''#t y) ''#t)
+   (else
+    (smart-if x y ''#t))))
+
+(define (make-totality-claim* sys m-expr f)
+  (let* ((name (get-name f)))
+    (define (convert app-form)
+      (cond
+       ((apply-rule '()
+                    (rule (get-variables f)
+                          '()
+                          (defined-function-app-form f)
+                          m-expr)
+                    app-form
+                    '())
+        => identity)
+       (else (error "make-totality-claim: convert error"
+                    (get-name f)
+                    m-expr
+                    app-form))))
+    (smart-if `(,(get-measure-predicate sys) ,m-expr)
+              (let loop ((expr (get-expression f)))
+                (cond
+                 ((expr-quoted? expr) ''#t)
+                 ((variable? expr) ''#t)
+                 ((if-form? expr)
+                  (let ((test/result (loop (if-form-test expr)))
+                        (then/result (loop (if-form-then expr)))
+                        (else/result (loop (if-form-else expr))))
+                    (smart-and test/result
+                               (smart-if (if-form-test expr)
+                                         then/result
+                                         else/result))))
+                 ((app-form? expr)
+                  (let ((rest
+                         (let f ((args (app-form-args expr)))
+                           (cond ((null? args) ''#t)
+                                 ((single? args) (loop (car args)))
+                                 (else (smart-and (loop (car args))
+                                                  (f (cdr args))))))))
+                    (if (eq? name (app-form-name expr))
+                        (smart-and `(,(get-measure-less-than sys)
+                                     ,(convert expr)
+                                     ,m-expr)
+                                   rest)
+                        rest)))
+                 (else (error "(vikalpa) make-totality-claim: error"
+                              (get-name f)
+                              m-expr))))
+              ''#f)))
+
+(define (make-guard-claim expr sys)
+  (define (find-preconds expr)
+    (cond
+     ((app-form? expr)
+      (let ((rest (append-map find-preconds (cdr expr))))
+        (append (cond ((lookup (car expr) sys) =>
+                       (lambda (f)
+                         (let ((preconds (get-guards f)))
+                           (map (lambda (precond)
+                                  (substitute (map cons
+                                                   (get-variables f)
+                                                   (cdr expr))
+                                              precond))
+                                preconds))))
+                      (else (error "make-guard-claim: error" (car expr))))
+                rest)))
+     ((if-form? expr)
+      (find-preconds (if-form-test expr)))
+     (else '())))
+  (define (build/find-if expr)
+    (cond
+     ((if-form? expr)
+      (smart-if (build/find-if (if-form-test expr))
+                (build (if-form-then expr))
+                (build (if-form-else expr))))
+     ((app-form? expr)
+      (apply smart-and (map build/find-if (app-form-args expr))))
+     (else ''#t)))
+  (define (build expr)
+    (cond
+     ((if-form? expr)
+      (apply smart-and
+             (append (find-preconds (if-form-test expr))
+                     (list (smart-if (if-form-test expr)
+                                     (build (if-form-then expr))
+                                     (build (if-form-else expr)))))))
+     ((app-form? expr)
+      (apply smart-and
+             (append (find-preconds expr)
+                     (list (build/find-if expr)))))
+     (else ''#t)))
+  (smart-if (build expr)
+            ''#t
+            ''#f))
+
+(define (make-induction-rule f vars c)
+  (unless (is-a? f <proved>)
+    (raise-exception
+     (make-exception
+      (make-exception-with-origin 'define-proof)
+      (make-exception-with-message
+       "measure function must be proved function")
+      (make-exception-with-irritants (get-name f)))))
+  (define (find-app-forms expr)
+    (cond
+     ((app-form? expr)
+      (let ((rest (append-map find-app-forms (cdr expr))))
+        (if (eq? (get-name f) (app-form-name expr))
+            (cons expr rest)
+            rest)))
+     ((if-form? expr)
+      (error "make-induction-claim(find-app-forms): not supported"
+             expr))
+     (else '())))
+  (define (prop form)
+    (cond
+     ((apply-rule '()
+                  (rule vars
+                        '()
+                        (app-form (get-name f) vars)
+                        c)
+                  form
+                  '())
+      => identity)
+     (else
+      (error "make-induction-claim: fail" app-form))))
+  (define rhs
+    (cond
+     ((apply-function f vars)
+      => (lambda (expr)
+           (let build ((expr expr))
+             (cond
+              ((if-form? expr)
+               (let ((app-forms (find-app-forms (if-form-test expr))))
+                 (smart-implies (if (null? app-forms)
+                                    ''#t
+                                    (fold smart-implies
+                                          c
+                                          (map prop app-forms)))
+                                (smart-if (if-form-test expr)
+                                          (build (if-form-then expr))
+                                          (build (if-form-else expr))))))
+              (else
+               (let ((app-forms (find-app-forms expr)))
+                 (fold smart-implies c (map prop app-forms))))))))
+     (else (error "make-induction-claim: invalid"
+                  f vars c))))
+  (rule vars (get-guards f) c rhs))
+
+(define (validate-sequence sys d seq)
+  (for-each (lambda (r)
+              (match r
+                (('rewrite _ _ . command-ops)
+                 (for-each (lambda (x)
+                             (match x
+                               (('set var expr)
+                                (validate-expression sys
+                                                     `(define-proof ,(get-name d))
+                                                     (get-variables d)
+                                                     expr))
+                               (else #f)))
+                           command-ops))
+                (else #f)))
+            seq))
+
+(define (add-proof/function sys f seed seq)
+  (define (update-claim claim)
+    (update-definition (make <total-function>
+                         #:name (get-name f)
+                         #:variables (get-variables f)
+                         #:guards (get-guards f)
+                         #:expression (get-expression f)
+                         #:code (get-code f)
+                         #:claim claim
+                         #:proof seq)
+                       sys))
+  (validate-sequence sys f seq)
+  (if (recursive? f)
+      (if seed
+          (begin
+            (validate-expression sys
+                                 `(defien-proof ,(get-name f))
+                                 (get-variables f)
+                                 seed)
+            (update-claim
+             (fold smart-implies
+                   (smart-and (make-totality-claim* sys seed f)
+                              (make-guard-claim (get-expression f)
+                                                sys))
+                   (get-guards f))))
+          (raise-exception
+           (make-exception
+            (make-exception-with-origin 'define-proof)
+            (make-exception-with-message "need measure expression")
+            (make-exception-with-irritants (get-expression f)))))
+      (update-claim
+       (fold smart-implies
+             (make-guard-claim (get-expression f) sys)
+             (get-guards f)))))
+
+(define (add-proof/theorem sys t seed seq)
+  (validate-sequence sys t seq)
+  (update-definition (make <theorem>
+                       #:name (get-name t)
+                       #:variables (get-variables t)
+                       #:expression (get-expression t)
+                       #:claim (get-expression t)
+                       #:proof seq)
+                     sys))
+
+(define (add-proof sys name seed seq)
+  (cond
+   ((not (sequence? seq))
+    (raise-exception
+     (make-exception
+      (make-exception-with-origin 'define-proof)
+      (make-exception-with-message "not sequence")
+      (make-exception-with-irritants seq))))
+   ((lookup name sys)
+    => (lambda (def)
+         (current-system
+          (if (and (is-a? def <provable>)
+                   (not (is-a? def <proved>)))
+              (cond
+               ((is-a? def <function>)
+                (add-proof/function sys def seed seq))
+               ((is-a? def <conjecture>)
+                (add-proof/theorem sys def seed seq))
+               (else
+                (raise-exception
+                 (make-exception
+                  (make-exception-with-origin 'define-proof)
+                  (make-exception-with-message "error")
+                  (make-exception-with-irritants def)))))
+              (raise-exception
+               (make-exception
+                (make-exception-with-origin 'define-proof)
+                (make-exception-with-message "not provable definition")
+                (make-exception-with-irritants def)))))))
+   (else
+    (raise-exception
+     (make-exception
+      (make-exception-with-origin 'define-proof)
+      (make-exception-with-message "definition is not found")
+      (make-exception-with-irritants name))))))
+
+(define-syntax define-proof
+  (syntax-rules ()
+    ((_ name
+        seed
+        seq)
+     (add-proof (current-system)
+                'name
+                'seed
+                'seq))
+    ((_ name seq)
+     (define-proof name #f seq))))
+
+(define (validate-expression/error sys name vars expr)
+  (with-exception-handler
+      (lambda (e)
+        (if (eq? 'validate-expression/error (exception-origin e))
+            `(error ,name ,vars ,expr))
+        (raise-exception e))
+    (lambda ()
+      (validate-expression sys 'validate-expression/error vars expr)
+      #f)))
+
+(define (validate-expression sys name vars expr)
+  (let* ((expr-fnames (expression-functions expr))
+         (expr-vars (expression-vars expr))
+         (expr-app-forms (expression-app-forms expr)))
+    (define (err msg x)
+      (raise-exception
+       (make-exception
+        (make-exception-with-origin name)
+        (make-exception-with-message msg)
+        (make-exception-with-irritants x))))
+    (for-each (lambda (x)
+                (when (member x expr-fnames)
+                  (err "invalid variable" x)))
+              vars)
+    (for-each (lambda (fname)
+                (unless (cond
+                         ((lookup fname sys) =>
+                          (lambda (f)
+                            (for-each
+                             (lambda (app-form)
+                               (when (equal? fname (app-form-name app-form))
+                                 (unless (= (length (get-variables f))
+                                            (length (app-form-args app-form)))
+                                   (err (format
+                                         #f
+                                         "~a :wrong number of arguments ~s"
+                                         (get-name f)
+                                         (get-variables f))
+                                        (app-form-args app-form)))))
+                             expr-app-forms)
+                            #t))
+                         (else #f))
+                  (err "undefined function" fname)))
+              expr-fnames)
+    (for-each (lambda (x)
+                (unless (member x vars)
+                  (err "undefined variable" x)))
+              expr-vars)))
+
+(define (dup? xs)
+  (if (null? xs)
+      #f
+      (if (member (car xs) (cdr xs))
+          #t
+          (dup? (cdr xs)))))
+
+(define (validate-vars desc vars)
+  (define (err)
+    (raise-exception
+     (make-exception
+      (make-exception-with-message
+       (string-append "(vikalpa) " desc ": duplicated variable"))
+      (make-exception-with-irritants vars))))
+  (when (dup? vars)
+    (err)))
+
+(define-method (get-type (s <axiom>)) 'axiom)
+(define-method (get-type (s <theorem>)) 'theorem)
+(define-method (get-type (s <conjecture>)) 'conjecture)
+(define-method (get-type (s <core-function>)) 'core-function)
+(define-method (get-type (s <function>)) 'function)
+(define-method (get-type (s <total-function>)) 'total-function)
+(define-method (get-type (s <admitted-function>)) 'admitted-function)
+(define-method (get-type (s <admitted-theorem>)) 'admitted-theorem)
+(define-method (get-type (s <macro>)) 'macro)
+
+(define-method (show (d <macro>))
+  (list (get-type d)))
+(define-method (show (d <theorem*>))
+  (list (get-type d)
+        (get-variables d)
+        (get-expression d)))
+(define-method (show (d <core-function>))
+  (list (get-type d)
+        (get-variables d)))
+(define-method (show (d <expandable-function>))
+  (list (get-type d)
+        (get-variables d)
+        (get-expression d)))
+(define-method (show (d <admitted-function>))
+  (list (get-type d)
+        (get-variables d)
+        (get-expression d)))
+
+(define* (system-apropos sys str)
+  (filter-map (lambda (d)
+                (let ((name (format #f "~a" (get-name d))))
+                  (if (string-match (string-append ".*"
+                                                   (regexp-quote str)
+                                                   ".*")
+                                    name)
+                      (list (get-name d) (show d))
+                      #f)))
+              (get-definitions sys)))
+
+(define (system-check sys)
+  (let loop ((sys sys)
+             (fails '()))
+    (if (system-empty? sys)
+        fails
+        (let ((d (first-definition sys))
+              (sys-without-first (remove-first-definition sys)))
+          (define* (next #:optional fail)
+            (loop sys-without-first
+                  (if fail
+                      (cons fail fails)
+                      fails)))
+          (cond
+           ((is-a? d <proved>)
+            (let ((result
+                   (if (is-a? d <theorem>)
+                       (rewrite sys-without-first
+                                (get-claim d)
+                                (get-proof d))
+                       (rewrite sys
+                                (get-claim d)
+                                (get-proof d)))))
+              (cond
+               ((equal? result (result/expr ''#t))
+                (next))
+               (else
+                (next (list (get-name d) result))))))
+           ((is-a? d <provable>)
+            (next (list (get-name d))))
+           (else (next)))))))
+
+(define (system? x)
+  (is-a? x <system>))
+
+(define/guard (system-lookup (sys system?) (name (const #t)))
+  (cond
+   ((lookup name sys) => show)
+   (else #f)))
+
+(define/guard (system-rewrite (sys system?) (expr (const #t)) (seq sequence?))
+  (rewrite sys (convert-to-expression expr) seq))