summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2022-07-14 00:11:44 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2022-07-14 00:11:44 +0900
commit7c6f69eb7a623782396075a1f126c2c665d704e4 (patch)
tree8345276b57e1a3980e3a69a29b67857f1c3f9533
parent577a3d6e856eb92bbab88f797ec54e6d29188d3d (diff)
Add huffman-encode.
-rw-r--r--Makefile12
-rw-r--r--huffman-encode.lisp481
2 files changed, 493 insertions, 0 deletions
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..b4f00d1
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,12 @@
+.PHONY: clean all
+
+all: huffman-encode.cert
+
+huffman-encode.cert: huffman-encode.lisp
+ -rm -f $@
+ acl2 <<< '(CERTIFY-BOOK "$(basename $@)")'
+ test -f $@
+
+clean:
+ rm -f *.{cert,fasl,port,lx64fsl}
+
diff --git a/huffman-encode.lisp b/huffman-encode.lisp
new file mode 100644
index 0000000..eeaa38f
--- /dev/null
+++ b/huffman-encode.lisp
@@ -0,0 +1,481 @@
+;;; Provide Huffman encoding
+(in-package "ACL2")
+
+;;; Deine Huffman tree
+(defun nodep (x)
+ (declare (xargs :guard t))
+ (and (consp x)
+ (eq (car x) 'node)))
+
+(defun huffman-treep (x)
+ (declare (xargs :guard t))
+ (flet ((symbol-list (x)
+ (if (nodep x)
+ (second x)
+ (list (second x)))))
+ (if (nodep x)
+ (and (true-listp x)
+ (equal (len x) 5)
+ (true-listp (second x))
+ (rationalp (third x))
+ (huffman-treep (fourth x))
+ (huffman-treep (fifth x))
+ (equal (second x)
+ (append (symbol-list (fourth x))
+ (symbol-list (fifth x))))
+ (equal (third x)
+ (+ (third (fourth x))
+ (third (fifth x)))))
+ (and (true-listp x)
+ (equal (len x) 3)
+ (equal (first x) 'leaf)
+ (rationalp (third x))))))
+
+(defun huffman-leaf (s w)
+ (declare (xargs :guard (rationalp w)))
+ (list 'leaf s w))
+
+(defun huffman-leafp (x)
+ (declare (xargs :guard t))
+ (and (huffman-treep x)
+ (not (nodep x))))
+
+(defun leaf-symbol (x)
+ (declare (xargs :guard (and (huffman-treep x)
+ (not (nodep x)))))
+ (second x))
+
+(defun symbol-list (x)
+ (declare (xargs :guard (huffman-treep x)))
+ (if (nodep x)
+ (second x)
+ (list (second x))))
+
+(defun weight (x)
+ (declare (xargs :guard (huffman-treep x)))
+ (third x))
+
+(defun left (x)
+ (declare (xargs :guard (and (huffman-treep x)
+ (nodep x))))
+ (fourth x))
+
+(defun right (x)
+ (declare (xargs :guard (and (huffman-treep x)
+ (nodep x))))
+ (fifth x))
+
+(defun huffman-node (l r)
+ (declare (xargs :guard (and (huffman-treep l)
+ (huffman-treep r))))
+ (list 'node
+ (append (symbol-list l)
+ (symbol-list r))
+ (+ (weight l) (weight r))
+ l
+ r))
+
+(defthm huffman-leaf-elim
+ (implies (and (not (nodep x))
+ (huffman-treep x))
+ (equal (huffman-leaf (leaf-symbol x)
+ (weight x))
+ x))
+ :rule-classes :elim)
+
+(defthm len=5
+ (implies (true-listp x)
+ (equal (equal (len x) 5)
+ (and (consp x)
+ (consp (cdr x))
+ (consp (cddr x))
+ (consp (cdddr x))
+ (consp (cddddr x))
+ (null (cdr (cddddr x)))))))
+
+(defthm huffman-node-elim
+ (implies (and (nodep x)
+ (huffman-treep x))
+ (equal (huffman-node (left x) (right x))
+ x))
+ :hints (("Goal" :use len=5
+ :in-theory (disable len=5)))
+ :rule-classes :elim)
+
+(defun node-count (x)
+ (if (nodep x)
+ (+ 1
+ (node-count (left x))
+ (node-count (right x)))
+ 0))
+
+(defthm node-count-left
+ (implies (nodep x)
+ (< (node-count (left x))
+ (node-count x)))
+ :rule-classes :linear)
+
+(defthm node-count-right
+ (implies (nodep x)
+ (< (node-count (right x))
+ (node-count x)))
+ :rule-classes :linear)
+
+(defthm huffman-treep-huffman-node
+ (implies (and (huffman-treep l)
+ (huffman-treep r))
+ (huffman-treep (huffman-node l r))))
+
+(defthm nodep-huffman-node
+ (implies (and (huffman-treep l)
+ (huffman-treep r))
+ (nodep (huffman-node l r))))
+
+(defthm symbol-list-left-right
+ (implies (and (nodep x)
+ (huffman-treep x))
+ (equal (symbol-list x)
+ (append (symbol-list (left x))
+ (symbol-list (right x))))))
+
+(defthm weight-left-right
+ (implies (and (nodep x)
+ (huffman-treep x))
+ (equal (weight x)
+ (+ (weight (left x))
+ (weight (right x))))))
+
+(defthm huffman-treep-left
+ (implies (and (nodep x)
+ (huffman-treep x))
+ (huffman-treep (left x))))
+
+(defthm huffman-treep-right
+ (implies (and (nodep x)
+ (huffman-treep x))
+ (huffman-treep (right x))))
+
+(defthm true-listp-symbol-list
+ (implies (huffman-treep x)
+ (true-listp (symbol-list x))))
+
+(defthm symbol-list-leaf
+ (implies (and (huffman-treep x)
+ (not (nodep x)))
+ (equal (symbol-list x)
+ (list (leaf-symbol x)))))
+
+(defthm rationalp-weight
+ (implies (huffman-treep x)
+ (rationalp (weight x))))
+
+(defthm rationalp-weight-2
+ (implies (and (not (nodep (huffman-leaf lsl wt)))
+ (huffman-treep (huffman-leaf lsl wt)))
+ (rationalp wt)))
+
+(defthm huffman-treep-huffman-leaf
+ (implies (rationalp w)
+ (huffman-treep (huffman-leaf s w))))
+
+(in-theory (disable
+ nodep huffman-treep
+ leaf-symbol
+ huffman-leaf huffman-node
+ symbol-list weight left right
+ node-count))
+
+;;; Generate huffman trees
+(defun huffman-leaf-listp (x)
+ (declare (xargs :guard t))
+ (if (atom x)
+ (null x)
+ (and (huffman-treep (car x))
+ (not (nodep (car x)))
+ (huffman-leaf-listp (cdr x)))))
+
+(defun huffman-tree-listp (x)
+ (declare (xargs :guard t))
+ (if (atom x)
+ (null x)
+ (and (huffman-treep (car x))
+ (huffman-tree-listp (cdr x)))))
+
+(defun orderdp (x)
+ (declare (xargs :guard (huffman-tree-listp x)))
+ (cond ((atom x) t)
+ ((<= (weight (car x)) (weight (car x)))
+ (orderdp (cdr x)))
+ (t nil)))
+
+
+(defun symbol-weight-pair-listp (x)
+ (declare (xargs :guard t))
+ (if (atom x)
+ (null x)
+ (and (consp (car x))
+ (consp (cdar x))
+ (rationalp (cadar x))
+ (null (cddar x))
+ (symbol-weight-pair-listp (cdr x)))))
+
+
+(defun insert (e x)
+ (declare (xargs :guard (and (huffman-treep e)
+ (huffman-tree-listp x))))
+ (cond ((endp x) (list e))
+ ((<= (weight e) (weight (car x)))
+ (cons e x))
+ (t
+ (cons (car x)
+ (insert e (cdr x))))))
+
+(defun generate (x a)
+ (declare (xargs :measure (len x)
+ :guard (and (huffman-tree-listp x)
+ (orderdp x)
+ (huffman-treep a))))
+ (cond ((endp x) a)
+ ((<= (weight a) (weight (car x)))
+ (generate (cdr x) (huffman-node a (car x))))
+ ((endp (cdr x))
+ (huffman-node (car x) a))
+ ((<= (weight a) (weight (cadr x)))
+ (generate (cdr x)
+ (huffman-node (car x) a)))
+ (t
+ (generate (insert a (cddr x))
+ (huffman-node (car x) (cadr x))))))
+
+(defun pairs-to-leaves (x)
+ (declare (xargs :guard (symbol-weight-pair-listp x)))
+ (if (endp x)
+ nil
+ (insert (huffman-leaf (caar x) (cadar x))
+ (pairs-to-leaves (cdr x)))))
+
+(defun generate-huffman-tree (x)
+ (declare (xargs :guard (and (symbol-weight-pair-listp x)
+ (< 1 (len x)))
+ :verify-guards nil))
+ (let ((leaves (pairs-to-leaves x)))
+ (generate (cdr leaves) (car leaves))))
+
+(defun count-and-remove (e x)
+ (declare (xargs :guard (true-listp x)))
+ (cond ((endp x) (mv 0 nil))
+ ((equal e (car x))
+ (mv-let (c rest)
+ (count-and-remove e (cdr x))
+ (mv (+ 1 c) rest)))
+ (t
+ (mv-let (c rest)
+ (count-and-remove e (cdr x))
+ (mv c (cons (car x) rest))))))
+
+
+(defun message-to-pairs (x)
+ (declare (xargs :guard (true-listp x)))
+ (if (endp x)
+ nil
+ (mv-let (c rest)
+ (count-and-remove (car x) x)
+ (cons (list (car x) c)
+ (message-to-pairs rest)))))
+
+
+;;; Huffman encode/decode.
+(defun encode-1 (x tree)
+ (declare (xargs :guard (huffman-treep tree)
+ :measure (node-count tree)))
+ (if (nodep tree)
+ (cond ((member-equal x (symbol-list (left tree)))
+ (cons 0 (encode-1 x (left tree))))
+ (t
+ (cons 1 (encode-1 x (right tree)))))
+ nil))
+
+(defun encode (x tree)
+ (declare (xargs :guard (and (true-listp x)
+ (nodep tree)
+ (huffman-treep tree))))
+ (if (endp x)
+ nil
+ (append (encode-1 (car x) tree)
+ (encode (cdr x) tree))))
+
+
+(defun bit-listp (x)
+ (declare (xargs :guard t))
+ (if (atom x)
+ (null x)
+ (and (bitp (car x))
+ (bit-listp (cdr x)))))
+
+(defun decode-1 (x tree)
+ (declare (xargs :guard (and (bit-listp x)
+ (huffman-treep tree))
+ :measure (node-count tree)))
+ (cond ((and (consp x) (nodep tree))
+ (if (equal (car x) 0)
+ (decode-1 (cdr x) (left tree))
+ (decode-1 (cdr x) (right tree))))
+ ((nodep tree) (mv nil nil))
+ (t
+ (mv (leaf-symbol tree) x))))
+
+(defun decode (x tree)
+ (declare (xargs :measure (len x)
+ :guard (and (bit-listp x)
+ (nodep tree)
+ (huffman-treep tree))))
+ (if (or (endp x)
+ (not (nodep tree)))
+ nil
+ (mv-let (symbol rest)
+ (decode-1 x tree)
+ (cons symbol (decode rest tree)))))
+
+
+;;; --- defthm: pairs ---
+
+(defthm rationalp-0-count-and-remove
+ (rationalp (car (count-and-remove e x))))
+
+(defthm symbol-weight-pair-listp-message-to-pairs
+ (symbol-weight-pair-listp (message-to-pairs x)))
+
+;; --- insert - generate
+
+(defthm huffman-tree-listp-insert
+ (implies (and (huffman-tree-listp x)
+ (huffman-treep e))
+ (huffman-tree-listp (insert e x))))
+
+(defthm orderdp-insert
+ (implies (orderdp x)
+ (orderdp (insert e x))))
+
+(defthm huffman-tree-listp-pairs-to-leaves
+ (implies (symbol-weight-pair-listp x)
+ (huffman-tree-listp (pairs-to-leaves x))))
+
+(defthm orderdp-pairs-to-leaves
+ (orderdp (pairs-to-leaves x)))
+
+(defthm huffman-treep-generate
+ (implies (and (huffman-treep a)
+ (huffman-tree-listp x)
+ (consp x))
+ (huffman-treep (generate x a))))
+
+(defthm nodep-generate
+ (implies (and (huffman-treep a)
+ (huffman-tree-listp x)
+ (consp x))
+ (nodep (generate x a))))
+
+(defthm huffman-tree-listp-cdr
+ (implies (huffman-tree-listp x)
+ (huffman-tree-listp (cdr x))))
+
+(verify-guards generate-huffman-tree)
+
+(defthm huffman-treep-car
+ (implies (and (consp x) (huffman-tree-listp x))
+ (huffman-treep (car x))))
+
+(defthm len>1-consp
+ (equal (< 1 (len x))
+ (and (consp x)
+ (consp (cdr x)))))
+
+(defthm nodep-generate-huffman-tree
+ (implies (and (symbol-weight-pair-listp x)
+ (< 1 (len x)))
+ (nodep (generate-huffman-tree x))))
+
+(defthm huffman-treep-generate-huffman-tree
+ (implies (and (symbol-weight-pair-listp x)
+ (< 1 (len x)))
+ (huffman-treep (generate-huffman-tree x))))
+
+;;; ----- decode-encode
+(defthm bit-listp-encode-1
+ (bit-listp (encode-1 x tree)))
+
+(defthm bit-listp-encode
+ (bit-listp (encode x tree)))
+
+(defthm consp-append
+ (equal (consp (append x y))
+ (or (consp x)
+ (consp y))))
+
+(defthm consp-encode-1
+ (implies (and (member-equal x (symbol-list tree))
+ (huffman-treep tree)
+ (nodep tree))
+ (consp (encode-1 x tree))))
+
+(defthm consp-encode
+ (implies (and (consp x)
+ (true-listp x)
+ (huffman-treep tree)
+ (nodep tree)
+ (subsetp x (symbol-list tree)))
+ (consp (encode x tree))))
+
+
+(defthm len-decode-1
+ (implies (and (consp x)
+ (nodep tree))
+ (< (len (mv-nth 1 (decode-1 x tree)))
+ (len x))))
+
+(defthm member-append
+ (iff (member-equal e (append x y))
+ (or (member-equal e x)
+ (member-equal e y))))
+
+(defthm decode-1-encode-1
+ (implies (and (huffman-treep tree)
+ (member-equal x (symbol-list tree)))
+ (and (equal (mv-nth 0 (decode-1 (encode-1 x tree) tree))
+ x)
+ (equal (mv-nth 1 (decode-1 (encode-1 x tree) tree))
+ nil))))
+
+(defthm decode1-append
+ (implies (and (huffman-treep tree)
+ (member-equal x (symbol-list tree)))
+ (and (equal (mv-nth 0 (decode-1 (append (encode-1 x tree)
+ y)
+ tree))
+ x)
+ (equal (mv-nth 1 (decode-1 (append (encode-1 x tree)
+ y)
+ tree))
+ y))))
+
+(defthm decode-encode-to-decode1-encode1
+ (implies (and (huffman-treep tree)
+ (nodep tree)
+ (member-equal x (symbol-list tree))
+ (subsetp y (symbol-list tree)))
+ (equal (decode (append (encode-1 x tree)
+ (encode y tree))
+ tree)
+ (cons (mv-nth 0 (decode-1 (encode-1 x tree) tree))
+ (decode (encode y tree)
+ tree))))
+ :hints (("Goal" :induct (decode x tree))))
+
+(defthm decode-encode
+ (implies (and (true-listp x)
+ (huffman-treep tree)
+ (nodep tree)
+ (subsetp x (symbol-list tree)))
+ (equal (decode (encode x tree)
+ tree)
+ x)))