1 files changed, 46 insertions, 0 deletions
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))