From ab711cc5ce71ee2feaa4e88a0b9af113c2d67e3d Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 6 Aug 2021 00:54:14 +0900
Subject: peano: Remove unnecessary hypothesis.

---
 peano.lisp | 61 +++++++++++++++++++++----------------------------------------
 1 file changed, 21 insertions(+), 40 deletions(-)

(limited to 'peano.lisp')

diff --git a/peano.lisp b/peano.lisp
index 138527b..8c7f7d3 100644
--- a/peano.lisp
+++ b/peano.lisp
@@ -26,23 +26,15 @@
     ((or (z? x) (z? y)) nil)
     (t (nat= (pred x) (pred y)))))
 
+(defthm nat=-reflexive
+  (nat= x x))
 
+(defthm nat=-symmetric
+  (equal (nat= x y)
+         (nat= y x)))
 
-(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)
+(defthm nat=-transitive
+  (implies (and (nat= x y)
                 (nat= y z))
            (nat= x z)))
 
@@ -68,23 +60,9 @@
            (equal (nat+ nil x)
                   x)))
 
-(defthm nat+-left-not-zp
-  (implies (and (nat? x)
-                (not (z? x))
-                (nat? y))
-           (not (equal (nat+ x y)
-                       y))))
-
-(defthm nat+-right-not-zp
-  (implies (and (nat? x)
-                (nat? y)
-                (not (z? y)))
-           (not (equal (nat+ x y)
-                       x)))
-  :hints (("Goal" :in-theory (disable nat+-commutative)
-                  :use ((:instance nat+-commutative
-                                   (x x)
-                                   (y y))))))
+(defthm nat+-right-cancellative
+  (equal (equal (nat+ x k) (nat+ y k))
+         (equal x y)))
 
 (defthm nat+-left-cancellative
   (implies (and (nat? x)
@@ -92,11 +70,14 @@
                 (nat? k))
            (equal (equal (nat+ k x) (nat+ k y))
                   (equal x y)))
-  :hints (("Goal" :induct (nat= x y))))
-
-(defthm nat+-right-cancellative
-  (implies (and (nat? x)
-                (nat? y)
-                (nat? k))
-           (equal (equal (nat+ x k) (nat+ y k))
-                  (equal x y))))
+  :hints (("Goal" :in-theory (disable nat+-commutative)
+                  :use ((:instance nat+-commutative
+                                   (x x)
+                                   (y k))
+                        (:instance nat+-commutative
+                                   (x y)
+                                   (y k))))))
+
+(defthm associativity-of-nat+
+  (equal (nat+ x (nat+ y z))
+         (nat+ (nat+ x y) z)))
-- 
cgit v1.2.3