From e58aa4ff8291a2a7972075b04ca2b3f5ced342ad Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 21 Nov 2020 06:13:13 +0900
Subject: wip31

---
 vikalpa/prelude.scm           |   6 +-
 vikalpa/the-little-prover.scm | 142 ++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 143 insertions(+), 5 deletions(-)
 create mode 100644 vikalpa/the-little-prover.scm

(limited to 'vikalpa')

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 <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))))
-- 
cgit v1.2.3