From e58aa4ff8291a2a7972075b04ca2b3f5ced342ad Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sat, 21 Nov 2020 06:13:13 +0900 Subject: wip31 --- vikalpa.scm | 28 +++++---- vikalpa/prelude.scm | 6 +- vikalpa/the-little-prover.scm | 142 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 158 insertions(+), 18 deletions(-) create mode 100644 vikalpa/the-little-prover.scm diff --git a/vikalpa.scm b/vikalpa.scm index f4ef953..5be2824 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -324,7 +324,7 @@ (eq? 'system (list-ref x 0)) (system-definitions? (system-definitions x)) (system-proofs? (system-proofs x)) - ((const #t) (system-totality-claims x)))) + ((const #t) (system-totality-claim-list x)))) (define (make-system defs prfs totality-claims) (list 'system defs prfs totality-claims)) @@ -335,7 +335,7 @@ (define (system-proofs sys) (list-ref sys 2)) -(define/guard (system-totality-claims (sys system?)) +(define (system-totality-claim-list sys) (list-ref sys 3)) (define (totality-claim id nat? less-than) @@ -628,7 +628,7 @@ (- x 1)) (define (natural->expr n) - (if (zero? n) + (if (<= n 0) ''0 `(succ ,(natural->expr (pred n))))) @@ -946,12 +946,12 @@ (cond ((lookup (definition-name x) sys) => (lambda (d) (if (equal? x d) - x + sys (error "(vikalpa) add-definition: duplicated" (definition-name d))))) (else (make-system (cons x (system-definitions sys)) (system-proofs sys) - (system-totality-claims sys))))) + (system-totality-claim-list sys))))) x)) (define (add-proof x) @@ -964,7 +964,7 @@ (error "add-proof: duplicated")))) (else (make-system (system-definitions sys) (cons x (system-proofs sys)) - (system-totality-claims sys))))) + (system-totality-claim-list sys))))) x)) (define reserved-symbols '(quote let if error)) @@ -1026,7 +1026,7 @@ m)))) (define (find-totality-claim name sys) - (assoc name (system-totality-claims sys))) + (assoc name (system-totality-claim-list sys))) (define (add-totality-claim tc) (let ((sys (current-system))) @@ -1047,14 +1047,13 @@ (current-system (make-system (system-definitions sys) (system-proofs sys) - (cons tc (system-totality-claims sys)))) - tc)) + (cons tc (system-totality-claim-list sys)))))) (define-syntax-rule (define-totality-claim name nat? <) (add-totality-claim (totality-claim 'name 'nat? '<))) (define* (core-system #:optional (parent (make-system '() '() '()))) - (parameterize ([current-system parent]) + (parameterize ((current-system parent)) (define-primitive-function not (x)) (define-primitive-function equal? (x y)) (define-primitive-function cons (x y)) @@ -1068,8 +1067,8 @@ (syntax-rules () ((_ name (systems ...) expr ...) (define* (name #:optional (parent (make-system '() '() '()))) - (parameterize ([current-system - ((compose systems ... core-system) parent)]) + (parameterize ((current-system + ((compose systems ... core-system) parent))) expr ... (unless (system? (current-system)) @@ -1342,7 +1341,7 @@ (define* (next #:optional fail) (loop (make-system (cdr defs) (system-proofs sys) - (system-totality-claims sys)) + (system-totality-claim-list sys)) (if fail (cons fail fails) fails))) @@ -1428,3 +1427,6 @@ (map macro-name (filter macro? (system-definitions sys)))) + +(define/guard (system-totality-claims (sys system?)) + (system-totality-claim-list sys)) diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index c55ea48..35f91dd 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -28,11 +28,6 @@ (define-system prelude () (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? <) @@ -40,6 +35,7 @@ (define-syntax-rules list () ((list) '()) ((list x . y) (cons x (list . y)))) + (define-syntax-rules and () ((and) '#t) ((and x) x) diff --git a/vikalpa/the-little-prover.scm b/vikalpa/the-little-prover.scm new file mode 100644 index 0000000..fd71082 --- /dev/null +++ b/vikalpa/the-little-prover.scm @@ -0,0 +1,142 @@ +;;; Vikalpa --- Proof Assistant +;;; Copyright © 2020 Masaya Tojo +;;; +;;; This file is part of Vikalpa. +;;; +;;; Vikalpa is free software; you can redistribute it and/or modify it +;;; under the terms of the GNU General Public License as published by +;;; the Free Software Foundation; either version 3 of the License, or +;;; (at your option) any later version. +;;; +;;; Vikalpa is distributed in the hope that it will be useful, but +;;; WITHOUT ANY WARRANTY; without even the implied warranty of +;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU +;;; General Public License for more details. +;;; +;;; You should have received a copy of the GNU General Public License +;;; along with Vikalpa. If not, see . + +(define-module (vikalpa the-little-prover) + #:export (atom? the-little-prover) + #:use-module (vikalpa)) + +(define (atom? x) + (not (pair? x))) + +(define (size x) + (if (atom? x) + 0 + (+ (size (car x)) + (size (cdr x))))) + +(define-system the-little-prover () + (define-primitive-function atom? (x)) + (define-primitive-function size (x)) + (define-primitive-function + (x y)) + (define-primitive-function natural? (x)) + (define-primitive-function < (x y)) + (define-totality-claim natural? natural? <) + + ;; Axioms of Equal + (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) + (if (equal? x y) (equal? x y) #t)) + + ;; Axioms of Cons + (define-axiom atom/cons (x y) + (equal? (atom? (cons x y)) #f)) + (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))) + + ;; Axioms of If + (define-axiom if-true (x y) + (equal? (if #t x y) x)) + (define-axiom if-false (x y) + (equal? (if #f x y) y)) + (define-axiom if-same (x y) + (equal? (if x y y) y)) + (define-axiom if-nest-A (x y z) + (if x (equal? (if x y z) y) #t)) + (define-axiom if-nest-E (x y z) + (if x #t (equal? (if x y z) z))) + + ;; Axioms of Size + (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))) + + ;; Axioms of `+` and `<` + (define-axiom identity-+ (x) + (if (natural? x) + (equal? (+ (+ x y) z)) + #t)) + (define-axiom commute-+ (x y) + (equal? (+ x y) (+ y x))) + (define-axiom associate-+ (x y z) + (equal? (+ (+ x y) z) (+ x (+ y z)))) + (define-axiom positive-+ (x y) + (if (< '0 x) + (if (< '0 y) + (equal? (< '0 (+ x y)) #t) + #t) + #t)) + (define-axiom natural?/+ (x y) + (if (natural? x) + (if (natural? y) + (equal? (natural? (+ x y)) #t) + #t) + #t)) + (define-axiom common-addends-< (x y z) + (equal? (< (+ x z) (+ y z) (< x y)))) + + ;; Axioms for Vikalpa + (define-axiom natural?/0 () + (equal? (natural? '0) #t)) + (define-axiom natural?/succ (x) + (if (natural? x) + (equal? (natural? (succ x)) #t) + #t)) + + + ;; Prelude + (define-function list-induction (x) + (if (atom? x) + x + (cons (car x) + (list-induction (cdr x))))) + + (define-proof list-induction + (natural? (size x)) + (((2 3) size/cdr) + ((2) if-same) + (() if-same))) + + (define-function star-induction (x) + (if (atom? x) + x + (cons (star-induction (car x)) + (star-induction (cdr x))))) + + (define-proof star-induction + (natural? (size x)) + (((2 3 1) size/car) + ((2 3 2) size/cdr) + ((2 3) if-true) + ((2) if-same) + (() if-same)))) -- cgit v1.2.3