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

---
 examples/the-little-prover.scm | 57 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)
 create mode 100644 examples/the-little-prover.scm

diff --git a/examples/the-little-prover.scm b/examples/the-little-prover.scm
new file mode 100644
index 0000000..0a12eaa
--- /dev/null
+++ b/examples/the-little-prover.scm
@@ -0,0 +1,57 @@
+(use-modules (vikalpa)
+             (vikalpa the-little-prover)
+             (ice-9 pretty-print))
+
+(define-system the-little-prover-0 (the-little-prover)
+  (define-theorem simple-list-induction (x)
+    (equal? (if (natural? (size x))
+                (if (atom? x) '#t (< (size (cdr x)) (size x)))
+                '#t)
+            #t))
+
+  (define-proof simple-list-induction
+    ()
+    (((1 2 3) size/cdr)
+     ((1 2) if-same)
+     ((1) if-same)
+     (() equal-same)))
+
+  (define-function list-length (xs)
+    (if (atom? xs)
+        '0
+        (+ '1 (list-length (cdr xs)))))
+
+  (define-proof list-length
+    (natural? (size xs))
+    ((() simple-list-induction)))
+
+  (define-theorem natural?/1 ()
+    (equal? (natural? 1) #t))
+
+  (define-proof natural?/1
+    ()
+    ((() if-same (set x (natural? '0)))
+     ((2 1) natural?/succ)
+     ((2) equal-same)
+     ((1) natural?/0)
+     (() if-true)))
+
+  (define-theorem natural?/list-length (xs)
+    (natural? (list-length xs)))
+
+  (define-proof natural?/list-length
+    (list-induction xs)
+    (((2 1) list-length)
+     ((2 1) if-nest-A)
+     ((2) natural?/0)
+     ((3 2 1) list-length)
+     ((3 2 1) if-nest-E)
+     ((3) if-same (set x (natural? (succ '0))))
+     ((3 2 2) natural?/+
+      ;; ルール探索アルゴリズムにバグがある
+      (set x (succ '0))
+      (set y (list-length (cdr xs))))
+     ((3 2) if-same)
+     ((3 1) natural?/1)
+     ((3) if-true)
+     (() if-same))))
-- 
cgit v1.2.3