From a66e8352af2ee48d59047a79a158ffda392556b4 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 4 Sep 2021 18:30:36 +0900
Subject: binary-tree: Change from member to assoc.

---
 binary-tree.lisp | 145 +++++++++++++++++++++++++++++++++----------------------
 1 file changed, 86 insertions(+), 59 deletions(-)

diff --git a/binary-tree.lisp b/binary-tree.lisp
index 037da4f..b26b8fb 100644
--- a/binary-tree.lisp
+++ b/binary-tree.lisp
@@ -1,9 +1,15 @@
 (defun emptyp (x)
-  (atom x))
+ (atom x))
 
-(defun val (x)
+(defun kv (x)
   (car x))
 
+(defmacro key (x)
+  `(car (kv ,x)))
+
+(defmacro val (x)
+  `(cdr (kv ,x)))
+
 (defun left (x)
   (cadr x))
 
@@ -36,36 +42,37 @@
   (if (emptyp x)
       t
       (and (lessp (left x) e)
-           (< (val x) e)
+           (< (car (kv x)) e)
            (lessp (right x) e))))
 
 (defun overp (x e)
   (if (emptyp x)
       t
       (and (overp (left x) e)
-           (< e (val x))
+           (< e (car (kv x)))
            (overp (right x) e))))
 
 (defun treep (x)
   (if (emptyp x)
       (null x)
       (and (consp x)
-           (rationalp (car x))
+           (consp (car x))
            (consp (cdr x))
-           (treep (cadr x))
            (consp (cddr x))
-           (treep (caddr x))
-           (lessp (left x) (val x))
-           (overp (right x) (val x))
-           (null (cdddr x)))))
+           (null (cdddr x))
+           (rationalp (key x))
+           (treep (left x))
+           (treep (right x))
+           (lessp (left x) (key x))
+           (overp (right x) (key x)))))
 
-(defun tree (x l r)
-  (list x l r))
+(defun tree (k v l r)
+  (list (cons k v) l r))
 
 (defthm tree-elim
   (implies (and (treep x)
                 (not (emptyp x)))
-           (equal (tree (val x) (left x) (right x))
+           (equal (tree (key x) (val x) (left x) (right x))
                   x))
   :rule-classes :elim)
 
@@ -79,100 +86,120 @@
                 (not (emptyp x)))
            (treep (right x))))
 
-(defthm rationalp-val
+(defthm consp-kv
+  (implies (and (treep x)
+                (not (emptyp x)))
+           (consp (kv x))))
+
+(defthm rationalp-key
   (implies (and (treep x)
                 (not (emptyp x)))
-           (rationalp (val x))))
+           (rationalp (key x))))
 
 (defthm lessp-left
   (implies (and (treep x)
                 (not (emptyp x)))
-           (lessp (left x) (val x))))
+           (lessp (left x) (key x))))
 
 (defthm overp-right
   (implies (and (treep x)
                 (not (emptyp x)))
-           (overp (right x) (val x))))
+           (overp (right x) (key x))))
 
 (defthm treep-tree
-  (implies (and (rationalp x)
+  (implies (and (rationalp k)
                 (treep l)
                 (treep r)
-                (lessp l x)
-                (overp r x))
-           (treep (tree x l r)))
+                (lessp l k)
+                (overp r k))
+           (treep (tree k v l r)))
   :rule-classes (:rewrite))
 
-(in-theory (disable emptyp treep val tree left right tree-count))
+(in-theory (disable emptyp treep kv tree left right tree-count))
 
-(defun tree-memberp (e x)
+(defun tree-assoc (k x)
   (declare (xargs :measure (tree-count x)))
   (if (emptyp x)
       nil
-      (if (= (val x) e)
-          t
-          (if (< e (val x))
-              (tree-memberp e (left x))
-              (tree-memberp e (right x))))))
+      (if (= (key x) k)
+          (kv x)
+          (if (< k (key x))
+              (tree-assoc k (left x))
+              (tree-assoc k (right x))))))
 
