diff options
Diffstat (limited to 'vikalpa/prelude.scm')
| -rw-r--r-- | vikalpa/prelude.scm | 534 |
1 files changed, 107 insertions, 427 deletions
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 66d2b73..176983c 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -1,5 +1,5 @@ ;;; Vikalpa --- Proof Assistant -;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo> +;;; Copyright © 2020, 2021 Masaya Tojo <masaya@tojo.tokyo> ;;; ;;; This file is part of Vikalpa. ;;; @@ -48,25 +48,23 @@ ((_ x y) (if x y #t)) ((_ x y z ...) (if x (implies y z ...) #t)))) -(define-system prelude/macros () - (define-syntax-rules and () - ((and) '#t) - ((and x) x) - ((and x . xs) (if x (and . xs) #f))) - (define-syntax-rules or () - ((or) '#f) - ((or x) x) - ((or x . xs) (if x x (or . xs)))) +(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)))) + (if x (implies y z . rest) #t))) + (define-syntax-rules is-a () + ((is-a x y) (implies x (equal? y #t))))) -(define-system prelude/equal (prelude/macros) +(define-system prelude/axiom/equal (prelude/macro) (define-axiom equal-same (x) (equal? (equal? x x) '#t)) (define-axiom equal-swap (x y) @@ -76,7 +74,7 @@ (define-axiom equal-if-false (x y) (if x #t (equal? x #f)))) -(define-system prelude/if (prelude/equal) +(define-system prelude/axiom/if (prelude/axiom/equal) (define-axiom if-nest (x y z) (if x (equal? (if x y z) y) @@ -91,426 +89,108 @@ (equal? (if (not x) y z) (if x z y)))) -(define-system prelude/integer (prelude/if) - (define-core-function integer? (x) exact-integer?) - (define-core-function positive-integer? (x) exact-positive-integer?) - (define-function zero? (x) - (equal? x 0)) +(define-system prelude/number (prelude/axiom/if) + (define-core-function number? (x) number?) + (define-axiom number-predicate (x) + (is-a (number? x) (number? x))) + + (define-core-function real? (x) real?) + (define-axiom real-predicate (x) + (implies (real? x) (equal? (real? x) #t))) + (define-axiom real-is-a-numbers (x) + (implies (real? x) (equal? (number? x) #t))) + + (define-core-function integer? (x) integer?) + (define-axiom integer-predicate (x) + (implies (integer? x) (equal? (integer? x) #t))) + (define-axiom integer-is-a-real (x) + (implies (integer? x) (equal? (number? x) #t))) + + (define-core-function/guard exact? (x) (number? x) exact?) + (define-axiom exact-predicate (x) + (implies (exact? x) (equal? (exact? x) #t))) + + (define-function/guard inexact? (x) + (number? x) + (not (exact? x))) + (define-theorem inexact-predicate (x) + (implies (inexact? x) (equal? (inexact? x) #t))) + + (define-core-function exact-integer? (x) exact-integer?) + (define-axiom exact-integer-predicate (x) + (implies (exact-integer? x) (equal? (exact-integer? x) #t))) + (define-axiom exact-integer-is-a-integer (x) + (implies (exact-integer? x) (equal? (integer? x) #t))) + (define-axiom exact-integer-is-a-exact (x) + (implies (exact-integer? x) (equal? (exact? x) #t))) + + (define-core-function/guard < (x y) (and (real? x) (real? y)) <) + (define-axiom less-than-predicate (x y) + (implies (< x y) (equal? (< x y) #t))) + + (define-function/guard positive? (x) + (real? x) + (< 0 x)) + (define-theorem positive-predicate (x) + (implies (positive? x) (equal? (positive? x) #t))) + (define-function/guard negative? (x) + (real? x) + (< x 0)) + (define-theorem negative-predicate (x) + (implies (negative? x) (equal? (negative? x) #t))) + + (define-function exact-positive-integer? (x) + (and (exact-integer? x) + (positive? x))) + (define-theorem exact-positive-integer-predicate (x) + (implies (exact-positive-integer? x) + (equal? (exact-positive-integer? x) #t))) + + (define-function exact-zero? (x) (equal? x 0)) + (define-theorem exact-zero-predicate (x) + (implies (exact-zero? x) (equal? (exact-zero? x) #t))) + (define-function natural? (x) - (if (zero? x) + (if (exact-zero? x) #t - (positive-integer? x))) - (define-core-function + (x y) - (lambda (x y) - (if (number? x) - (if (number? y) - (+ x y) - x) - (if (number? y) - y - 0)))) - (define-axiom succ/pred (x) - (implies (integer? x) - (equal? (succ (pred x)) x))) - - (define-trivial-total-function < (x y) - (if (positive-integer? x) - (if (positive-integer? y) - (< (pred x) (pred y)) - #f) - (if (positive-integer? y) - #t - (if (negative-integer? x) - (if (negative-integer? y) - (< (succ x) (succ y)) - #t) - #f)))) - (set-measure-predicate natural?) - (set-measure-less-than <) - (define-axiom integer?/true (x) - (implies (integer? x) - (equal? (integer? x) #t))) - (define-axiom integer/pred (x) - (implies (integer? x) - (equal? (integer? (pred x)) #t))) - (define-axiom integer/succ (x) - (implies (integer? x) - (equal? (integer? (pred x)) #t))) - (define-axiom positive-integer?-is-predicate (x) - (implies (positive-integer? x) - (equal? (positive-integer? x) #t))) - (define-axiom negative-integer?-is-predicate (x) - (implies (negative-integer? x) - (equal? (negative-integer? x) #t))) - (define-axiom natural/pred (x) - (implies (positive-integer? x) - (equal? (natural? (pred x)) #t))) - (define-axiom positive-integer/pred (x) - (implies (natural? x) - (equal? (positive-integer? (pred x)) #t))) - (define-axiom positive-integer-is-integer (x) - (implies (positive-integer? x) - (equal? (integer? x) #t))) - (define-axiom negative-integer-is-integer (x) - (implies (negative-integer? x) - (equal? (integer? x) #t))) - (define-axiom axiom-zero (x) - (if (integer? x) - (if (positive-integer? x) - (equal? (zero? x) #f) - (if (negative-integer? x) - (equal? (zero? x) #f) - (equal? (zero? x) #t))) - (equal? (zero? x) #f))) - (define-axiom axiom-positive-integer (x) - (if (integer? x) - (if (negative-integer? x) - (equal? (positive-integer? x) #f) - (if (zero? x) - (equal? (positive-integer? x) #f) - (equal? (positive-integer? x) #t))) - (equal? (positive-integer? x) #f))) - (define-axiom axiom-negative-integer (x) - (if (integer? x) - (if (positive-integer? x) - (equal? (negative-integer? x) #f) - (if (zero? x) - (equal? (negative-integer? x) #f) - (equal? (negative-integer? x) #t))) - (equal? (negative-integer? x) #f))) - (define-axiom integer/negate (x) - (implies (integer? x) - (equal? (integer? (negate x)) #t))) - (define-axiom positive-integer/negate (x) - (if (negative-integer? x) - (equal? (positive-integer? (negate x)) #t) - (implies (integer? x) - (equal? (positive-integer? (negate x)) #f)))) - (define-axiom negative-integer/negate (x) - (if (positive-integer? x) - (equal? (negative-integer? (negate x)) #t) - (implies (integer? x) - (equal? (negative-integer? (negate x)) #f)))) - (define-axiom zero/negate (x) - (implies (zero? x) - (equal? (zero? (negate x)) #t))) - (define-function abs (x) - (if (integer? x) - (if (negative-integer? x) - (negate x) - x) - 0)) - (define-theorem natural-is-integer (x) - (implies (natural? x) (equal? (integer? x) #t))) - (define-theorem natural/abs (x) - (equal? (natural? (abs x)) #t)) - (define-theorem zero-is-0 (x) - (implies (zero? x) - (equal? x 0))) - (define-theorem not-natural-implies-not-positive-integer (x) - (implies (not (natural? x)) - (equal? (positive-integer? x) #f))) - (define-theorem natural-and-not-zero-implies-positive-integer (x) - (implies (natural? x) - (not (zero? x)) - (equal? (positive-integer? x) #t))) - (define-theorem %%abs/pred--zero/pred (x) - (implies (integer? x) - (not (positive-integer? x)) - (natural? x) - (equal? (zero? x) #t))) - (define-theorem %%abs/pred--x-is-1 (x) - (implies (positive-integer? x) - (not (positive-integer? (pred x))) - (equal? x 1))) - (define-theorem %%abs/pred-1 (x) - (implies (positive-integer? x) - (positive-integer? (pred x)) - (equal? (< (pred x) x) #t))) - (define-theorem abs/pred (x) - (if (positive-integer? x) - (equal? (< (abs (pred x)) (abs x)) #t) - #t)) - (define-theorem abs/succ (x) - (if (negative-integer? x) - (equal? (< (abs (succ x)) (abs x)) #t) - #t)) - (define-function natural-induction (x) - (if (natural? x) - (if (zero? x) - 0 - (succ (natural-induction (pred x)))) - 0)) - (define-function integer-induction (x) - (if (positive-integer? x) - (succ (integer-induction (pred x))) - (if (negative-integer? x) - (pred (integer-induction (succ x))) - 0))) - (define-function + (x y) - (if (positive-integer? x) - (succ (+ (pred x) y)) - (if (negative-integer? x) - (pred (+ (succ x) y)) - y)))) - -(define-system prelude/pair (prelude/integer) - (define-core-function pair? (x) pair?) - (define-core-function cons (x y) cons) - (define-core-function car (x) - (lambda (x) (if (pair? x) (car x) '()))) - (define-core-function cdr (x) - (lambda (x) (if (pair? x) (cdr x) '())))) - -(define-system prelude/tree (prelude/pair) - (define-trivial-total-function size (x) - (if (pair? x) - (+ 1 - (+ (size (car x)) - (size (cdr x)))) - 0)) - (define-axiom natural/size (x) - (equal? (natural? (size x)) #t)) - (define-axiom size/car (x) - (equal? (< (size (car x)) (size x)) #t)) - (define-axiom size/cdr (x) - (equal? (< (size (cdr x)) (size x)) #t)) - (define-function tree-induction (x) - (if (not (pair? x)) - x - (cons (tree-induction (car x)) - (tree-induction (cdr x)))))) - -(define-system prelude/proofs (prelude/tree) - (define-proof natural/abs - (((1) natural?) - ((1 1 1) abs) - ((1 1) if-same (set x (integer? x))) - ((1 1 3 1) if-nest) - ((1 1 3) integer?) - ((1 1 2 1) if-nest) - ((1 1 2) if-same (set x (negative-integer? x))) - ((1 1 2 2 1) if-nest) - ((1 1 2 2) integer/negate) - ((1 1 2 3 1) if-nest) - ((1) if-same (set x (integer? x))) - ((1 3 1) if-nest) - ((1 3) if-true) - ((1 3 1 1) abs) - ((1 3 1 1) if-nest) - ((1 3 1) negative-integer?) - ((1 3) not) - ((1 2 1) if-nest) - ((1 2 1 3) integer?-is-predicate) - ((1 2 1) if-same) - ((1 2) if-true) - ((1 2 1 1) abs) - ((1 2 1 1) if-nest) - ((1 2) if-same (set x (negative-integer? x))) - ((1 2 2 1 1) if-nest) - ((1 2 3 1 1) if-nest) - ((1 2 3 1) equal-if-false) - ((1 2 3) not) - ((1 2 2) if-same (set x (positive-integer? x))) - ((1 2 2 2 1) negative-integer/negate) - ((1 2 2 2) not) - ((1 2 2 3 1) negative-integer/negate) - ((1 2 2 3) not) - ((1 2 2 1) axiom-positive-integer) - ((1 2 2) if-false) - ((1 2) if-same) - ((1) if-same) - (() equal?))) - - (define-proof abs/pred - (((2 1 1) abs) - ((2 1) if-same (set x (positive-integer? (pred x)))) - ((2 1 2 1 2 1) axiom-negative-integer) - ((2 1 2 1 2) if-false) - ((2 1 2 1 1) positive-integer-is-integer) - ((2 1 2 1) if-true) - ((2 1 2 2) abs) - ((2 1 2 2 1) positive-integer-is-integer) - ((2 1 2 2) if-true) - ((2 1 2 2) if-same (set x (integer? x))) - ((2 1 2 2 2 1) axiom-negative-integer) - ((2 1 2 2 2) if-false) - ((2 1 2 2 3 1) axiom-negative-integer) - ((2 1 2 2 3) if-false) - ((2 1 2 2) if-same) - ((2 1 2) %%abs/pred-1) - ((2 1 3) if-same (set x (integer? (pred x)))) - ((2 1 3 2 1) if-nest) - ((2 1 3 3 1) if-nest) - ((2 1 3 2) if-same (set x (negative-integer? (pred x)))) - ((2 1 3 2 2 1) if-nest) - ((2 1 3 2 3 1) if-nest) - ((2 1 3 1 1 1) %%abs/pred--x-is-1) - ((2 1 3 2 1 1 1) %%abs/pred--x-is-1) - ((2 1 3 2 2 1 1 1) %%abs/pred--x-is-1) - ((2 1 3 2 2 2 1) %%abs/pred--x-is-1) - ((2 1 3 2 3 1 1) %%abs/pred--x-is-1) - ((2 1 3 2 3 2 1) %%abs/pred--x-is-1) - ((2 1 3 3 2 1) %%abs/pred--x-is-1) - ((2 1 3) (eval)) - ((2 1) if-same) - ((2) equal-same) - (() if-same))) - - (define-proof %%abs/pred-1 - (natural-induction x) - (((2 2 1 1) zero-is-0) - ((2 2 1) positive-integer?) - ((2 2) if-false) - ((2 3) if-same (set x (positive-integer? (pred x)))) - ((2 3 2 1) if-nest) - ((2 3 3 1) if-nest) - ((2 3 3) if-true) - ((2 3 2 2 2) if-nest) - ((2 3 2 2 1) natural-and-not-zero-implies-positive-integer) - ((2 3 2 2) if-true) - ((2 3 2) if-same (set x (positive-integer? (pred (pred x))))) - ((2 3 2 2 1) if-nest) - ((2 3 2 3 1) if-nest) - ((2 3 2 3) if-true) - ((2 3 2 2 2 1) <) - ((2 3 2 2 2 1) if-nest) - ((2 3 2 2 2 1 1) natural-and-not-zero-implies-positive-integer) - ((2 3 2 2 2 1) if-true) - ((2 3 2 2 2 1) equal-if) - ((2 3 2 2 2) equal?) - ((2 3 2 2) if-same) - ((2 3 2 3 1) <) - ((2 3 2 3 1) if-nest) - ((2 3 2 3 1 1) natural-and-not-zero-implies-positive-integer) - ((2 3 2 3 1) if-true) - ((2 3 2 3 1 1 1) %%abs/pred--x-is-1) - ((2 3 2 3 1 2) %%abs/pred--x-is-1) - ((2 3 2 3) (eval)) - ((2 3 2) if-same) - ((2 3 3 2) if-nest) - ((2 3 3) if-same) - ((2 3) if-same) - ((2) if-same) - ((3 1) not-natural-implies-not-positive-integer) - ((3) if-false) - (() if-same))) - - (define-proof %%abs/pred--x-is-1 - (((2 2) if-same (set x (zero? (pred x)))) - ((2 2 2) if-same (set x (integer? x))) - ((2 2 2 2 1) succ/pred) - ((2 2 2 2 1 1) zero-is-0) - ((2 2 2 2) (eval)) - ((2 2 2 1) positive-integer-is-integer) - ((2 2 2) if-true) - ((2 2) if-same (set x (natural? (pred x)))) - ((2 2 2) if-same (set x (integer? (pred x)))) - ((2 2 2 2 1) %%abs/pred--zero/pred) - ((2 2 2 2) if-true) - ((2 2 2 1) natural-is-integer) - ((2 2 2) if-true) - ((2 2 1) natural/pred) - ((2 2) if-true) - ((2) if-same) - (() if-same))) - - (define-proof %%abs/pred--zero/pred - (((2 2 1) natural?) - ((2 2 1) if-nest) - ((2 2 2) if-same (set x (zero? x))) - ((2 2 2 2 1 1) zero-is-0) - ((2 2 2 2) (eval)) - ((2 2 2 1) axiom-zero) - ((2 2 2) if-true) - ((2 2) if-same) - ((2) if-same) - (() if-same))) + (exact-positive-integer? x))) + (define-theorem (predicate natural?) (x) + (implies (natural? x) (equal? (natural? x) #t)))) - (define-proof natural-is-integer - (((1) natural?) - (() if-same (set x (integer? x))) - ((2 2 1) integer?-is-predicate) - ((2 2) equal-same) - ((2) if-same) - ((3 1) if-nest) - ((3) if-false) - (() if-same))) +(define-system prelude/measure/natural (prelude/number) + (set-measure-predicate natural?) + (set-measure-predicate <)) - (define-proof zero-is-0 - (((1) zero?) - ((2 1) equal-if) - ((2) equal?) +(define-system prelude (prelude/measure/natural) + (define-proof inexact? + (((2) if-nest) (() if-same))) - - (define-proof not-natural-implies-not-positive-integer - (((1 1) natural?) - (() if-same (set x (integer? x))) - ((2 1 1) if-nest) - ((2) if-not) - ((2) if-not) - ((2 2) if-same (set x (positive-integer? x))) - ((2 2 3 1) equal-if-false) - ((2 2 3) equal?) - ((2 2 1) axiom-positive-integer) - ((2 2) if-false) - ((2) if-same) - ((3 1 1) if-nest) - ((3 1) not) - ((3) if-true) - ((3 1) axiom-positive-integer) - ((3) equal?) + (define-proof inexact-predicate + (((1) inexact?) + (() if-not) + ((3 1) inexact?) + ((3 1 1) equal-if-false) + ((3) (eval)) (() if-same))) - - (define-proof natural-and-not-zero-implies-positive-integer - (((1) natural?) - (() if-same (set x (integer? x))) - ((2 1) if-nest) - ((2 2 2 1) axiom-positive-integer) - ((2 2 2) equal?) - ((2 2) if-same) - ((2) if-same) - ((3 1) if-nest) - ((3) if-false) + (define-proof positive? + (((2 1 1) (eval)) + ((2 1) if-true) + ((2) if-nest) (() if-same))) - - (define-proof natural-induction - (abs x) - (((1) natural/abs) - (() if-true) - ((2 3) if-same (set x (positive-integer? x))) - ((2 3 2) abs/pred) - ((2 3 1) natural-and-not-zero-implies-positive-integer) - ((2 3) if-true) - ((2) if-same) + (define-proof positive-predicate + (((1) positive?) + ((2 1) positive?) + ((2 1) less-than-predicate) + ((2) (eval)) (() if-same))) - - (define-proof integer-induction - (abs x) - (((1) natural/abs) - (() if-true) - ((2) abs/pred) - ((3 2) abs/succ) - ((3) if-same) + (define-proof negative? + (((2 1) if-nest) + ((2 1) (eval)) + ((2) if-true) (() if-same))) - - (define-proof + - (abs x) - (((1) natural/abs) - (() if-true) - ((2) abs/pred) - ((3 2) abs/succ) - ((3) if-same) - (() if-same))) - - (define-proof tree-induction - (size x) - (((2 3 1) size/car) - ((2 3 2) size/cdr) - ((2 3) if-true) - ((2) if-same) - ((1) natural/size) - (() if-true)))) - - -(define-system prelude (prelude/proofs)) + (define-proof negative-predicate + (((1) negative?) + ((2 1) negative?) + ((2 1) less-than-predicate) + ((2) (eval)) + (() if-same)))) |