lists: remove-nth, shuffle: Add remove-nth and shuffle.

3 files changed, 88 insertions, 0 deletions

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))