-(defthm lessp-not-member
+(defthm lessp-not-assoc
   (implies (and (treep x)
-                (lessp x e))
-           (not (tree-memberp e x)))
-  :hints (("Goal" :induct (lessp x e))))
+                (lessp x k))
+           (not (tree-assoc k x)))
+  :hints (("Goal" :induct (lessp x k))))
 
-(defthm overp-not-member
+(defthm overp-not-assoc
   (implies (and (treep x)
-                (overp x e))
-           (not (tree-memberp e x)))
-  :hints (("Goal" :induct (overp x e))))
+                (overp x k))
+           (not (tree-assoc k x)))
+  :hints (("Goal" :induct (overp x k))))
 
-(defthm not-tree-memberp-lemma-lessp2
+(defthm not-tree-assoc-lemma-lessp2
   (implies (and (treep x)
                 (<= e1 e2)
                 (lessp x e1))
            (lessp x e2))
   :rule-classes ((:rewrite :match-free :all)))
 
-(defthm not-tree-memberp-lemma-overp2
+(defthm not-tree-assoc-lemma-overp2
   (implies (and (treep x)
                 (< e1 e2)
                 (overp x e2))
            (overp x e1))
   :rule-classes ((:rewrite :match-free :all)))
 
-(defthm not-tree-memberp
+(defthm not-tree-assoc
   (implies (and (treep x)
                 (not (emptyp x)))
-           (if (= e (val x))
+           (if (= k (key x))
                t
-               (if (< e (val x))
-                   (not (tree-memberp e (right x)))
-                   (not (tree-memberp e (left x))))))
-  :hints (("Goal" :induct (tree-memberp e x))))
+               (if (< k (key x))
+                   (not (tree-assoc k (right x)))
+                   (not (tree-assoc k (left x))))))
+  :hints (("Goal" :induct (tree-assoc k x))))
 
-(defun tree-to-list (x)
+(defun tree-to-alist (x)
   (declare (xargs :measure (tree-count x)))
   (if (emptyp x)
       nil
-      (append (tree-to-list (left x))
-              (list (val x))
-              (tree-to-list (right x)))))
+      (append (tree-to-alist (left x))
+              (list (kv x))
+              (tree-to-alist (right x)))))
+
+(defthm alistp-append
+  (implies (true-listp x)
+           (iff (alistp (append x y))
+                (and (alistp x)
+                     (alistp y)))))
+
+(defthm alistp-tree-to-alist
+  (implies (treep x)
+           (alistp (tree-to-alist x))))
+
+(defthm assoc-append-nil
+  (equal (assoc-equal k (append nil x))
+         (assoc-equal k x)))
 
-(defthm member-append
-  (iff (member e (append x y))
-       (or (member e x)
-           (member e y))))
+(defthm assoc-append
+  (implies (alistp x)
+           (equal (assoc k (append x y))
+                  (or (assoc k x)
+                      (assoc k y)))))
 
-(defthm tree-memberp-member-tree-to-list
+(defthm tree-assoc-assoc-tree-to-list
   (implies (treep x)
-           (iff (tree-memberp e x)
-                (member e (tree-to-list x))))
+           (equal (tree-assoc k x)
+                  (assoc k (tree-to-alist x))))
   :rule-classes nil)
 
-(defthm member-tree-to-list-tree-memberp
+(defthm assoc-tree-to-list-tree-assoc
   (implies (treep x)
-           (iff (member e (tree-to-list x))
-                (tree-memberp e x)))
-  :hints (("Goal" :use (tree-memberp-member-tree-to-list)))
+           (equal (assoc k (tree-to-alist x))
+                  (tree-assoc k x)))
+  :hints (("Goal" :use (tree-assoc-assoc-tree-to-list)))
   :rule-classes nil)
-- 
cgit v1.2.3