;;; 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 (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-equal '(result/expr (quote b)) (system-eval (test) '(if 'nil 'a 'b))) (test-end "test-vikalpa-equal-t-nil")