diff options
| -rw-r--r-- | vikalpa.scm | 609 |
1 files changed, 318 insertions, 291 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index bff63f0..e7126f8 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -17,31 +17,24 @@ ;;; along with Vikalpa. If not, see <http://www.gnu.org/licenses/>. (define-module (vikalpa) - #:export () ;; (rewrite - ;; show - ;; check - ;; system->scheme - ;; load-system - ;; system-primitives - ;; system-functions - ;; system-macros - ;; system-theorems - ;; system-axioms - ;; system-totality-claims - ;; define-system - ;; define-axiom - ;; define-theorem - ;; define-primitive-function - ;; define-function - ;; define-scheme-function - ;; define-proof - ;; define-totality-claim - ;; define-syntax-rules - ;; system-eval) + #:export (rewrite + describe + system-check + system-apropos + system-code + system-load + set-measure-predicate + set-measure-less-than + define-system + define-proof + define-core-function + define-function + define-theorem) #:use-module (ice-9 match) #:use-module (ice-9 format) #:use-module (ice-9 control) #:use-module (ice-9 exceptions) + #:use-module (ice-9 regex) #:use-module ((srfi srfi-1) #:select (every any member lset-union fold append-map find)) @@ -56,13 +49,9 @@ #:getter get-definitions #:init-keyword #:definitions #:init-value '()) - (natural-predicate #:getter get-natural-predicate + (measure-predicate #:getter get-measure-predicate #:init-value #f) - (natural-less-than #:getter get-natural-less-than - #:init-value #f) - (ordinal-predicate #:getter get-ordinal-predicate - #:init-value #f) - (ordinal-less-than #:getter get-ordinal-less-than + (measure-less-than #:getter get-measure-less-than #:init-value #f)) (define-class <definition> () @@ -85,27 +74,27 @@ (define-class <theorem> (<theorem*> <proved>)) (define-class <axiom> (<theorem*>)) -(define-class <condition> () - (expressions #:getter get-expressions #:init-keyword #:expressions)) - (define-class <function*> (<definition>) - (condition #:getter get-condition #:init-keyword #:condition)) + (conditions #:getter get-conditions #:init-keyword #:conditions)) (define-class <core-function> (<function*>) (procedure #:getter get-procedure #:init-keyword #:procedure)) (define-class <expandable-function> (<function*>) (expression #:getter get-expression #:init-keyword #:expression) - (code #:getter get-code #:init-keyword #:expressions)) + (code #:getter get-code #:init-keyword #:code)) (define-class <function> (<expandable-function> <provable>)) (define-class <total-function> (<expandable-function> <proved>)) (define-class <trivial-total-function> (<expandable-function>)) +(define-generic macro-mrules) +(define-generic macro-literals) +(define-class <macro> (<definition>) + (mrules #:getter macro-mrules #:init-keyword #:mrules) + (literals #:getter macro-literals #:init-keyword #:literals)) + (define (write-definition sym d port) (format port "#<~a: ~s>" sym (cons (get-name d) (get-variables d)))) -(define-method (display (d <definition>) port) - (write d port)) - (define-method (write (s <system>) port) (format port "#<system: function: ~a theorem: ~a macro: ~a>" (length (filter (cut is-a? <> <function*>) @@ -115,6 +104,8 @@ (length (filter (cut is-a? <> <macro>) (get-definitions s))))) +(define-method (write (d <macro>) port) + (write-definition 'macro d port)) (define-method (write (d <conjecture>) port) (write-definition 'conjecture d port)) (define-method (write (d <theorem>) port) @@ -126,7 +117,7 @@ (define-method (write (d <function>) port) (write-definition 'function d port)) (define-method (write (d <core-function>) port) - (write-definition 'function d port)) + (write-definition 'core-function d port)) (define-method (write (d <trivial-total-function>) port) (write-definition 'trivial-total-function d port)) (define-method (write (d <total-function>) port) @@ -138,53 +129,60 @@ (eq? name (get-name x))) (get-definitions s))) -(define-generic update-natural-predicate) -(define-method (update-natural-predicate (s <symbol>) (sys <system>)) +(define-generic update-measure-predicate) +(define-method (update-measure-predicate (s <symbol>) (sys <system>)) (let ((new (shallow-clone sys))) - (slot-set! new 'natural-predicate s) + (slot-set! new 'measure-predicate s) new)) -(define-generic update-natural-less-than) -(define-method (update-natural-less-than (s <symbol>) (sys <system>)) +(define-generic update-measure-less-than) +(define-method (update-measure-less-than (s <symbol>) (sys <system>)) (let ((new (shallow-clone sys))) - (slot-set! new 'natural-less-than s) - new)) - -(define-generic update-ordinal-predicate) -(define-method (update-ordinal-predicate (s <symbol>) (sys <system>)) - (let ((new (shallow-clone sys))) - (slot-set! new 'ordinal-predicate s) - new)) - -(define-generic update-ordinal-less-than) -(define-method (update-ordinal-less-than (s <symbol>) (sys <system>)) - (let ((new (shallow-clone sys))) - (slot-set! new 'ordinal-less-than-function s) + (slot-set! new 'measure-less-than s) new)) (define-generic update-definition) (define-method (update-definition (d <definition>) (sys <system>)) + (define (update d defs) + (if (null? defs) + (raise-exception + (make-exception + (make-exception-with-origin 'update-definition) + (make-exception-with-message "not found") + (make-exception-with-irritants (list d defs)))) + (if (equal? (get-name d) (get-name (car defs))) + (cons d (cdr defs)) + (cons (car defs) (update d (cdr defs)))))) (let ((new (shallow-clone sys))) (slot-set! new 'definitions - (cons d (get-definitions sys))) + (update d (get-definitions sys))) new)) - -(define-generic update-definition) -(define-method (update-definition (d <definition>) (sys <system>)) +(define-generic remove-first-definition) +(define-method (remove-first-definition (sys <system>)) (let ((new (shallow-clone sys))) (slot-set! new 'definitions - (cons d (get-definitions sys))) + (cdr (get-definitions sys))) new)) +(define-generic first-definition) +(define-method (first-definition (sys <system>)) + (car (get-definitions sys))) + +(define-generic system-empty?) +(define-method (system-empty? (sys <system>)) + (null? (get-definitions sys))) (define-generic add-definition) (define-method (add-definition (d <definition>) (s <system>)) (if (lookup (get-name d) s) (raise-exception (make-exception - (make-exception-with-message - "(vikalpa) add-definition: duplicated definition") + (make-exception-with-origin 'add-definition) + (make-exception-with-message "duplicated definition") (make-exception-with-irritants (get-name d)))) - (update-definition d s))) + (let ((new (shallow-clone s))) + (slot-set! new 'definitions + (cons d (get-definitions s))) + new))) (define-generic validate) (define-method (validate (d <definition>)) @@ -229,16 +227,15 @@ (m p?) (n t? getter-var getter) ...) (begin - (define len (+ 1 (length (list n ...)))) (define (constractor getter-var ...) - (let ((data (make-list len))) + (let ((data (make-list (+ 1 (length (list t? ...)))))) (list-set! data m 'name) (list-set! data n getter-var) ... data)) (define (p? x) (and (list? x) - (= len (length x)) + (= (+ 1 (length (list t? ...))) (length x)) (eq? 'name (list-ref x m)) (t? (list-ref x n)) ...)) (define (getter x) @@ -520,11 +517,14 @@ expr code-expr)) -(define-type mrule - mrule - (0 mrule?) - (1 (const #t) lhs mrule-lhs) - (2 (const #t) rhs mrule-rhs)) +(define-generic mrule-lhs) +(define-generic mrule-rhs) +(define-class <mrule> () + (lhs #:getter mrule-lhs #:init-keyword #:lhs) + (rhs #:getter mrule-rhs #:init-keyword #:rhs)) + +(define (mrule lhs rhs) + (make <mrule> #:lhs lhs #:rhs rhs)) (define (mrule-vars mrl) (define (all-vars x) @@ -536,12 +536,6 @@ (else '()))) (all-vars (mrule-lhs mrl))) -(define-generic macro-mrules) -(define-generic macro-literals) -(define-class <macro> (<definition>) - (mrules #:getter macro-mrules #:init-keyword #:mrules) - (literals #:getter macro-literals #:init-keyword #:literals)) - (define (macro name mrules literals) (make <macro> #:name name @@ -620,10 +614,11 @@ (expr expr)) (cond ((null? ms) expr) - (else (expand (cdr ms) - (cond - ((apply-macro (car ms) expr) => identity) - (else expr))))))) + (else + (expand (cdr ms) + (cond + ((apply-macro (car ms) expr) => identity) + (else expr))))))) (define (expand* ms expr) (let loop ((ms ms) @@ -817,11 +812,11 @@ (define (function->rules x) (list (rule (get-variables x) - (get-expressions (get-condition x)) + (get-conditions x) (defined-function-app-form x) (get-expression x)) (rule (get-variables x) - (get-expressions (get-condition x)) + (get-conditions x) (get-expression x) (defined-function-app-form x)))) @@ -859,7 +854,7 @@ (define (rewrite/induction sys fname vars expr fail) (cond ((lookup fname sys) - (cut make-induction-claim <> vars expr)) + => (cut make-induction-claim <> vars expr)) (else (fail 'induction 'not-found fname)))) (define (rewrite1 sys expr fail r) @@ -872,13 +867,6 @@ (cond ((equal? '(eval) cmd/name) (rewrite/eval extracted-expr sys)) - ((match cmd/name - (`(induction ,(f . vars)) - (rewrite/induction sys f vars extracted-expr fail)) - (`(induction . ,x) - (fail 'induction x)) - (else #f)) => identity) - ((eq? 'error cmd/name) (fail extracted-expr)) ((and (symbol? cmd/name) (lookup cmd/name sys)) => (lambda (x) @@ -888,14 +876,15 @@ ((is-a? x <expandable-function>) (cond ((any (cut apply-rule '() <> extracted-expr '()) - (function->rules x)) => identity) + (function->rules x)) + => identity) (else (fail 'apply-function cmd extracted-expr)))) (else (fail 'invalid-command cmd extracted-expr))))) (else (fail 'command-not-found cmd extracted-expr))))))) -(define/guard (rewrite (sys (cut is-a? <> <system>)) (expr (const #t)) (seq sequence?)) +(define/guard (rewrite (sys (cut is-a? <> <system>)) (expr (const #t)) (seq (const #t))) (let ((expr (convert-to-expression expr))) (let loop ((expr expr) (seq seq)) @@ -995,7 +984,7 @@ (let ((f (make <core-function> #:name 'name #:variables '(var ...) - #:condition '(precond ...) + #:conditions '(precond ...) #:procedure proc))) (current-system (add-definition f (current-system))) (validate f) @@ -1007,10 +996,22 @@ (let ((f (make <function> #:name 'name #:variables '(var ...) - #:condition '(precond ...) + #:conditions '(precond ...) + #:expression (convert-to-expression 'expr) + #:code (code 'expr)))) + (current-system (add-definition f (current-system))) + (validate f) + f)))) + +(define-syntax define-function/no-code + (syntax-rules () + ((_ name (var ...) precond ... expr) + (let ((f (make <function> + #:name 'name + #:variables '(var ...) + #:conditions '(precond ...) #:expression (convert-to-expression 'expr) - #:precond '(precond ...) - #:code 'expr))) + #:code (code 'expr)))) (current-system (add-definition f (current-system))) (validate f) f)))) @@ -1021,10 +1022,9 @@ (let ((f (make <trivial-total-function> #:name 'name #:variables '(var ...) - #:condition '(precond ...) + #:conditions '(precond ...) #:expression (convert-to-expression 'expr) - #:precond '(precond ...) - #:code 'expr))) + #:code (code 'expr)))) (current-system (add-definition f (current-system))) (validate f) f)))) @@ -1053,8 +1053,8 @@ (define (err) (raise-exception (make-exception - (make-exception-with-message - (string-append "(vikalpa) " desc ": unbound function")) + (make-exception-with-origin 'desc) + (make-exception-with-message "unbound function") (make-exception-with-irritants name)))) (cond ((lookup name (current-system)) @@ -1064,36 +1064,20 @@ (err)))) (else (err)))) -(define-syntax set-natural-predicate +(define-syntax set-measure-predicate (syntax-rules () ((_ name) (begin - (validate-function-name "set-natural-predicate" 'name) - (current-system (update-natural-predicate 'name (current-system))))))) + (validate-function-name 'set-measure-predicate 'name) + (current-system (update-measure-predicate 'name (current-system))))))) -(define-syntax set-natural-less-than +(define-syntax set-measure-less-than (syntax-rules () ((_ name) (begin - (validate-function-name "set-natural-less-than" 'name) + (validate-function-name 'set-measure-less-than 'name) (current-system - (update-natural-less-than 'name (current-system))))))) - -(define-syntax set-ordinal-predicate - (syntax-rules () - ((_ name) - (begin - (validate-function-name "set-ordinal-predicate" 'name) - (current-system - (update-ordinal-predicate 'name (current-system))))))) - -(define-syntax set-ordinal-less-than - (syntax-rules () - ((_ name) - (begin - (validate-function-name "set-ordinal-less-than" 'name) - (current-system - (update-natural-less-than 'name (current-system))))))) + (update-measure-less-than 'name (current-system))))))) (define (defined-function-app-form f) (app-form (get-name f) (get-variables f))) @@ -1128,12 +1112,7 @@ (else (if/if x y ''#t)))) -(define-class <totality-claim-method> () - (id #:getter totality-claim-id #:init-keyword #:id) - (natural #:getter totality-claim-natural #:init-keyword #:natural) - (less-than #:getter totality-claim-less-than #:init-keyword #:less-than)) - -(define (make-totality-claim tc m-expr f) +(define (make-totality-claim* sys m-expr f) (let* ((name (get-name f))) (define (convert app-form) (cond @@ -1149,7 +1128,7 @@ (get-name f) m-expr app-form)))) - (if/if `(,(totality-claim-natural tc) ,m-expr) + (if/if `(,(get-measure-predicate sys) ,m-expr) (let loop ((expr (get-expression f))) (cond ((expr-quoted? expr) ''#t) @@ -1170,7 +1149,7 @@ (else (and/if (loop (car args)) (f (cdr args)))))))) (if (eq? name (app-form-name expr)) - (and/if `(,(totality-claim-less-than tc) + (and/if `(,(get-measure-less-than sys) ,(convert expr) ,m-expr) rest) @@ -1187,7 +1166,7 @@ (let ((rest (append-map find-preconds (cdr expr)))) (append (cond ((lookup (car expr) sys) => (lambda (f) - (let ((preconds (get-condition f))) + (let ((preconds (get-conditions f))) (map (lambda (precond) (substitute (map cons (get-variables f) @@ -1237,14 +1216,14 @@ (error "make-induction-claim(find-app-forms): not supported" expr)) (else '()))) - (define (prop app-form) + (define (prop form) (cond ((apply-rule '() (rule vars '() (app-form (get-name f) vars) c) - app-form + form '()) => identity) (else @@ -1268,22 +1247,86 @@ (else (error "make-induction-claim: invalid" f vars c)))) -(define seed? (const #t)) +(define (add-proof/function sys f seed seq) + (if seed + (update-definition (make <total-function> + #:name (get-name f) + #:variables (get-variables f) + #:conditions (get-conditions f) + #:expression (get-expression f) + #:code (get-code f) + #:claim (make-totality-claim* sys seed f) + #:proof seq) + sys) + (raise-exception + (make-exception + (make-exception-with-origin 'define-proof) + (make-exception-with-message "need seed") + (make-exception-with-irritants (get-expression f)))))) + +(define (add-proof/theorem sys t seed seq) + (let ((claim + (match seed + ((fname . vars) + (cond ((lookup fname sys) + => (cut make-induction-claim <> vars (get-expression t))) + (else (get-expression t)))) + (else (get-expression t))))) + (update-definition (make <theorem> + #:name (get-name t) + #:variables (get-variables t) + #:expression (get-expression t) + #:claim claim + #:proof seq) + sys))) -;; (define-syntax define-proof -;; (syntax-rules () -;; ((_ name -;; (((n ...) cmd ...) ...)) -;; (add-proof (proof 'name -;; '() -;; '(((n ...) cmd ...) ...)))) -;; ((_ name -;; (seed ...) -;; (((n ...) cmd ...) ...)) -;; (add-proof (proof 'name -;; '(seed ...) -;; '(((n ...) cmd ...) ...)))))) +(define (add-proof sys name seed seq) + (cond + ((not (sequence? seq)) + (raise-exception + (make-exception + (make-exception-with-origin 'define-proof) + (make-exception-with-message "not sequence") + (make-exception-with-irritants seq)))) + ((lookup name sys) + => (lambda (def) + (current-system + (if (and (is-a? def <provable>) + (not (is-a? def <proved>))) + (cond + ((is-a? def <function>) + (add-proof/function sys def seed seq)) + ((is-a? def <conjecture>) + (add-proof/theorem sys def seed seq)) + (else + (raise-exception + (make-exception + (make-exception-with-origin 'define-proof) + (make-exception-with-message "error") + (make-exception-with-irritants def))))) + (raise-exception + (make-exception + (make-exception-with-origin 'define-proof) + (make-exception-with-message "not provable definition") + (make-exception-with-irritants def))))))) + (else + (raise-exception + (make-exception + (make-exception-with-origin 'define-proof) + (make-exception-with-message "definition is not found") + (make-exception-with-irritants name)))))) +(define-syntax define-proof + (syntax-rules () + ((_ name + seed + seq) + (add-proof (current-system) + 'name + 'seed + 'seq)) + ((_ name seq) + (define-proof name #f seq)))) (define (validate-expression sys name vars expr) (let* ((expr-fnames (expression-functions expr)) @@ -1292,8 +1335,8 @@ (define (err msg x) (raise-exception (make-exception - (make-exception-with-message - (format #f "(vikalpa) ~a: ~a" name msg)) + (make-exception-with-origin name) + (make-exception-with-message msg) (make-exception-with-irritants x)))) (for-each (lambda (x) (when (member x expr-fnames) @@ -1348,149 +1391,89 @@ (define (trivial-total? f sys) (and (not (recur? f)))) -;; (define (prove sys def pf) -;; (cond -;; ((theorem? def) -;; (prove/theorem sys def pf)) -;; ((function? def) -;; (prove/function sys def pf)) -;; (else (error "prove" def pf)))) - -;; (define (prove/theorem sys t pf) -;; (let ((sys-without-self -;; (make-system (filter (lambda (d) (not (equal? t d))) -;; (get-definitions sys)) -;; (system-proofs sys) -;; (system-totality-claim-list sys)))) -;; (rewrite sys-without-self -;; (theorem-expression t) -;; (proof-sequence pf)))) +(define/guard (system-apropos (sys system?) (str string?)) + (filter (lambda (name) + (string-match (string-append ".*" + (regexp-quote str) + ".*") + (symbol->string name))) + (map get-name (get-definitions sys)))) -;; (define (prove/function sys f pf) -;; (match (proof-seed pf) -;; (() -;; (error "prove/function error")) -;; ((id m-expr) -;; (cond -;; ((find-totality-claim id sys) -;; => (lambda (tc) -;; (let ((claim (make-totality-claim tc m-expr f))) -;; (validate-expression sys -;; `(claim-of ,(function-name f)) -;; (function-vars f) -;; claim) -;; (rewrite sys -;; claim -;; (proof-sequence pf))))) -;; (else -;; (error "(vikalpa) define-proof: totality-claim is not found:" -;; (proof-name pf) -;; (proof-seed pf))))) -;; (else -;; (error "define-proof: fail" -;; (proof-name pf) (proof-seed pf))))) +(define (system-code sys) + `(begin + ,@(map (lambda (f) + `(define (,(get-name f) ,@(get-variables f)) + ,(code-expr (get-code f)))) + (reverse (filter (lambda (x) + (and (is-a? x <expandable-function>) + (get-code x))) + (get-definitions sys)))))) -;; (define (system->scheme sys) -;; `(begin -;; ,@(map (lambda (f) -;; `(define (,(function-name f) ,@(function-vars f)) -;; ,(code-expr (function-code f)))) -;; (reverse (filter (lambda (x) -;; (and (function*? x) -;; (function-code x))) -;; (get-definitions sys)))))) - -;; (define/guard (check (sys system?)) -;; (let loop ((sys sys) -;; (fails '())) -;; (let ((defs (get-definitions sys))) -;; (define* (next #:optional fail) -;; (loop (make-system (cdr defs) -;; (system-proofs sys) -;; (system-totality-claim-list sys)) -;; (if fail -;; (cons fail fails) -;; fails))) -;; (cond -;; ((null? defs) fails) -;; ((or (theorem? (car defs)) -;; (function? (car defs))) -;; (cond -;; ((and (function? (car defs)) -;; (trivial-total? (car defs) sys)) -;; (next)) -;; (else -;; (cond -;; ((find-proof (get-name (car defs)) sys) -;; => (lambda (pf) -;; (let ((result (prove sys (car defs) pf))) -;; (cond -;; ((equal? result ''#t) -;; (next)) -;; (else -;; (next (list (get-name (car defs)) -;; result))))))) -;; (else -;; (next (list (get-name (car defs))))))))) -;; (else -;; (next)))))) - -;; (define/guard (show (sys system?) (name symbol?)) -;; (cond -;; ((lookup name sys) -;; => (lambda (def) -;; (cond -;; ((function? def) -;; `(define-function ,(function-name def) ,(function-vars def) -;; ,(function-expression def))) -;; ((theorem? def) -;; `(define-theorem ,(theorem-name def) ,(theorem-vars def) -;; ,(theorem-expression def))) -;; ((axiom? def) -;; `(define-axiom ,(theorem-name def) ,(theorem-vars def) -;; ,(theorem-expression def))) -;; ((primitive-function? def) -;; `(define-primitive-function -;; ,(function-name def) -;; ,(function-vars def))) -;; (((cut is-a? <> <macro>) def) -;; `(define-syntax-rules ,(macro-name def))) -;; (else -;; `(error 'fatal-error ,name))))) -;; (else -;; `(error 'not-found ,name)))) - -;; (define/guard (load-system (sys system?)) -;; (primitive-eval (system->scheme sys))) - -;; (define/guard (system-primitives (sys system?)) -;; (append reserved-symbols -;; (map function-name -;; (filter primitive-function? -;; (get-definitions sys))))) - -;; (define/guard (system-functions (sys system?)) -;; (map function-name -;; (filter function? -;; (get-definitions sys)))) +(define (check sys) + (let loop ((sys sys) + (fails '())) + (if (system-empty? sys) + fails + (let ((d (first-definition sys)) + (sys-without-first (remove-first-definition sys))) + (define* (next #:optional fail) + (loop sys-without-first + (if fail + (cons fail fails) + fails))) + (cond + ((is-a? d <proved>) + (let ((result + (if (is-a? d <theorem>) + (rewrite sys-without-first + (get-claim d) + (get-proof d)) + (rewrite sys + (get-claim d) + (get-proof d))))) + (cond + ((equal? result ''#t) + (next)) + (else + (next (list (get-name d) result)))))) + ((is-a? d <provable>) + (next (list (get-name d)))) + (else (next))))))) -;; (define/guard (system-theorems (sys system?)) -;; (map theorem-name -;; (filter theorem? -;; (get-definitions sys)))) +(define (system? x) + (is-a? x <system>)) -;; (define/guard (system-axioms (sys system?)) -;; (map theorem-name -;; (filter axiom? -;; (get-definitions sys)))) +(define/guard (describe (sys system?) (name symbol?)) + (cond + ((lookup name sys) + => (lambda (def) + (cond + ((is-a? def <core-function>) + `(define-core-function ,(get-name def) ,(get-variables def))) + ((is-a? def <expandable-function>) + `(define-function ,(get-name def) ,(get-variables def) + ,(get-expression def))) + ((is-a? def <axiom>) + `(define-axiom ,(get-name def) ,(get-variables def) + ,(get-expression def))) + ((is-a? def <theorem*>) + `(define-theorem ,(get-name def) ,(get-variables def) + ,(get-expression def))) + (((cut is-a? <> <macro>) def) + `(define-syntax-rules ,(get-name def))) + (else + `(error 'fatal-error ,name))))) + (else + `(error 'not-found ,name)))) -;; (define/guard (system-macros (sys system?)) -;; (map macro-name -;; (filter (cut is-a? <> <macro>) -;; (get-definitions sys)))) +(define/guard (system-load (sys system?)) + (primitive-eval (system-code sys))) -;; (define/guard (system-totality-claims (sys system?)) -;; (system-totality-claim-list sys)) +;; (define/guard (system-environment (sys system?)) +;; (map (lambda (def) +;; (list (get-name def) +;; (show sys name))) +;; (get-definitions sys))) (define-system prelude () (define-core-function not (x) not) @@ -1505,9 +1488,22 @@ (lambda (x) (if (pair? x) (car x) '()))) (define-core-function cdr (x) (pair? x) (lambda (x) (if (pair? x) (cdr x) '()))) - (define-core-function + (x y) +) - (set-natural-predicate natural?) - (set-natural-less-than <) + (define-core-function + (x y) + (lambda (x y) + (if (number? x) + (if (number? y) + (+ x y) + x) + (if (number? y) + y + 0)))) + (set-measure-predicate natural?) + (set-measure-less-than <) + (define-trivial-total-function list-induction (x) + (if (not (pair? x)) + x + (cons (car x) + (list-induction (cdr x))))) (define-trivial-total-function size (x) (if (not (pair? x)) 0 @@ -1575,9 +1571,22 @@ (define-axiom cdr/cons (x y) (equal? (cdr (cons x y)) y)) + (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-axiom equal-car (x1 y1 x2 y2) (implies (equal? (cons x1 y1) (cons x2 y2)) (equal? x1 x2))) + + (define-theorem caar-cons2 (x y z) + (equal? (car (car (cons (cons x y) z))) x)) + (define-function app (x y) (if (not (pair? x)) y @@ -1586,4 +1595,22 @@ (define-theorem assoc-app (x y z) (equal? (app x (app y z)) - (app (app x y) z)))) + (app (app x y) z))) + + (define-proof caar-cons2 + (((1 1) car/cons) + ((1) car/cons) + (() equal-same))) + + (define-proof app + (size x) + (((2 3) size/cdr) + ((2) if-same) + ((1) natural/size) + (() if-true))) + + (define-proof assoc-app + (list-induction x) + ()) + ) + |