(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 :match-free :all)
                  (:forward-chaining :match-free :all))))

(local
 (defthm remove-nth-remove1
   (implies (and (consp x)
                 (< i (len x)))
            (perm (remove-nth i x)
                  (remove1 (nth i x) (double-rewrite 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)) (double-rewrite x)))