diff options
| -rw-r--r-- | Makefile.am | 5 | ||||
| -rw-r--r-- | tests/test-vikalpa-equal-t-nil.scm | 432 | ||||
| -rw-r--r-- | vikalpa.scm | 91 |
3 files changed, 491 insertions, 37 deletions
diff --git a/Makefile.am b/Makefile.am index 4d43492..44052ed 100644 --- a/Makefile.am +++ b/Makefile.am @@ -44,8 +44,9 @@ bin_SCRIPTS = SOURCES = \ vikalpa.scm -TESTS = \ - tests/test-vikalpa.scm +TESTS = \ + tests/test-vikalpa.scm \ + tests/test-vikalpa-equal-t-nil.scm TEST_EXTENSIONS = .scm diff --git a/tests/test-vikalpa-equal-t-nil.scm b/tests/test-vikalpa-equal-t-nil.scm new file mode 100644 index 0000000..251fd10 --- /dev/null +++ b/tests/test-vikalpa-equal-t-nil.scm @@ -0,0 +1,432 @@ +;;; Vikalpa --- Proof Assistant +;;; Copyright © 2020, 2021 Masaya Tojo <masaya@tojo.tokyo> +;;; +;;; This file is part of Vikalpa. +;;; +;;; Vikalpa is free software; you can redistribute it and/or modify it +;;; under the terms of the GNU General Public License as published by +;;; the Free Software Foundation; either version 3 of the License, or +;;; (at your option) any later version. +;;; +;;; Vikalpa is distributed in the hope that it will be useful, but +;;; WITHOUT ANY WARRANTY; without even the implied warranty of +;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU +;;; General Public License for more details. +;;; +;;; You should have received a copy of the GNU General Public License +;;; along with Vikalpa. If not, see <http://www.gnu.org/licenses/>. + +(define-module (tests vikalpa-equal-t-nil) + #:use-module (srfi srfi-64) + #:use-module (vikalpa)) + +(define-syntax-rule (if/nil test t f) + (if (equal? test 'nil) + f + t)) + +(define (bool->t/nil x) + (if x + 't + 'nil)) + +(define-system test/defs (core-system/equal-t-nil) + (define-syntax-rules implies () + ((implies x y) (if x y 't)) + ((implies x y z . rest) + (if x (implies y z . rest) 't))) + (define-axiom equal-same (x) + (equal (equal x x) 't)) + (define-axiom equal-swap (x y) + (equal (equal x y) (equal y x))) + (define-axiom equal-if (x y) + (implies (equal x y) (equal x y))) + (define-axiom equal-if-false (x y) + (if x 't (equal x 'nil))) + (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 'nil x y) y)) + (define-axiom if-same (x y) + (equal (if x y y) y)) + (define-axiom if-not (x y z) + (equal (if (not x) y z) + (if x z y))) + (define-core-function natural? (x) + (lambda (x) + (bool->t/nil (and (exact-integer? x) + (<= 0 x))))) + (define-core-function/guard < (x y) + (and (natural? x) (natural? y)) + (lambda (x y) + (bool->t/nil (< x y)))) + (define-core-function/guard + (x y) + (and (natural? x) (natural? y)) + +) + (set-measure-predicate natural?) + (set-measure-less-than <) + (define-core-function pair? (x) (compose bool->t/nil pair?)) + (define-core-function cons (x y) cons) + (define-core-function/guard car (x) (pair? x) car) + (define-core-function/guard cdr (x) (pair? x) cdr) + (define-axiom (car cons) (x y) + (equal (car (cons x y)) x)) + (define-axiom (cdr cons) (x y) + (equal (cdr (cons x y)) y)) + (define-axiom (pair? cons) (x y) + (equal (pair? (cons x y)) 't)) + (define-axiom (eliminate cons) (x) + (implies (pair? x) + (equal (cons (car x) (cdr x)) x))) + (define-axiom (predicate pair?) (x) + (implies (pair? x) (equal (pair? x) 't))) + + (define-function size (x) + (if (pair? x) + (+ (size (car x)) + (size (cdr x))) + 1)) + (admit size) + (define-axiom (natural? size) (x) + (equal (natural? (size x)) 't)) + (define-axiom (< size car) (x) + (implies (natural? x) + (equal (< (size (car x)) (size x)) 't))) + (define-axiom (< size cdr) (x) + (implies (pair? x) + (equal (< (size (cdr x)) (size x)) 't))) + (define-guard-theorem size) + + (define-function null? (x) + (equal x '())) + (define-theorem (predicate null?) (x) + (implies (null? x) (equal (null? x) 't))) + (define-theorem (substitute null?) (x) + (implies (null? x) (equal x '()))) + + (define-function cdr-induction (x) + (if (pair? x) + (cons (car x) (cdr-induction (cdr x))) + '())) + (define-guard-theorem cdr-induction) + + (define-function list? (x) + (if (null? x) + 't + (if (pair? x) + (list? (cdr x)) + 'nil))) + (define-guard-theorem list?) + + (define-theorem (predicate list?) (x) + (implies (list? x) (equal (list? x) 't))) + (define-theorem (is null? list?) (x) + (implies (null? x) (equal (list? x) 't))) + (define-theorem (is pair? (o list? cdr) list?) (x) + (implies (pair? x) + (list? (cdr x)) + (equal (list? x) 't))) + (define-theorem (is list? (o not null?) pair?) (x) + (implies (list? x) + (not (null? x)) + (equal (pair? x) 't))) + + (define-theorem (is-not pair? null?) (x) + (implies (pair? x) + (equal (null? x) 'nil))) + + (define-theorem (is list? pair? (o list? cdr)) (x) + (implies (list? x) + (pair? x) + (equal (list? (cdr x)) 't))) + + (define-theorem (is list? (o not pair?) null?) (x) + (implies (list? x) + (not (pair? x)) + (equal (null? x) 't))) + + (define-function/guard append (x y) + (and (list? x) (list? y)) + (if (null? x) + y + (cons (car x) (append (cdr x) y)))) + (define-guard-theorem append) + + (define-theorem (substitute (append null? _)) (x) + (equal (append '() x) x)) + + (define-theorem (associative append) (x y z) + (implies (list? x) + (list? y) + (list? z) + (equal (append (append x y) z) + (append x (append y z)))))) + +(define-system test/proofs (test/defs) + (define-proof (predicate null?) + ((rewrite (1) null?) + (rewrite (2 1 1) equal-if) + (eval (2 1)) + (rewrite (2) equal-same) + (rewrite () if-same))) + + (define-proof (guard size) + ((rewrite (2 1) (natural? size)) + (rewrite (2 2 1) (natural? size)) + (rewrite (2 2 2 1) (predicate pair?)) + (rewrite (2 2 2 2) (predicate pair?)) + (eval (2)) + (rewrite () if-same))) + + (define-proof (guard cdr-induction) + ((rewrite (2) if-nest) + (rewrite (2) (predicate pair?)) + (rewrite () if-same))) + + (define-proof list? + (size x) + ((rewrite (1) (natural? size)) + (rewrite () if-true) + (rewrite (3 2) (< size cdr)) + (rewrite (3) if-same) + (rewrite () if-same))) + + (define-proof (guard list?) + ((rewrite (3 2) (predicate pair?)) + (rewrite (3) if-same) + (rewrite () if-same))) + + (define-proof (substitute null?) + ((rewrite (1) null?) + (rewrite (2 1) equal-if) + (eval (2)) + (rewrite () if-same))) + + (define-proof (predicate list?) + (cdr-induction x) + ((rewrite (2) if-same (= x (list? (cdr x)))) + (rewrite (2 2 1) if-nest) + (rewrite (2 2 2 2 1) list?) + (rewrite (2 2 2 2 1 3 2) equal-if) + (rewrite (2 2 2 2 1 3) if-nest) + (rewrite (2 2 2 2 1) if-same) + (rewrite (2 2 2 2) equal-same) + (rewrite (2 2 2) if-same) + (rewrite (2 2) if-same) + (rewrite (2 3 1) if-nest) + (rewrite (2 3) if-true) + (rewrite (2 3 1) list?) + (rewrite (2 3 1 3) if-nest) + (rewrite (2 3) if-same (= x (null? x))) + (rewrite (2 3 2 1) if-nest) + (rewrite (2 3 2) if-true) + (rewrite (2 3 2 1 1) (substitute null?)) + (eval (2 3 2)) + (rewrite (2 3 3 1) if-nest) + (rewrite (2 3 3) if-nest) + (rewrite (2 3) if-same) + (rewrite (2) if-same) + (rewrite (3 1) list?) + (rewrite (3) if-same (= x (null? x))) + (rewrite (3 2 1) if-nest) + (rewrite (3 2) if-true) + (rewrite (3 2 1 1) (substitute null?)) + (eval (3 2)) + (rewrite (3 3 1) if-nest) + (rewrite (3 3 1) if-nest) + (rewrite (3 3) if-false) + (rewrite (3) if-same) + (rewrite () if-same))) + + (define-proof (is null? list?) + ((rewrite (1) null?) + (rewrite (2 1 1) equal-if) + (eval (2)) + (rewrite () if-same))) + + (define-proof (is pair? (o list? cdr) list?) + ((rewrite (2 2 1) list?) + (rewrite (2 2 1 3 2) (predicate list?)) + (rewrite (2 2 1 3) if-nest) + (rewrite (2 2 1) if-same) + (rewrite (2 2) equal-same) + (rewrite (2) if-same) + (rewrite () if-same))) + + (define-proof cdr-induction + (size x) + ((rewrite (1) (natural? size)) + (rewrite () if-true) + (rewrite (2) (< size cdr)) + (rewrite () if-same))) + + (define-proof (is list? (o not null?) pair?) + ((rewrite (2) if-not) + (rewrite (1) list?) + (rewrite () if-same (= x (null? x))) + (rewrite (2 1) if-nest) + (rewrite (2) if-true) + (rewrite (2) if-nest) + (rewrite (3 1) if-nest) + (rewrite (3) if-same (= x (pair? x))) + (rewrite (3 2 1) if-nest) + (rewrite (3 2 2 3 1) (predicate pair?)) + (rewrite (3 2 2 3) equal-same) + (rewrite (3 2 2) if-same) + (rewrite (3 2) if-same) + (rewrite (3 3 1) if-nest) + (rewrite (3 3) if-false) + (rewrite (3) if-same) + (rewrite () if-same))) + + (define-proof (is-not pair? null?) + ((rewrite () if-same (= x (null? x))) + (rewrite (2 1 1) (substitute null?)) + (eval (2 1)) + (rewrite (2) if-false) + (rewrite (3 2 1) equal-if-false) + (rewrite (3 2) equal-same) + (rewrite (3) if-same) + (rewrite () if-same))) + + (define-proof (is list? pair? (o list? cdr)) + ((rewrite () if-same (= x (pair? x))) + (rewrite (2 2) if-nest) + (rewrite (3 2) if-nest) + (rewrite (3) if-same) + (rewrite (2 1) list?) + (rewrite (2 1 1) (is-not pair? null?)) + (rewrite (2 1) if-false) + (rewrite (2 1) if-nest) + (rewrite (2 2 1) (predicate list?)) + (eval (2 2)) + (rewrite (2) if-same) + (rewrite () if-same))) + + (define-proof append + (size x) + ((rewrite (2 2 1) (natural? size)) + (rewrite (2 2) if-true) + (rewrite (2 2 3) if-same (= x (pair? x))) + (rewrite (2 2 3 2) (< size cdr)) + (rewrite (2 2 3 1) (is list? (o not null?) pair?)) + (rewrite (2 2 3) if-true) + (rewrite (2 2) if-same) + (rewrite (2) if-same) + (rewrite () if-same))) + + (define-proof (guard append) + ((rewrite (2 2 3 2 2 2) (predicate pair?)) + (rewrite (2 2 3 2 2) if-nest) + (rewrite (2 2 3 2 1) (is list? pair? (o list? cdr))) + (rewrite (2 2 3 2) if-true) + (rewrite (2 2 3 1) (is list? (o not null?) pair?)) + (rewrite (2 2 3) if-true) + (rewrite (2 2) if-same) + (rewrite (2) if-same) + (rewrite () if-same))) + + (define-proof (is list? (o not pair?) null?) + ((rewrite (2) if-not) + (rewrite () if-same (= x (pair? x))) + (rewrite (2 2) if-nest) + (rewrite (2) if-same) + (rewrite (3 2) if-nest) + (rewrite (3 1) list?) + (rewrite (3) if-same (= x (null? x))) + (rewrite (3 2 1) if-nest) + (rewrite (3 2) if-true) + (rewrite (3 2 1) (predicate null?)) + (eval (3 2)) + (rewrite (3 3 1) if-nest) + (rewrite (3 3 1) if-nest) + (rewrite (3 3) if-false) + (rewrite (3) if-same) + (rewrite () if-same))) + + (define-proof (substitute (append null? _)) + ((rewrite (1) append) + (eval (1 1)) + (rewrite (1) if-true) + (rewrite () equal-same))) + + (define-proof (associative append) + (cdr-induction x) + ((rewrite (3 2 2 2) if-same (= x (null? x))) + (rewrite (3 2 2 2 2 1 1 1) (substitute null?)) + (rewrite (3 2 2 2 2 2 1) (substitute null?)) + (rewrite (3 2 2 2 1) (is list? (o not pair?) null?)) + (rewrite (3 2 2 2) if-true) + (rewrite (3 2 2 2 1 1) (substitute (append null? _))) + (rewrite (3 2 2 2 2) (substitute (append null? _))) + (rewrite (3 2 2 2) equal-same) + (rewrite (3 2 2) if-same) + (rewrite (3 2) if-same) + (rewrite (3) if-same) + (rewrite (2) if-same (= x (list? y))) + (rewrite (2 2 1 2) if-nest) + (rewrite (2 2 2 2) if-nest) + (rewrite (2 3 1 2) if-nest) + (rewrite (2 3 2 2) if-nest) + (rewrite (2 3 1) if-same) + (rewrite (2 3) if-true) + (rewrite (2 3) if-same) + (rewrite (2 2) if-same (= x (list? z))) + (rewrite (2 2 2 1 2) if-nest) + (rewrite (2 2 2 2 2) if-nest) + (rewrite (2 2 3 1 2) if-nest) + (rewrite (2 2 3 2 2) if-nest) + (rewrite (2 2 3 1) if-same) + (rewrite (2 2 3) if-true) + (rewrite (2 2 3) if-same) + (rewrite (2 2 2) if-same (= x (list? (cdr x)))) + (rewrite (2 2 2 2 1) if-nest) + (rewrite (2 2 2 3 1) if-nest) + (rewrite (2 2 2 3) if-true) + (rewrite (2 2 2 2 2 2 2) append) + (rewrite (2 2 2 2 2 2 2 1) (is-not pair? null?)) + (rewrite (2 2 2 2 2 2 2) if-false) + (rewrite (2 2 2 2 2 2 2 2) equal-if) + (rewrite (2 2 2 2 2 2 1 1) append) + (rewrite (2 2 2 2 2 2 1 1 1) (is-not pair? null?)) + (rewrite (2 2 2 2 2 2 1 1) if-false) + (rewrite (2 2 2 2 2 2 1) append) + (rewrite (2 2 2 2 2 2 1) if-same + (= x (pair? (cons (car x) (append (cdr x) y))))) + (rewrite (2 2 2 2 2 2 1 2 1) (is-not pair? null?)) + (rewrite (2 2 2 2 2 2 1 1) (pair? cons)) + (rewrite (2 2 2 2 2 2 1) if-true) + (rewrite (2 2 2 2 2 2 1) if-false) + (rewrite (2 2 2 2 2 2 1 1) (car cons)) + (rewrite (2 2 2 2 2 2 1 2 1) (cdr cons)) + (rewrite (2 2 2 2 2 2) equal-same) + (rewrite (2 2 2 2 2) if-same) + (rewrite (2 2 2 2) if-same) + (rewrite (2 2 2) if-same (= x (list? x))) + (rewrite (2 2 2 2 1) (is list? pair? (o list? cdr))) + (rewrite (2 2 2 2) if-true) + (rewrite (2 2 2 3 3) if-nest) + (rewrite (2 2 2 3) if-same) + (rewrite (2 2 2) if-same) + (rewrite (2 2) if-same) + (rewrite (2) if-same) + (rewrite () if-same)))) + +(define-system test (test/proofs)) + +(test-begin "test-vikalpa-equal-t-nil") + +(test-equal '(result/expr b) + (system-rewrite (test) + '(car (cdr (cons a (cons b c)))) + '((rewrite (1) (cdr cons)) + (rewrite () (car cons))))) + +(test-equal '() + (system-check (test))) + +(test-end "test-vikalpa-equal-t-nil") diff --git a/vikalpa.scm b/vikalpa.scm index 6a2af81..8c3d10c 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -26,7 +26,7 @@ set-measure-predicate set-measure-less-than core-system - core-system/equal + core-system/equal-t-nil define-system define-proof define-core-function @@ -61,12 +61,22 @@ #:init-keyword #:definitions #:init-value '()) (equal-symbol #:getter get-equal-symbol - #:init-value 'equal?) + #:init-value 'equal? + #:init-keyword #:equal-symbol) + (true-object #:getter get-true-object + #:init-value ''#t + #:init-keyword #:true-object) + (false-object #:getter get-false-object + #:init-value ''#f + #:init-keyword #:false-object) (measure-predicate #:getter get-measure-predicate #:init-value #f) (measure-less-than #:getter get-measure-less-than #:init-value #f)) +(define-syntax-rule (true) (get-true-object (current-system))) +(define-syntax-rule (false) (get-false-object (current-system))) + (define-class <definition> () (name #:getter get-name #:init-keyword #:name) @@ -132,11 +142,6 @@ (equal? name (get-name x))) (get-definitions s))) -(define-method (update-equal-symbol (s <symbol>) (sys <system>)) - (let ((new (shallow-clone sys))) - (slot-set! new 'equal-symbol s) - new)) - (define-method (update-measure-predicate (s <symbol>) (sys <system>)) (let ((new (shallow-clone sys))) (slot-set! new 'measure-predicate s) @@ -1075,7 +1080,7 @@ #:guards (get-guards f) #:expression (get-expression f) #:code (get-code f) - #:claim ''#t + #:claim (true) #:proof '()))) (current-system (update-definition g (current-system))) (validate g))) @@ -1116,7 +1121,7 @@ #:name (get-name d) #:variables (get-variables d) #:expression (get-expression d) - #:claim ''#t + #:claim (true) #:proof '()) (make <admitted-function> #:name (get-name d) @@ -1124,7 +1129,7 @@ #:guards (get-guards d) #:expression (get-expression d) #:code (get-code d) - #:claim ''#t + #:claim (true) #:proof '())))) (validate g) (current-system (update-definition g (current-system)))))) @@ -1145,15 +1150,24 @@ (define-core-function equal? (x y) equal?) (current-system))) -(define (core-system/equal) - (parameterize ((current-system (make <system>))) - (current-system (update-equal-symbol 'equal (current-system))) +(define (core-system/equal-t-nil) + (parameterize ((current-system (make <system> + #:equal-symbol 'equal + #:true-object ''t + #:false-object ''nil))) (define-syntax-rules and () - ((and) '#t) + ((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?) + ((and x . xs) (if x (and . xs) 'nil))) + (define-core-function equal (x y) (lambda (x y) + (if (equal? x y) + 't + 'nil))) + (define-core-function not (x) + (lambda (x) + (if (eq? x 'nil) + 't + 'nil))) (current-system))) (define-syntax define-system @@ -1216,28 +1230,28 @@ (define (smart-if x y z) (cond ((equal? y z) y) - ((equal? x ''#t) y) - ((equal? x ''#f) z) + ((equal? x (true)) y) + ((equal? x (false)) z) (else `(if ,x ,y ,z)))) (define (smart-and . args) (cond - ((null? args) ''#t) - ((equal? ''#t (car args)) (apply smart-and (cdr args))) + ((null? args) (true)) + ((equal? (true) (car args)) (apply smart-and (cdr args))) (else (let ((rest (apply smart-and (cdr args)))) - (if (equal? ''#t rest) + (if (equal? (true) rest) (car args) (smart-if (car args) rest - ''#f)))))) + (false))))))) (define (smart-implies x y) (cond - ((equal? ''#f x) ''#t) - ((equal? ''#t y) ''#t) + ((equal? (false) x) (true)) + ((equal? (true) y) (true)) (else - (smart-if x y ''#t)))) + (smart-if x y (true))))) (define (make-totality-claim* m-expr f) (let* ((name (get-name f))) @@ -1258,8 +1272,8 @@ (smart-if `(,(get-measure-predicate (current-system)) ,m-expr) (let loop ((expr (get-expression f))) (cond - ((expr-quoted? expr) ''#t) - ((variable? expr) ''#t) + ((expr-quoted? expr) (true)) + ((variable? expr) (true)) ((if-form? expr) (let ((test/result (loop (if-form-test expr))) (then/result (loop (if-form-then expr))) @@ -1271,7 +1285,7 @@ ((app-form? expr) (let ((rest (let f ((args (app-form-args expr))) - (cond ((null? args) ''#t) + (cond ((null? args) (true)) ((single? args) (loop (car args))) (else (smart-and (loop (car args)) (f (cdr args)))))))) @@ -1284,7 +1298,7 @@ (else (error "(vikalpa) make-totality-claim: error" (get-name f) m-expr)))) - ''#f))) + (false)))) (define (make-guard-claim expr) (define (find-preconds expr) @@ -1313,7 +1327,7 @@ (build (if-form-else expr)))) ((app-form? expr) (apply smart-and (map build/find-if (app-form-args expr)))) - (else ''#t))) + (else (true)))) (define (build expr) (cond ((if-form? expr) @@ -1326,7 +1340,7 @@ (apply smart-and (append (find-preconds expr) (list (build/find-if expr))))) - (else ''#t))) + (else (true)))) (build expr)) (define (make-induction-claim f vars c) @@ -1368,7 +1382,7 @@ ((if-form? expr) (let ((app-forms (find-app-forms (if-form-test expr)))) (smart-implies (if (null? app-forms) - ''#t + (true) (fold smart-implies c (map prop app-forms))) @@ -1607,7 +1621,7 @@ (if (lookup `(guard ,(get-name f)) (current-system)) #f (if (equal? (make-guard-claim (get-expression f)) - ''#t) + (true)) #f `((guard ,(get-name f)) (add (define-guard-theorem ,(get-name f))))))) @@ -1639,8 +1653,15 @@ (parameterize ((current-system sys)) (rewrite (get-claim d) (get-proof d)))))) + (display + (list result + (parameterize ((current-system sys)) + (result/expr (true))))) + (newline) (cond - ((equal? result (result/expr ''#t)) + ((equal? result + (parameterize ((current-system sys)) + (result/expr (true)))) (next)) (else (next (list (get-name d) result)))))) |