From f59adfbf19139706fffc97f8a35e4add214a8a9e Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Mon, 21 Dec 2020 12:37:29 +0900 Subject: wip61 --- vikalpa.scm | 39 +++++++++++++++-------- vikalpa/prelude.scm | 90 +++++++++++++++++++++++++++++++---------------------- 2 files changed, 78 insertions(+), 51 deletions(-) diff --git a/vikalpa.scm b/vikalpa.scm index 1c29e7e..5f7b16d 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -988,14 +988,21 @@ (syntax-rules () ((_ name (var ...) expr) (let ((f (let ((expression (convert-to-expression 'expr))) - (make (if (member 'name (expression-functions expression)) - - ) - #:name 'name - #:variables '(var ...) - #:conditions '() - #:expression expression - #:code (code 'expr))))) + (if (member 'name (expression-functions expression)) + (make + #:name 'name + #:variables '(var ...) + #:conditions '() + #:expression expression + #:code (code 'expr)) + (make + #:name 'name + #:variables '(var ...) + #:conditions '() + #:expression expression + #:code (code 'expr) + #:claim ''#t + #:proof '()))))) (current-system (add-definition f (current-system))) (validate f) f)))) @@ -1461,12 +1468,18 @@ (get-variables d) (get-expression d))) -(define/guard (system-apropos (sys system?) (str string?)) +(define* (system-apropos sys + str + #:key all?) (filter-map (lambda (d) - (if (string-match (string-append ".*" - (regexp-quote str) - ".*") - (symbol->string (get-name d))) + (if (and (or all? + (not (string-match "^%" + (symbol->string + (get-name d))))) + (string-match (string-append ".*" + (regexp-quote str) + ".*") + (symbol->string (get-name d)))) (list (get-name d) (show d)) #f)) (get-definitions sys))) diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 9fb7571..66d2b73 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -17,12 +17,7 @@ ;;; along with Vikalpa. If not, see . (define-module (vikalpa prelude) - #:export (exact-positive-integer? - exact-negative-integer? - succ pred - implies - negate - prelude) + #:export (prelude) #:use-module (vikalpa)) (define (exact-positive-integer? x) @@ -96,22 +91,28 @@ (equal? (if (not x) y z) (if x z y)))) -(define-system prelude/number (prelude/if) +(define-system prelude/integer (prelude/if) (define-core-function integer? (x) exact-integer?) (define-core-function positive-integer? (x) exact-positive-integer?) - (define-core-function negative-integer? (x) exact-negative-integer?) - (define-core-function negate (x) negate) - (define-function natural? (x) - (if (integer? x) - (not (negative-integer? x)) - #f)) (define-function zero? (x) (equal? x 0)) - (define-core-function succ (x) succ) - (define-core-function pred (x) pred) + (define-function natural? (x) + (if (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) @@ -126,7 +127,7 @@ #f)))) (set-measure-predicate natural?) (set-measure-less-than <) - (define-axiom integer?-is-predicate (x) + (define-axiom integer?/true (x) (implies (integer? x) (equal? (integer? x) #t))) (define-axiom integer/pred (x) @@ -144,7 +145,7 @@ (define-axiom natural/pred (x) (implies (positive-integer? x) (equal? (natural? (pred x)) #t))) - (define-axiom positive-integer/succ (x) + (define-axiom positive-integer/pred (x) (implies (natural? x) (equal? (positive-integer? (pred x)) #t))) (define-axiom positive-integer-is-integer (x) @@ -200,9 +201,7 @@ x) 0)) (define-theorem natural-is-integer (x) - (if (natural? x) - (equal? (integer? x) #t) - #t)) + (implies (natural? x) (equal? (integer? x) #t))) (define-theorem natural/abs (x) (equal? (natural? (abs x)) #t)) (define-theorem zero-is-0 (x) @@ -215,16 +214,16 @@ (implies (natural? x) (not (zero? x)) (equal? (positive-integer? x) #t))) - (define-theorem %abs/pred--zero/pred (x) + (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) + (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) + (define-theorem %%abs/pred-1 (x) (implies (positive-integer? x) (positive-integer? (pred x)) (equal? (< (pred x) x) #t))) @@ -242,6 +241,12 @@ 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)) @@ -249,7 +254,7 @@ (pred (+ (succ x) y)) y)))) -(define-system prelude/pair (prelude/number) +(define-system prelude/pair (prelude/integer) (define-core-function pair? (x) pair?) (define-core-function cons (x y) cons) (define-core-function car (x) @@ -333,26 +338,26 @@ ((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 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 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 + (define-proof %%abs/pred-1 (natural-induction x) (((2 2 1 1) zero-is-0) ((2 2 1) positive-integer?) @@ -379,8 +384,8 @@ ((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 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) @@ -391,7 +396,7 @@ ((3) if-false) (() if-same))) - (define-proof %abs/pred--x-is-1 + (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) @@ -401,7 +406,7 @@ ((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 1) %%abs/pred--zero/pred) ((2 2 2 2) if-true) ((2 2 2 1) natural-is-integer) ((2 2 2) if-true) @@ -410,7 +415,7 @@ ((2) if-same) (() if-same))) - (define-proof %abs/pred--zero/pred + (define-proof %%abs/pred--zero/pred (((2 2 1) natural?) ((2 2 1) if-nest) ((2 2 2) if-same (set x (zero? x))) @@ -480,6 +485,15 @@ ((2) if-same) (() if-same))) + (define-proof integer-induction + (abs x) + (((1) natural/abs) + (() if-true) + ((2) abs/pred) + ((3 2) abs/succ) + ((3) if-same) + (() if-same))) + (define-proof + (abs x) (((1) natural/abs) -- cgit v1.2.3