diff options
Diffstat (limited to 'examples/prelude.scm')
| -rw-r--r-- | examples/prelude.scm | 411 |
1 files changed, 411 insertions, 0 deletions
diff --git a/examples/prelude.scm b/examples/prelude.scm new file mode 100644 index 0000000..077b90d --- /dev/null +++ b/examples/prelude.scm @@ -0,0 +1,411 @@ +;;; Vikalpa --- Proof Assistant +;;; Copyright © 2020, 2021 Masaya Tojo <masaya@tojo.tokyo> +;;; +;;; This file is part of Vikalpa. +;;; +;;; Vikalpa is free software; you can redistribute it and/or modify it +;;; under the terms of the GNU General Public License as published by +;;; the Free Software Foundation; either version 3 of the License, or +;;; (at your option) any later version. +;;; +;;; Vikalpa is distributed in the hope that it will be useful, but +;;; WITHOUT ANY WARRANTY; without even the implied warranty of +;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU +;;; General Public License for more details. +;;; +;;; You should have received a copy of the GNU General Public License +;;; along with Vikalpa. If not, see <http://www.gnu.org/licenses/>. + +(define-module (vikalpa prelude) + #:export (prelude) + #:use-module (vikalpa)) + +(define-syntax-rule (define-axiom/is p1 p2) + (define-axiom (is p1 p2) (x) (is (p1 x) (p2 x)))) + +(define-syntax-rule (define-theorem/is p1 p2) + (define-theorem (is p1 p2) (x) (is (p1 x) (p2 x)))) + +(define-syntax-rule (define-proof/is p1 p2 pc) + (define-proof (is p1 p2) + ((rewrite (2) if-same (set x (pc x))) + (rewrite (2 2 1) (is pc p2)) + (eval (2 2)) + (rewrite (2 1) (is p1 pc)) + (rewrite (2) if-true) + (rewrite () if-same)))) + +(define-syntax implies + (syntax-rules () + ((_ x y) (if x y #t)) + ((_ x y z ...) (if x (implies y z ...) #t)))) + +(define-system prelude/macro () + (define-syntax-rules cond (else) + ((cond (else e)) e) + ((cond (test then) . rest) + (if test then (cond . rest)))) + (define-syntax-rules or () + ((or) '#f) + ((or x) x) + ((or x . xs) (if x x (or . xs)))) + (define-syntax-rules implies () + ((implies x y) (if x y #t)) + ((implies x y z . rest) + (if x (implies y z . rest) #t))) + (define-syntax-rules predicate () + ((predicate x) (implies x (equal? x #t)))) + (define-syntax-rules is () + ((is x y) (implies x (equal? y #t))) + ((is x y . ys) (implies x (is y . ys))))) + +(define-system prelude/axiom/equal (prelude/macro) + (define-axiom equal-same (x) + (equal? (equal? x x) '#t)) + (define-axiom equal-swap (x y) + (equal? (equal? x y) (equal? y x))) + (define-axiom equal-if (x y) + (implies (equal? x y) (equal? x y))) + (define-axiom equal-if-false (x y) + (if x #t (equal? x #f)))) + +(define-system prelude/axiom/if (prelude/axiom/equal) + (define-axiom if-nest (x y z) + (if x + (equal? (if x y z) y) + (equal? (if x y z) z))) + (define-axiom if-true (x y) + (equal? (if '#t x y) x)) + (define-axiom if-false (x y) + (equal? (if '#f x y) y)) + (define-axiom if-same (x y) + (equal? (if x y y) y)) + (define-axiom if-not (x y z) + (equal? (if (not x) y z) + (if x z y)))) + +(define-system prelude/number (prelude/axiom/if) + (define-core-function number? (x) number?) + (define-axiom (predicate number?) (x) (predicate (number? x))) + + (define-core-function real? (x) real?) + (define-axiom (predicate real?) (x) (predicate (real? x))) + (define-axiom/is real? number?) + + (define-core-function integer? (x) integer?) + (define-axiom (predicate integer?) (x) (predicate (integer? x))) + (define-axiom/is integer? real?) + (define-theorem/is integer? number?) + (define-proof/is integer? number? real?) + + (define-core-function/guard exact? (x) (number? x) exact?) + (define-axiom (predicate exact?) (x) (predicate (exact? x))) + (define-function/guard inexact? (x) + (number? x) + (not (exact? x))) + (define-theorem (predicate inexact?) (x) (predicate (inexact? x))) + + (define-core-function exact-integer? (x) exact-integer?) + (define-axiom (predicate exact-integer?) (x) (predicate (exact-integer? x))) + (define-axiom/is exact-integer? integer?) + (define-axiom/is exact-integer? exact?) + (define-theorem/is exact-integer? real?) + (define-proof/is exact-integer? real? integer?) + (define-theorem/is exact-integer? number?) + (define-proof/is exact-integer? number? real?) + (define-core-function/guard < (x y) (and (real? x) (real? y)) <) + (define-axiom (predicate <) (x y) (predicate (< x y))) + + (define-function/guard positive? (x) + (real? x) + (< 0 x)) + (define-theorem (predicate positive?) (x) (predicate (positive? x))) + (define-function/guard negative? (x) + (real? x) + (< x 0)) + (define-theorem (predicate negative?) (x) (predicate (negative? x))) + (define-function exact-positive-integer? (x) + (and (exact-integer? x) + (positive? x))) + (define-theorem (predicate exact-positive-integer?) (x) + (predicate (exact-positive-integer? x))) + (define-theorem/is exact-positive-integer? exact-integer?) + (define-theorem/is exact-positive-integer? exact?) + (define-proof/is exact-positive-integer? exact? exact-integer?) + (define-theorem/is exact-positive-integer? integer?) + (define-proof/is exact-positive-integer? integer? exact-integer?) + (define-theorem/is exact-positive-integer? real?) + (define-proof/is exact-positive-integer? real? exact-integer?) + (define-theorem/is exact-positive-integer? number?) + (define-proof/is exact-positive-integer? number? exact-integer?) + + (define-function exact-zero? (x) (equal? x 0)) + (define-theorem (predicate exact-zero?) (x) + (predicate (exact-zero? x))) + (define-theorem/is exact-zero? exact-integer?) + (define-theorem/is exact-zero? integer?) + (define-proof/is exact-zero? integer? exact-integer?) + (define-theorem/is exact-zero? exact?) + (define-proof/is exact-zero? exact? exact-integer?) + (define-theorem/is exact-zero? real?) + (define-proof/is exact-zero? real? exact-integer?) + (define-theorem/is exact-zero? number?) + (define-proof/is exact-zero? number? real?) + + (define-function natural? (x) + (if (exact-zero? x) + #t + (exact-positive-integer? x))) + + (define-theorem (predicate natural?) (x) + (predicate (natural? x))) + (define-theorem/is natural? exact-integer?) + (define-theorem/is natural? integer?) + (define-proof/is natural? integer? exact-integer?) + (define-theorem/is natural? exact?) + (define-proof/is natural? exact? exact-integer?) + (define-theorem/is natural? real?) + (define-proof/is natural? real? exact-integer?) + (define-theorem/is natural? number?) + (define-proof/is natural? number? real?) + + (define-theorem/is exact-zero? natural?) + (define-theorem/is exact-positive-integer? natural?) + (set-measure-predicate natural?) + (set-measure-less-than <) + +(define-core-function/guard + (x y) (and (number? x) (number? y)) +) + (define-core-function/guard - (x y) (and (number? x) (number? y)) -) + (define-function/guard succ (x) (natural? x) (+ x 1)) + (define-function/guard pred (x) (exact-positive-integer? x) (- x 1)) + (define-function/guard natural-induction (x) + (natural? x) + (if (exact-zero? x) + #t + (succ (natural-induction (pred x))))) + (admit natural-induction) + + (define-axiom (+ natural? natural?) (x y) + (implies (natural? x) + (natural? y) + (equal? (+ x y) + (if (exact-zero? x) + y + (succ (+ (pred x) y)))))) + (define-axiom pred/succ (x) + (implies (natural? x) + (equal? (pred (succ x)) x))) + (define-theorem succ/pred (x) + (implies (exact-positive-integer? x) + (equal? (succ (pred x)) x))) + (define-theorem (is natural? (o natural? succ)) (x) + (is (natural? x) (natural? (succ x)))) + + (define-theorem (is (o natural? pred) natural?) (x) + (is (natural? (pred x)) + (natural? x))) + + (define-axiom pred/zero (x) + (equal? (natural? (pred 0)) #f)) + + (define-theorem (is (o not natural?) (o not natural? pred)) (x) + (is (not (natural? x)) + (not (natural? (pred x))))) + + (define-theorem (is (o natural?) + (o not exact-zero?) + exact-positive-integer?) + (x) + (is (not (natural? x)) + (not (exact-zero? x)) + (exact-positive-integer? x))) + + (define-function/guard natural-induction-+ (x y) + (and (natural? x) (natural? y)) + (if (exact-zero? x) + y + (succ (natural-induction-+ (pred x) y)))) + (admit natural-induction-+) + + (define-theorem (is natural? (o not exact-zero?) exact-positive-integer?) (x) + (is (natural? x) + (not (exact-zero? x)) + (exact-positive-integer? x))) + + (define-theorem (implies natural? + (equal? (o natural? pred) + exact-positive-integer?)) + (x) + (implies (natural? x) + (equal? (natural? (pred x)) + (exact-positive-integer? x)))) + + (define-theorem (+ (-> natural? natural? natural?)) (x y) + (implies (natural? x) + (natural? y) + (natural? (+ x y))))) + +(define-system prelude/measure/natural (prelude/number) + (set-measure-predicate natural?) + (set-measure-predicate <)) + +(define-system prelude/pair (prelude/measure/natural) + (define-core-function pair? (x) pair?) + (define-core-function cons (x y) cons) + (define-core-function/guard car (x) (pair? x) car) + (define-core-function/guard cdr (x) (pair? x) cdr) + (define-function size (x) + (if (pair? x) + (+ (size (car x)) + (size (cdr x))) + 1)) + (admit size)) + + +(define-system prelude (prelude/pair) + (define-proof inexact? + ((rewrite (2) if-nest) + (rewrite () if-same))) + (define-proof (predicate inexact?) + ((rewrite (1) inexact?) + (rewrite () if-not) + (rewrite (3 1) inexact?) + (rewrite (3 1 1) equal-if-false) + (eval (3)) + (rewrite () if-same))) + (define-proof positive? + ((eval (2 1 1)) + (rewrite (2 1) if-true) + (rewrite (2) if-nest) + (rewrite () if-same))) + (define-proof (predicate positive?) + ((rewrite (1) positive?) + (rewrite (2 1) positive?) + (rewrite (2 1) (predicate <)) + (eval (2)) + (rewrite () if-same))) + (define-proof negative? + ((rewrite (2 1) if-nest) + (eval (2 1)) + (rewrite (2) if-true) + (rewrite () if-same))) + (define-proof (predicate negative?) + ((rewrite (1) negative?) + (rewrite (2 1) negative?) + (rewrite (2 1) (predicate <)) + (eval (2)) + (rewrite () if-same))) + (define-proof exact-positive-integer? + ((rewrite (1 2) (is exact-integer? real?)) + (rewrite (1) if-same) + (eval ()))) + (define-proof (predicate exact-positive-integer?) + ((rewrite (1) exact-positive-integer?) + (rewrite () if-same (set x (exact-integer? x))) + (rewrite (3 1) if-nest) + (rewrite (3) if-false) + (rewrite (2 1) if-nest) + (rewrite (2 2 1) exact-positive-integer?) + (rewrite (2 2 1 1) (predicate exact-integer?)) + (rewrite (2 2 1 2) (predicate positive?)) + (eval (2 2)) + (rewrite (2) if-same) + (rewrite () if-same))) + (define-proof (predicate exact-zero?) + ((rewrite (1) exact-zero?) + (rewrite (2 1 1) equal-if) + (eval (2)) + (rewrite () if-same))) + (define-proof (predicate natural?) + ((rewrite (1) natural?) + (rewrite () if-same (set x (exact-zero? x))) + (rewrite (2 1) if-nest) + (rewrite (2) if-true) + (rewrite (3 1) if-nest) + (rewrite (1) exact-zero?) + (rewrite (2 1 1) equal-if) + (eval (2)) + (rewrite (1) exact-zero?) + (rewrite (3 2 1) natural?) + (rewrite (3 2 1) if-nest) + (rewrite (3 2 1) (predicate exact-positive-integer?)) + (eval (3 2)) + (rewrite (3) if-same) + (rewrite () if-same))) + (define-proof (is exact-positive-integer? exact-integer?) + ((rewrite (1) exact-positive-integer?) + (rewrite () if-same (set x (exact-integer? x))) + (rewrite (3 1) if-nest) + (rewrite (2 1) if-nest) + (rewrite (2 2 1) (predicate exact-integer?)) + (eval (2 2)) + (rewrite (2) if-same) + (rewrite (3) if-false) + (rewrite () if-same))) + (define-proof (is exact-zero? exact-integer?) + ((rewrite (1) exact-zero?) + (rewrite (2 1 1) equal-if) + (eval (2)) + (rewrite () if-same))) + (define-proof (is natural? exact-integer?) + ((rewrite (1) natural?) + (rewrite () if-same (set x (exact-zero? x))) + (rewrite (2 1) if-nest) + (rewrite (2) if-true) + (rewrite (2 1) (is exact-zero? exact-integer?)) + (eval (2)) + (rewrite (3 1) if-nest) + (rewrite (3 2 1) (is exact-positive-integer? exact-integer?)) + (eval (3 2)) + (rewrite (3) if-same) + (rewrite () if-same))) + (define-proof succ + ((rewrite (2 1 1) (is natural? number?)) + (eval (2)) + (rewrite () if-same))) + (define-proof pred + ((rewrite (2 1 1) (is exact-positive-integer? number?)) + (eval (2)) + (rewrite () if-same))) + + (define-proof (+ (-> natural? natural? natural?)) + ((induction (2 2) (natural-induction-+ x y)) + (rewrite (2 2 2 1) (+ natural? natural?)) + (rewrite (2 2 2 1) if-nest) + (rewrite (2 2 2) (predicate natural?)) + (rewrite (2 2 3 2) if-same (set x (natural? (pred x)))) + (rewrite (2 2 3 2 2 1) (+ natural? natural?)) + (rewrite (2 2 3 2 2 1) if-nest) + (rewrite (2 2 3 2 2) (is natural? (o natural? succ))) + (rewrite (2 2 3 2 1) (implies natural? + (equal? (o natural? pred) + exact-positive-integer?))) + (rewrite (2 2 3 2 1) (is natural? (o not exact-zero?) + exact-positive-integer?)) + (rewrite (2 2 3 2) if-true) + (rewrite (2 2 3) if-same) + (rewrite (2 2) if-same) + (rewrite (2) if-same) + (rewrite () if-same))) + + (define-proof (is exact-zero? natural?) + ((rewrite (1) exact-zero?) + (rewrite (2 1 1) equal-if) + (eval (2)) + (rewrite () if-same))) + + (define-proof (is exact-positive-integer? natural?) + ((rewrite (2 1) natural?) + (rewrite (2 1 3) (predicate exact-positive-integer?)) + (rewrite (2 1) if-same) + (eval (2)) + (rewrite () if-same))) + + (define-proof (is (o natural? pred) natural?) + ((rewrite () if-same (set x (natural? x))) + (rewrite (2 2 1) (predicate natural?)) + (eval (2 2)) + (rewrite (3 2 1) equal-if-false) + (eval (3 2)) + (rewrite (2) if-same))) + (admit (is natural? (o natural? succ)))) |