From 8ada9230a681e8c1ee23686815c866d6eebde7e8 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 16 Jul 2022 15:34:00 +0900
Subject: lists: remove-nth, shuffle: Add remove-nth and shuffle.

---
 Makefile              | 12 ++++++------
 lists/Makefile        | 22 ++++++++++++++++++++++
 lists/remove-nth.lisp | 20 ++++++++++++++++++++
 lists/shuffle.lisp    | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 94 insertions(+), 6 deletions(-)
 create mode 100644 lists/Makefile
 create mode 100644 lists/remove-nth.lisp
 create mode 100644 lists/shuffle.lisp

diff --git a/Makefile b/Makefile
index f86226c..c30f9d8 100644
--- a/Makefile
+++ b/Makefile
@@ -1,16 +1,16 @@
-.PHONY: clean all
+subdirs := lists
 
-all: huffman-encode.cert perm.cert
+.PHONY: clean all $(subdirs)
+
+all: huffman-encode.cert $(subdirs)
 
 huffman-encode.cert: huffman-encode.lisp
 	-rm -f $@
 	acl2 <<< '(CERTIFY-BOOK "$(basename $@)")'
 	test -f $@
 
-perm.cert: perm.lisp
-	-rm -f $@
-	acl2 <<< '(CERTIFY-BOOK "$(basename $@)")'
-	test -f $@
+$(subdirs):
+	$(MAKE) -C $@
 
 clean:
 	rm -f *.{cert,fasl,port,lx64fsl}
diff --git a/lists/Makefile b/lists/Makefile
new file mode 100644
index 0000000..4f5d8ca
--- /dev/null
+++ b/lists/Makefile
@@ -0,0 +1,22 @@
+.PHONY: clean all
+
+all: remove-nth.cert shuffle.cert perm.cert
+
+remove-nth.cert: remove-nth.lisp
+	-rm -f $@
+	acl2 <<< '(CERTIFY-BOOK "$(basename $@)")'
+	test -f $@
+
+perm.cert: perm.lisp
+	-rm -f $@
+	acl2 <<< '(CERTIFY-BOOK "$(basename $@)")'
+	test -f $@
+
+shuffle.cert: shuffle.lisp remove-nth.cert perm.cert
+	-rm -f $@
+	acl2 <<< '(CERTIFY-BOOK "$(basename $@)")'
+	test -f $@
+
+clean:
+	rm -f *.{cert,fasl,port,lx64fsl}
+
diff --git a/lists/remove-nth.lisp b/lists/remove-nth.lisp
new file mode 100644
index 0000000..8c62e9d
--- /dev/null
+++ b/lists/remove-nth.lisp
@@ -0,0 +1,20 @@
+(in-package "ACL2")
+
+(defun remove-nth (i x)
+  (declare (xargs :guard (and (natp i)
+                              (true-listp x))))
+  (cond ((endp x) nil)
+        ((zp i) (cdr x))
+        (t
+         (cons (car x)
+               (remove-nth (1- i) (cdr x))))))
+
+(defthm len-remove-nth
+  (implies (and (consp x)
+                (< i (len x)))
+           (equal (len (remove-nth i x))
+                  (- (len x) 1))))
+
+(defthm true-listp-remove-nth
+   (implies (true-listp x)
+            (true-listp (remove-nth i x))))
diff --git a/lists/shuffle.lisp b/lists/shuffle.lisp
new file mode 100644
index 0000000..7fa59ca
--- /dev/null
+++ b/lists/shuffle.lisp
@@ -0,0 +1,46 @@
+(in-package "ACL2")
+
+(include-book "remove-nth")
+(include-book "perm")
+
+(include-book "std/util/bstar" :dir :system)
+(local (include-book "system/random" :dir :system))
+(local (include-book "tools/mv-nth" :dir :system))
+(local (include-book "std/lists/len" :dir :system))
+
+(defun shuffle (x state)
+  (declare (xargs :stobjs state
+                  :measure (len x)
+                  :guard (true-listp x)))
+  (if (endp x)
+      (mv nil state)
+      (b* (((mv i state) (random$ (len x) state))
+           ((mv result state) (shuffle (remove-nth i x) state)))
+        (mv (cons (nth i x) result) state))))
+
+(local
+ (defthm nth-member
+   (implies (and (consp x)
+                 (equal (nth i x) e)
+                 (< i (len x)))
+            (member-equal e x))
+   :rule-classes (:rewrite :forward-chaining)))
+
+(local
+ (defthm remove-nth-remove1
+   (implies (and (consp x)
+                 (< i (len x)))
+            (perm (remove-nth i x)
+                  (remove1 (nth i x) x)))
+   :hints (("Goal" :induct (remove-nth i x))
+           ("Subgoal *1/3.8'"
+            :cases ((consp (cdr x)))))))
+
+(local
+ (defthm member-nth
+   (implies (and (consp x)
+                 (< i (len x)))
+            (member (nth i x) x))))
+
+(defthm perm-shuffle
+  (perm (mv-nth 0 (shuffle x state)) x))
-- 
cgit v1.2.3