diff options
Diffstat (limited to 'vikalpa/prelude.scm')
-rw-r--r-- | vikalpa/prelude.scm | 208 |
1 files changed, 148 insertions, 60 deletions
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 8816131..c55ea48 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -17,23 +17,9 @@ ;;; along with Vikalpa. If not, see <http://www.gnu.org/licenses/>. (define-module (vikalpa prelude) - #:export (atom? size implies natural? prelude) + #:export (implies prelude) #:use-module (vikalpa)) -(define (atom? x) - (not (pair? x))) - -(define (natural? x) - (and (integer? x) - (not (negative? x)))) - -(define (size x) - (if (pair? x) - (+ 1 - (size (car x)) - (size (cdr x))) - 0)) - (define-syntax implies (syntax-rules () ((_ x y) (if x y #t)) @@ -41,8 +27,16 @@ (if x (implies y z rest ...) #t)))) (define-system prelude () - (define-function atom? (x) - (not (pair? x))) + (define-primitive-function pair? (x y)) + (define-primitive-function cons (x y)) + (define-primitive-function car (x)) + (define-primitive-function cdr (x)) + (define-primitive-function sub1 (x)) + (define-primitive-function add1 (x)) + (define-primitive-function < (x y)) + (define-primitive-function natural? (x)) + (define-totality-claim natural? natural? <) + (define-syntax-rules list () ((list) '()) ((list x . y) (cons x (list . y)))) @@ -62,23 +56,23 @@ ((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 atom/cons (x y) - (equal? (atom? (cons x y)) '#f)) + (define-axiom pair/cons (x y) + (equal? (pair? (cons x y)) '#t)) (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 cons/car+cdr (x) - (if (atom? x) - '#t - (equal? (cons (car x) (cdr x)) x))) + (if (pair? x) + (equal? (cons (car x) (cdr x)) x) + '#t)) (define-axiom if-nest (x y z) (if x (equal? (if x y z) y) @@ -89,65 +83,153 @@ (equal? (if '#f x y) y)) (define-axiom if-same (x y) (equal? (if x y y) y)) - (define-axiom natural?/size (x) - (equal? (natural? (size x)) - '#t)) - (define-axiom </size/car (x) - (if (atom? x) - '#t - (equal? (< (size (car x)) (size x)) - '#t))) - (define-axiom </size/cdr (x) - (if (atom? x) - '#t - (equal? (< (size (cdr x)) (size x)) - '#t))) (define-axiom if-not (x y z) (equal? (if (not x) y z) (if x z y))) + + (define-axiom axiom-less-than (x y) + (implies (natural? x) + (natural? y) + (equal? (< x y) + (if (equal? '0 x) + (if (equal? '0 y) + #f + #t) + (if (equal? '0 y) + #f + (< (sub1 x) (sub1 y))))))) + (define-function natural-induction (n) + (if (natural? n) + (if (equal? '0 n) + '0 + (add1 (natural-induction (sub1 n)))) + 'undefined)) + + (define-proof natural-induction + (natural? n) + ()) + + (define-axiom false-if (x) + (if x #t (equal? #f x))) + (define-axiom sub1/add1 (x) (implies (natural? x) (equal? (sub1 (add1 x)) x))) - (define-axiom natural?/0 (x) + + (define-axiom natural/zero () (equal? (natural? '0) '#t)) - (define-axiom natural?/add1 (x) - (implies (natural? x) - (equal? (natural? (add1 x)) '#t))) - (define-axiom sub1/add1 (x) + + (define-axiom not/true () + (equal? (not #t) #f)) + + (define-axiom not/false () + (equal? (not #f) #t)) + + (define-theorem equal/zero-less-than (x) (implies (natural? x) - (equal? (sub1 (add1 x)) x))) - (define-axiom </sub1 (x) + (equal? (not (< '0 x)) + (equal? x '0)))) + + (define-proof equal/zero-less-than + (natural-induction x) + (((2 2) if-nest) + ((3) if-nest) + ((2 2 1) if-same (set x (natural? '0))) + ((2 2 1 2 1) axiom-less-than) + ((2 2 1 1) natural/zero) + ((2 2 1) if-true) + ((2 2 1 1 1) equal-same) + ((2 2 1 1) if-true) + ((2 2 1 1 1 2) equal-if) + ((2 2 1 1 1) equal-same) + ((2 2 1 1) if-true) + ((2 2 1) not/false) + ((2 2 2 1) equal-if) + ((2 2 2) equal-same) + ((2 2) equal-same) + ((2 3 2 2) if-same (set x (natural? '0))) + ((2 3 2 2 2 1 1) axiom-less-than) + ((2 3 2 2 2 1 1 1) equal-same) + ((2 3 2 2 2 1 1) if-true) + ((2 3 2 2 2 1 1) if-nest) + ((2 3 2 2 2 1) not/true) + ((2 3 2 2 2 2) equal-swap) + ((2 3 2 2 2 2) false-if) + ((2 3 2 2 2) equal-same) + ((2 3 2 2 1) natural/zero) + ((2 3 2 2) if-true) + ((2 3 2) if-same) + ((2 3) if-same) + ((2) if-same) + (() if-same))) + + (define-axiom natural/sub1 (x) (implies (natural? x) - (equal? (< (sub1 x) x) '#t))) - (define-theorem common-add1 (x y) + (if (equal? '0 x) + '#t + (equal? (natural? (sub1 x)) #t)))) + +;; (define-proof natural-induction +;; (total/natural? n) +;; (((2) if-nest) +;; ((2 3) </sub1) +;; ((2) if-same) +;; (() if-same))) + +(define-theorem natural/add1 (x) (implies (natural? x) - (natural? y) - (equal? (equal? (add1 x) (add1 y)) - (equal? x y)))) - (define-axiom false-if (x) - (if x '#t (equal? x '#f))) - (define-axiom equal?/01 (x) - (equal? (equal? '0 '1) #f)) - (define-axiom natural?/sub1 (x) + (equal? (natural? (add1 x)) #t))) + + #; + (define-axiom natural/sub1 (x) (if (natural? x) - (if (equal? '0 x) - '#t - (equal? (natural? (sub1 x)) '#t)) + (if (< '0 x) + (equal? (natural? (sub1 x)) '#t) + '#t) '#t)) + + #; + (define-theorem less-than/sub1 (x) + (implies (natural? x) + (< '0 x) + (equal? (< (sub1 x) x) '#t))) + + #; (define-axiom add1/sub1 (x) (if (natural? x) (if (equal? '0 x) '#t (equal? (add1 (sub1 x)) x)) '#t)) - + + #; (define-primitive-function + (x y) (if (natural? x) (if (equal? '0 x) y (add1 (+ (sub1 x) y))) 'undefined)) + + #; + (define-axiom natural/size (x) + (equal? (natural? (size x)) + '#t)) + #; + (define-axiom size/car (x) + (if (pair? x) + (equal? (< (size (car x)) (size x)) + '#t) + '#t)) + + #; + (define-axiom size/cdr (x) + (if (pair? x) + (equal? (< (size (cdr x)) (size x)) + '#t) + '#t)) + + #; (define-proof + (total/natural? x) (((2) if-nest) @@ -155,9 +237,11 @@ ((2) if-same) (() if-same))) + #; (define-theorem thm-1+1=2 () (equal? (+ 1 1) 2)) - + + #; (define-function natural-induction (n) (if (natural? n) (if (equal? '0 n) @@ -165,6 +249,7 @@ (add1 (natural-induction (sub1 n)))) 'undefined)) + #; (define-proof natural-induction (total/natural? n) (((2) if-nest) @@ -172,11 +257,13 @@ ((2) if-same) (() if-same))) + #; (define-theorem equal?/add1 (n) (if (natural? n) (equal? (equal? n (add1 n)) #f) #t)) - + + #; (define-proof equal?/add1 (induction (natural-induction n)) (((2 2 2 1 1) equal-if) @@ -205,7 +292,8 @@ ((2) if-same) ((3) if-nest) (() if-same))) - + + #; (define-proof thm-1+1=2 () ((() if-same (set x (natural? '0))) |