peano: Add peano.lisp file.

1 files changed, 102 insertions, 0 deletions

diff --git a/peano.lisp b/peano.lisp
new file mode 100644
index 0000000..791e04e
--- /dev/null
+++ b/peano.lisp
@@ -0,0 +1,102 @@
+(defmacro zero? (x)
+  `(equal ,x nil))
+
+(defmacro z? (x)
+  `(atom ,x))
+
+(defmacro succ (x)
+  `(cons nil ,x))
+
+(defmacro pred (x)
+  `(cdr ,x))
+
+(defun nat? (x)
+  (if (z? x)
+      (null x)
+      (and (equal (car x) nil)
+           (nat? (pred x)))))
+
+(defthm zero-is-nat
+  (implies (zero? x)
+           (nat? x)))
+
+(defun nat= (x y)
+  (cond
+    ((and (z? x) (z? y)) t)
+    ((or (z? x) (z? y)) nil)
+    (t (nat= (pred x) (pred y)))))
+
+
+
+(defthm nat-reflexive
+  (implies (nat? x)
+           (nat= x x)))
+
+(defthm nat-symmetric
+  (implies (and (nat? x)
+                (nat? y))
+           (equal (nat= x y)
+                  (nat= y x))))
+
+(defthm nat-transitive
+  (implies (and (nat? x)
+                (nat? y)
+                (nat? z)
+                (nat= x y)
+                (nat= y z))
+           (nat= x z)))
+
+(defthm nat=-to-equal
+  (implies (and (nat? x)
+                (nat? y))
+           (equal (nat= x y)
+                  (equal x y))))
+
+(defun nat+ (x y)
+  (if (z? y)
+      x
+      (succ (nat+ x (pred y)))))
+
+(defthm nat+-commutative
+  (implies (and (nat? x)
+                (nat? y))
+           (equal (nat+ x y)
+                  (nat+ y x))))
+
+(defthm nat+-zero
+  (implies (nat? x)
+           (equal (nat+ nil x)
+                  x)))
+
+(defthm nat+-cancellative-1-1-1
+  (implies (and (consp x)
+                (nat? x)
+                (nat? k))
+           (not (equal (nat+ x k)
+                       k))))
+
+(defthm nat+-cancellative-1-1
+  (implies (and (consp x)
+                (nat? x)
+                (nat? k))
+           (not (equal (nat+ k x)
+                       k)))
+  :hints (("Goal" :in-theory (disable nat+-commutative)
+                  :use ((:instance nat+-commutative
+                                    (x x)
+                                    (y k))))))
+
+(defthm nat+-cancellative-1
+  (implies (and (consp x)
+                (nat? x)
+                (nat? k))
+           (not (equal (nat+ k x)
+                       k))))
+
+(defthm nat+-cancellative
+  (implies (and (nat? x)
+                (nat? y)
+                (nat? k))
+           (equal (equal (nat+ k x) (nat+ k y))
+                  (equal x y)))
+  :hints (("Goal" :induct (nat= x y))))