diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/test-vikalpa-equal-t-nil.scm | 432 |
1 files changed, 432 insertions, 0 deletions
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") |