diff options
author | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-21 06:13:13 +0900 |
---|---|---|
committer | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-21 06:13:13 +0900 |
commit | e58aa4ff8291a2a7972075b04ca2b3f5ced342ad (patch) | |
tree | 4787a23a61b6d348df467a02c82be82ef49bdf9a /vikalpa/the-little-prover.scm | |
parent | 6ac3c8c7d47cb68d0edc87dbf9a3d3dc1610bbd4 (diff) |
wip31
Diffstat (limited to 'vikalpa/the-little-prover.scm')
-rw-r--r-- | vikalpa/the-little-prover.scm | 142 |
1 files changed, 142 insertions, 0 deletions
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 <masaya@tojo.tokyo> +;;; +;;; 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 <http://www.gnu.org/licenses/>. + +(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)))) |