diff options
Diffstat (limited to 'lists')
| -rw-r--r-- | lists/Makefile | 22 | ||||
| -rw-r--r-- | lists/remove-nth.lisp | 20 | ||||
| -rw-r--r-- | lists/shuffle.lisp | 46 |
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)) |