From 6f7d68bed5e0097257f1b36289f8af3b7efaa4ae Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sat, 7 Nov 2020 15:06:03 +0900 Subject: wip --- Makefile.am | 20 +- README.org | 4 +- configure.ac | 4 +- examples/prelude.scm | 411 ++++++++++ examples/the-little-prover.scm | 5 + guix.scm | 28 +- pre-inst-env.in | 10 +- rabbit-prover.scm | 20 - tests/test-vikalpa.scm | 44 ++ vikalpa.scm | 1605 ++++++++++++++++++++++++++++++++++++++++ 10 files changed, 2100 insertions(+), 51 deletions(-) create mode 100644 examples/prelude.scm create mode 100644 examples/the-little-prover.scm delete mode 100644 rabbit-prover.scm create mode 100644 tests/test-vikalpa.scm create mode 100644 vikalpa.scm 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 ## -## 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 . +## along with Vikalpa. If not, see . 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 +;;; +;;; 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 . + +(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 +;;; Vikalpa --- Proof Assistant +;;; Copyright © 2020, 2021 Masaya Tojo ;;; -;;; 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 . +;;; along with Vikalpa. If not, see . (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 # -# 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 . +# along with Vikalpa. If not, see . 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 -;;; -;;; 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 . - -(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 +;;; +;;; 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 . + +(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 +;;; +;;; 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 . + +(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 () + (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 () + (name #:getter get-name + #:init-keyword #:name) + (variables #:getter get-variables + #:init-keyword #:variables + #:init-value '())) + +(define-class ()) + +(define-class () + (claim #:getter get-claim #:init-keyword #:claim) + (proof #:getter get-proof #:init-keyword #:proof)) + +(define-class ()) + +(define-class () + (expression #:getter get-expression #:init-keyword #:expression)) + +(define-class ( )) +(define-class ( )) +(define-class ()) +(define-class ( )) + +(define-class () + (guards #:getter get-guards #:init-keyword #:guards)) +(define-class () + (procedure #:getter get-procedure #:init-keyword #:procedure)) +(define-class () + (expression #:getter get-expression #:init-keyword #:expression) + (code #:getter get-code #:init-keyword #:code)) +(define-class ( )) +(define-class ( )) +(define-class ( )) + +(define-class () + (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 ) port) + (format port "#" + (length (filter (cut is-a? <> ) + (get-definitions s))) + (length (filter (cut is-a? <> ) + (get-definitions s))) + (length (filter (cut is-a? <> ) + (get-definitions s))))) + +(define-method (write (s ) port) + (format port "#" + (length (filter (cut is-a? <> ) + (get-definitions s))) + (length (filter (cut is-a? <> ) + (get-definitions s))) + (length (filter (cut is-a? <> ) + (get-definitions s))))) + +(define-method (lookup name (s )) + (find (lambda (x) + (equal? name (get-name x))) + (get-definitions s))) + +(define-method (update-measure-predicate (s ) (sys )) + (let ((new (shallow-clone sys))) + (slot-set! new 'measure-predicate s) + new)) + +(define-method (update-measure-less-than (s ) (sys )) + (let ((new (shallow-clone sys))) + (slot-set! new 'measure-less-than s) + new)) + +(define-method (update-definition (d ) (sys )) + (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 )) + (let ((new (shallow-clone sys))) + (slot-set! new 'definitions + (cdr (get-definitions sys))) + new)) + +(define-method (first-definition (sys )) + (car (get-definitions sys))) + +(define-method (system-empty? (sys )) + (null? (get-definitions sys))) + +(define-method (add-definition (d ) (s )) + (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 )) + (let* ((vars (get-variables d)) + (name (get-name d))) + (validate-vars (format #f "~a" name) vars))) + +(define-method (validate (d )) + (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 )) + (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 () + (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 + #:vars var + #:preconds preconds + #:lhs lhs + #:rhs rhs)) + +(define (rule? x) + (is-a? x )) + +(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 () + (lhs #:getter mrule-lhs #:init-keyword #:lhs) + (rhs #:getter mrule-rhs #:init-keyword #:rhs)) + +(define (mrule lhs rhs) + (make #: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 + #: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? <> ) + (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 )) + (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 ) + (rewrite/core-function sys x extracted-expr)) + ((is-a? x ) + (rewrite/theorem cmd-name cmd-ops sys x preconds extracted-expr)) + ((is-a? x ) + (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 ))) +(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 + #: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 + #: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 + #: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 + #: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 + #: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 ) + (is-a? d )) + (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 ) + (make + #:name (get-name d) + #:variables (get-variables d) + #:expression (get-expression d) + #:claim ''#t + #:proof '()) + (make + #: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 ))) + (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 ) + 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 ) + (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 + #: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 + #: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 ) + (not (is-a? def ))) + (cond + ((is-a? def ) + (add-proof/function sys def seed seq)) + ((is-a? def ) + (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) +(define-method (get-type (s )) 'theorem) +(define-method (get-type (s )) 'conjecture) +(define-method (get-type (s )) 'core-function) +(define-method (get-type (s )) 'function) +(define-method (get-type (s )) 'total-function) +(define-method (get-type (s )) 'admitted-function) +(define-method (get-type (s )) 'admitted-theorem) +(define-method (get-type (s )) 'macro) + +(define-method (show (d )) + (list (get-type d))) +(define-method (show (d )) + (list (get-type d) + (get-variables d) + (get-expression d))) +(define-method (show (d )) + (list (get-type d) + (get-variables d))) +(define-method (show (d )) + (list (get-type d) + (get-variables d) + (get-expression d))) +(define-method (show (d )) + (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 ) + (let ((result + (if (is-a? d ) + (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 ) + (next (list (get-name d)))) + (else (next))))))) + +(define (system? x) + (is-a? x )) + +(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)) -- cgit v1.2.3