diff options
| -rw-r--r-- | vikalpa.scm | 394 | ||||
| -rw-r--r-- | vikalpa/prelude.scm | 208 |
2 files changed, 313 insertions, 289 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index 74dbe6c..cc88c06 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -33,6 +33,7 @@ define-primitive-function define-function define-proof + define-totality-claim define-syntax-rules total/natural? induction @@ -214,77 +215,6 @@ (environment (cdr x)))) (else #f))) -(define* (rebuild expr preconds - #:key - (quoted-proc (lambda (expr preconds) expr)) - (variable-proc (lambda (expr preconds) expr)) - (if-proc (lambda (expr preconds next) (next))) - (app-form-proc (lambda (expr preconds next) (next)))) - (let rec ((expr expr) - (preconds preconds)) - (cond - ((expr-quoted? expr) - (quoted-proc expr preconds)) - ((variable? expr) - (variable-proc expr preconds)) - ((if-form? expr) - (letrec ((next - (lambda* (#:optional (expr expr)) - (let* ((expr/test (rec (if-form-test expr) preconds)) - (expr/then (rec (if-form-then expr) (cons (if-form-test expr) preconds))) - (expr/else (rec (if-form-else expr) (cons (expr-not (if-form-test expr)) preconds)))) - (if-form expr/test expr/then expr/else))))) - (if-proc expr preconds next))) - ((app-form? expr) - (letrec ((next - (lambda* (#:optional (expr expr)) - (let f ((expr-args (app-form-args expr))) - (cond ((null? expr-args) '()) - (else - (cons (rec (car expr-args) preconds) - (f (cdr expr-args))))))))) - (app-form-proc expr preconds next))) - (else - (error "(vikalpa) rebuild: error"))))) - -(define* (expr-fold expr acc preconds - #:key - (quoted-proc (lambda (expr acc preconds) acc)) - (variable-proc (lambda (expr acc preconds) acc)) - (if-proc (lambda (expr acc preconds next) (next))) - (app-form-proc (lambda (expr acc preconds next) (next)))) - (let rec ((expr expr) - (acc acc) - (preconds preconds)) - (cond - ((expr-quoted? expr) - (quoted-proc expr acc preconds)) - ((variable? expr) - (variable-proc expr acc preconds)) - ((if-form? expr) - (letrec ((next - (lambda* (#:optional (expr expr) (acc acc) (preconds preconds)) - (let* ((acc/test - (rec (if-form-test expr) acc preconds)) - (acc/then - (rec (if-form-then expr) acc/test (cons (if-form-test expr) preconds)))) - (rec (if-form-else expr) acc/then (cons (expr-not (if-form-test expr)) preconds)))))) - (if-proc expr acc preconds next))) - ((app-form? expr) - (letrec ((next - (lambda* (#:optional (expr expr) (acc acc) (preconds preconds)) - (let fold ((expr-args (app-form-args expr)) - (acc acc)) - (cond ((null? expr-args) acc) - (else - (fold (cdr expr-args) - (rec (car expr-args) - acc - preconds)))))))) - (app-form-proc expr acc preconds next))) - (else - (error "(vikalpa) expr-fold: error"))))) - (define (substitute env expr) (cond ((expr-quoted? expr) expr) ((pair? expr) @@ -390,13 +320,14 @@ (define (system? x) (and (list? x) - (= 3 (length x)) + (= 4 (length x)) (eq? 'system (list-ref x 0)) (system-definitions? (system-definitions x)) - (system-proofs? (system-proofs x)))) + (system-proofs? (system-proofs x)) + ((const #t) (system-totality-claims x)))) -(define (make-system defs prfs) - (list 'system defs prfs)) +(define (make-system defs prfs totality-claims) + (list 'system defs prfs totality-claims)) (define (system-definitions sys) (list-ref sys 1)) @@ -404,6 +335,21 @@ (define (system-proofs sys) (list-ref sys 2)) +(define (system-totality-claims sys) + (list-ref sys 3)) + +(define (totality-claim id nat? less-than) + (list id nat? less-than)) + +(define (totality-claim-id x) + (list-ref x 0)) + +(define (totality-claim-natural x) + (list-ref x 1)) + +(define (totality-claim-less-than x) + (list-ref x 2)) + (define (lookup x sys) (assoc x (system-definitions sys))) @@ -462,7 +408,7 @@ (define/guard (function (name variable?) (vars vars?) (expr expression?) - (code any?) + (code (const #t)) (primitive boolean?)) (list name 'function vars expr code primitive)) @@ -599,7 +545,7 @@ (eq? (macro-name m) (car expr))) (let loop ((rs (macro-mrules m))) (cond ((null? rs) - (error "macro fail" m expr)) + (error "(vikalpa) macro fail" m expr)) ((apply-mrule (car rs) (macro-literals m) expr) => identity) (else (loop (cdr rs)))))) (else #f))) @@ -827,9 +773,10 @@ (values extracted-expr (case i ((1) '()) - ((2) (cons precond extracted-preconds)) - ((3) (cons (expr-not precond) extracted-preconds)) - (else (fail "(if) invaild path" path))) + ((2) (cons (prop-not (prop-not precond)) + extracted-preconds)) + ((3) (cons (prop-not precond) extracted-preconds)) + (else (fail 'if-invaild-path path))) (lambda (x) (append (list-head expr i) (list (builder x)) @@ -844,7 +791,7 @@ (list (builder x)) (list-tail expr (+ i 1))))))) (else - (fail "invalid path" path)))))) + (fail 'invalid-path path)))))) (define (function->rules x) (list (rule (function-vars x) @@ -865,27 +812,27 @@ (cons (function-name f) args) '())) -(define (parse-options/theorem ops) +(define (parse-options/theorem ops fail) (if (null? ops) (values '()) (receive (env) - (parse-options/theorem (cdr ops)) + (parse-options/theorem (cdr ops) fail) (case (caar ops) ((set) (let ((op (car ops))) (cons (cons (list-ref op 1) (list-ref op 2)) env))) (else - (error "invalid option:" (car ops))))))) + (fail 'invalid-option (car ops))))))) (define (rewrite/theorem cmd b thm preconds expr fail) (receive (env) - (parse-options/theorem (command-options cmd)) + (parse-options/theorem (command-options cmd) fail) (cond ((any (cut apply-rule preconds <> expr env) (theorem*-rules thm)) => identity) (else - (fail (format #f "no match theorem ~a: ~s" cmd expr)))))) + (fail 'apply-theorem cmd expr))))) ;; (rewrite system? rewriter? expression? procedure?) -> expr (define (rewrite1 sys expr fail r) @@ -901,7 +848,8 @@ (('equal? `(quote ,x) `(quote ,y)) (expr-quote (equal? x y))) (else - (fail "error: equal? ~a" extracted-expr)))) + (fail 'equal? 'extracted-expr)))) + ((eq? 'error cmd/name) (fail extracted-expr)) ((and (symbol? cmd/name) (lookup cmd/name sys)) => (lambda (x) @@ -913,10 +861,10 @@ ((any (cut apply-rule '() <> extracted-expr '()) (function->rules x)) => identity) (else - (fail (format #f "no match-function (~a)" cmd))))) + (fail 'apply-function cmd extracted-expr)))) (else - (fail "rewrite error" cmd))))) - (else (fail "no cmd" cmd extracted-expr))))))) + (fail 'invalid-command cmd extracted-expr))))) + (else (fail 'command-not-found cmd extracted-expr))))))) (define/guard (rewrite (sys system?) (expr expression?) (seq sequence?)) (debug "rewrite ~y~%" expr) @@ -924,20 +872,25 @@ (seq seq)) (debug "~y~%" expr) #;(format #t "~y~%" expr) - (if (null? seq) - expr - (loop (rewrite1 sys - expr - (lambda (x . args) - (apply error - (format #f "rewrite: ~a" x) - args)) - (car seq)) - (cdr seq))))) + (reset + (if (null? seq) + expr + (loop (rewrite1 sys + expr + (lambda args + (shift k (cons 'error args))) + (car seq)) + (cdr seq)))))) (define (expr-not x) (list 'not x)) +(define (prop-not x) + (match x + (('not ('not expr)) (prop-not expr)) + (('not expr) expr) + (expr (expr-not expr)))) + (define (expr-equal? x) (and (list? x) (= 3 (length x)) @@ -954,10 +907,14 @@ (define (expression->rules vars preconds expr) (if (if-form? expr) (append (expression->rules vars - (cons (if-form-test expr) preconds) + (cons (prop-not + (prop-not + (if-form-test expr))) + preconds) (if-form-then expr)) (expression->rules vars - (cons (expr-not (if-form-test expr)) preconds) + (cons (prop-not (if-form-test expr)) + preconds) (if-form-else expr))) (if (expr-equal? expr) (list (rule vars @@ -975,18 +932,20 @@ '() (theorem*-expression def))) -(define current-system (make-parameter (make-system '() '()))) +(define current-system (make-parameter (make-system '() '() '()))) (define (add-definition x) (let ((sys (current-system))) (current-system - (cond ((lookup (theorem*-name x) sys) - => (lambda (thm) - (if (equal? x thm) - sys - (error "add-definition: error")))) + (cond ((lookup (definition-name x) sys) + => (lambda (d) + (if (equal? x d) + x + (error "(vikalpa) add-definition: duplicated" + (definition-name d))))) (else (make-system (cons x (system-definitions sys)) - (system-proofs sys))))) + (system-proofs sys) + (system-totality-claims sys))))) x)) (define (add-proof x) @@ -996,12 +955,13 @@ => (lambda (prf) (if (equal? x prf) sys - (error "add-proof: error")))) + (error "add-proof: duplicated")))) (else (make-system (system-definitions sys) - (cons x (system-proofs sys)))))) + (cons x (system-proofs sys)) + (system-totality-claims sys))))) x)) -(define reserved-symbols '(quote let if)) +(define reserved-symbols '(quote let if error)) (define (reserved? x) (member x reserved-symbols)) @@ -1059,63 +1019,52 @@ (add-definition m) m)))) -(define (size x) - (if (pair? x) - (+ 1 - (size (car x)) - (size (cdr x))) - 0)) -(define (add1 n) (1+ n)) -(define (sub1 n) (1- n)) +(define (find-totality-claim name sys) + (assoc name (system-totality-claims sys))) + +(define (add-totality-claim tc) + (let ((sys (current-system))) + (cond ((find-totality-claim (totality-claim-id tc) sys) + => (lambda (tc2) + (unless (equal? tc tc2) + (error "(vikalpa) define-totality-claim: duplicated" + tc))))) + (unless (and (symbol? (totality-claim-id tc)) + (cond ((lookup (totality-claim-natural tc) sys) + => function*?) + (else #f)) + (cond ((lookup (totality-claim-less-than tc) sys) + => function*?) + (else #f))) + (error "(vikalpa) define-totality-claim: invalid totality-claim" + tc)) + (current-system + (make-system (system-definitions sys) + (system-proofs sys) + (cons tc (system-totality-claims sys)))) + tc)) -(define (core-primitive-function) - (list (primitive-function 'not '(x)) - (primitive-function 'equal? '(x y)) - (primitive-function 'pair? '(x)) - (primitive-function 'cons '(x y)) - (primitive-function 'car '(x)) - (primitive-function 'cdr '(x)) - (primitive-function 'size '(x)) - (primitive-function 'natural? '(x)) - (primitive-function 'add1 '(x)) - (primitive-function 'sub1 '(x)) - (primitive-function '< '(x y)))) +(define-syntax-rule (define-totality-claim name nat? <) + (add-totality-claim (totality-claim 'name 'nat? '<))) -(define* (empty-system #:optional (parent (make-system '() '()))) +(define* (core-system #:optional (parent (make-system '() '() '()))) (parameterize ([current-system parent]) (define-primitive-function not (x)) (define-primitive-function equal? (x y)) - (define-primitive-function pair? (x)) - (define-primitive-function cons (x y)) - (define-primitive-function car (x)) - (define-primitive-function cdr (x)) - (define-primitive-function size (x)) - (define-primitive-function natural? (x)) - (define-primitive-function add1 (x)) - (define-primitive-function sub1 (x)) - (define-primitive-function < (x y)) - (unless (system? (current-system)) - (error "define-system: error")) (current-system))) (define-syntax define-system (syntax-rules () ((_ name (systems ...) expr ...) - (define* (name #:optional (parent (make-system '() '()))) + (define* (name #:optional (parent (make-system '() '() '()))) (parameterize ([current-system - ((compose systems ... empty-system) parent)]) + ((compose systems ... core-system) parent)]) expr ... (unless (system? (current-system)) - (error "define-system: error")) + (error "define-system: invalid system")) (current-system)))))) - -(define (atom? x) - (not (pair? x))) - -(define (any? x) #t) - (define (measure? x) (and (pair? x) (variable? (car x)) @@ -1131,9 +1080,6 @@ (define (function-app-form f) (cons (function-name f) (function-vars f))) -(define (expand-all b expr) - (expand* (filter macro? b) expr)) - (define (single? x) (and (pair? x) (null? (cdr x)))) @@ -1164,7 +1110,7 @@ (else (if/if x y ''#t)))) -(define (make-total-claim/natural m-expr f) +(define (make-totality-claim tc m-expr f) (let* ((name (function-name f))) (define (convert app-form) (cond @@ -1176,9 +1122,11 @@ app-form '()) => identity) - (else (error "make-total-claim/natural: convert error" + (else (error "make-totality-claim: convert error" + (function-name f) + m-expr app-form)))) - (if/if `(natural? ,m-expr) + (if/if `(,(totality-claim-natural tc) ,m-expr) (let loop ((expr (function-expression f))) (cond ((expr-quoted? expr) ''#t) @@ -1199,10 +1147,14 @@ (else (and/if (loop (car args)) (f (cdr args)))))))) (if (eq? name (app-form-name expr)) - (and/if `(< ,(convert expr) ,m-expr) + (and/if `(,(totality-claim-less-than tc) + ,(convert expr) + ,m-expr) rest) rest))) - (else (error "(vikalpa) make-total-claim: error")))) + (else (error "(vikalpa) make-totality-claim: error" + (function-name f) + m-expr)))) ''#t))) (define/guard (make-induction-claim (f function*?) @@ -1216,13 +1168,14 @@ (cons expr rest) rest))) ((if-form? expr) - (error "make-induction-claim: FAILED m(- -)m")) + (error "make-induction-claim(find-app-forms): not supported" + expr)) (else '()))) (let ((c (theorem*-expression t))) (define (prop app-form) (cond ((apply-rule '() - (rule (function-vars f) + (rule vars '() (cons (function-name f) vars) c) @@ -1230,7 +1183,7 @@ '()) => identity) (else - (error "make-induction-claim: fail")))) + (error "make-induction-claim: fail" app-form)))) (cond ((apply-function f vars) => (lambda (expr) @@ -1273,24 +1226,12 @@ (define seed? (const #t)) (define-syntax define-proof - (syntax-rules (total natural? induction) - ((_ name - (total/natural? m-expr) - (((n ...) cmd ...) ...)) - (add-proof (proof 'name - '(total/natural? m-expr) - '(((n ...) cmd ...) ...)))) - ((_ name - (induction (f var ...)) - (((n ...) cmd ...) ...)) - (add-proof (proof 'name - '(induction (f var ...)) - '(((n ...) cmd ...) ...)))) + (syntax-rules () ((_ name - () + (seed ...) (((n ...) cmd ...) ...)) (add-proof (proof 'name - '() + '(seed ...) '(((n ...) cmd ...) ...)))))) (define (function*? x) @@ -1337,12 +1278,18 @@ (define (prove/theorem sys t pf) (match (proof-seed pf) - (('induction (f . vars)) - (rewrite sys - (make-induction-claim (lookup f sys) - vars - t) - (proof-sequence pf))) + ((f . vars) + (cond + ((lookup f sys) + => (lambda (seed) + (rewrite sys + (make-induction-claim seed + vars + t) + (proof-sequence pf)))) + (else (error "(vikalpa) define-proof: induction function is not found." + (proof-name pf) + (cons f vars))))) (() (rewrite sys (theorem*-expression t) @@ -1352,12 +1299,20 @@ (define (prove/function sys f pf) (match (proof-seed pf) - (('total/natural? m-expr) - (rewrite sys - (make-total-claim/natural m-expr f) - (proof-sequence pf))) + ((id m-expr) + (cond + ((find-totality-claim id sys) + => (lambda (tc) + (rewrite sys + (make-totality-claim tc m-expr f) + (proof-sequence pf)))) + (else + (error "(vikalpa) define-proof: totality-claim is not found:" + (proof-name pf) + (proof-seed pf))))) (else - (error "prove/function: fail")))) + (error "define-proof: fail" + (proof-name pf) (proof-seed pf))))) (define (system->scheme sys) `(begin @@ -1375,7 +1330,8 @@ (let ((defs (system-definitions sys))) (define* (next #:optional fail) (loop (make-system (cdr defs) - (system-proofs sys)) + (system-proofs sys) + (system-totality-claims sys)) (if fail (cons fail fails) fails))) @@ -1383,12 +1339,9 @@ ((null? defs) fails) ((or (theorem? (car defs)) (function? (car defs))) - (cond + (cond ((and (function? (car defs)) (trivial-total? (car defs))) - #; - (format #t "`~a` is trivial total function.~%" - (definition-name (car defs))) (next)) (else (cond @@ -1397,61 +1350,44 @@ (let ((result (prove sys (car defs) pf))) (cond ((equal? result ''#t) - #; - (format #t "`~a` is ~a.~%" - (definition-name (car defs)) - (if (function? (car defs)) - "total function" - "true")) (next)) (else - #; - (format #t "`~a`'s proof is failed:~%~y" - (definition-name (car defs)) - result) (next (list (definition-name (car defs)) result))))))) (else - #; - (format #t "`~a`'s proof is not found.~%" - (definition-name (car defs))) (next (list (definition-name (car defs))))))))) (else (next)))))) +(define (pp x) + (pretty-print x + #:width 79 + #:max-expr-width 50)) + (define/guard (show (sys system?) (name symbol?)) - (define (pp x) - (pretty-print x - #:width 79 - #:max-expr-width 50)) (cond ((lookup name sys) => (lambda (def) (cond ((function? def) - (pp - `(define-function ,(function-name def) ,(function-vars def) - ,(function-expression def)))) + `(define-function ,(function-name def) ,(function-vars def) + ,(function-expression def))) ((theorem? def) - (pp - `(define-theorem ,(theorem*-name def) ,(theorem*-vars def) - ,(theorem*-expression def)))) + `(define-theorem ,(theorem*-name def) ,(theorem*-vars def) + ,(theorem*-expression def))) ((axiom? def) - (pp - `(define-axiom ,(theorem*-name def) ,(theorem*-vars def) - ,(theorem*-expression def)))) + `(define-axiom ,(theorem*-name def) ,(theorem*-vars def) + ,(theorem*-expression def))) ((primitive-function? def) - (pp - `(define-primitive-function - ,(primitive-function-name def) - ,(primitive-function-vars def)))) + `(define-primitive-function + ,(primitive-function-name def) + ,(primitive-function-vars def))) ((macro? def) - (pp - `(define-syntax-rules ,(macro-name def)))) + `(define-syntax-rules ,(macro-name def))) (else - (error "show: error"))))) + `(error 'fatal-error ,name))))) (else - (format #t "~a: not found~%" name)))) + `(error 'not-found ,name)))) (define/guard (load-system (sys system?)) (primitive-eval (system->scheme sys))) 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))) |