diff options
author | Masaya Tojo <masaya@tojo.tokyo> | 2021-01-05 10:25:26 +0900 |
---|---|---|
committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-01-05 10:25:26 +0900 |
commit | 42f3851f4f6b80acdc416ff0f95bee52ef369b9a (patch) | |
tree | a144682ad8cdad3c16127add89492a8ba4408280 /vikalpa/prelude.scm | |
parent | f590c9c29ff60b1e3ab9ebfb8703d390a5b3df1c (diff) |
wip69
Diffstat (limited to 'vikalpa/prelude.scm')
-rw-r--r-- | vikalpa/prelude.scm | 47 |
1 files changed, 29 insertions, 18 deletions
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index e24d32d..74cbe98 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -43,6 +43,21 @@ (- x) 0)) +(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)) @@ -97,15 +112,16 @@ (define-core-function real? (x) real?) (define-axiom (predicate real?) (x) (predicate (real? x))) - (define-axiom (is real? number?) (x) (is (real? x) (number? 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?) (x) (is (integer? x) (real? 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))) @@ -113,13 +129,12 @@ (define-core-function exact-integer? (x) exact-integer?) (define-axiom (predicate exact-integer?) (x) (predicate (exact-integer? x))) - (define-axiom (is exact-integer? integer?) (x) - (is (exact-integer? x) - (integer? x))) - (define-axiom (is exact-integer? exact?) (x) (is (exact-integer? x) - (exact? x))) - (define-theorem (is exact-integer? real?) (x) - (is (exact-integer? x) (real? 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))) @@ -137,17 +152,20 @@ (positive? x))) (define-theorem (predicate exact-positive-integer?) (x) (predicate (exact-positive-integer? x))) + (define-theorem/is exact-positive-integer? 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-function natural? (x) (if (exact-zero? x) #t (exact-positive-integer? x))) (define-theorem (predicate natural?) (x) - (predicate (natural? x)))) + (predicate (natural? x))) + (define-theorem/is natural? exact-integer?)) (define-system prelude/measure/natural (prelude/number) (set-measure-predicate natural?) @@ -192,13 +210,6 @@ (rewrite (2 1) (predicate <)) (eval (2)) (rewrite () if-same))) - (define-proof (is exact-integer? real?) - ((rewrite (2) if-same (set x (integer? x))) - (rewrite (2 2 1) (is integer? real?)) - (eval (2 2)) - (rewrite (2 1) (is exact-integer? integer?)) - (rewrite (2) if-true) - (rewrite () if-same))) (define-proof exact-positive-integer? ((rewrite (1 2) (is exact-integer? real?)) (rewrite (1) if-same) |