PeterReid
commented
12 years ago This is the code that's making it hang, by the way.
(include-book "data-structures/structures" :dir :system)
(defstructure bst left key right)
(defun key< (x y)
(< x y))
(in-theory (disable key<))
(defun key? (x)
(natp x))
(in-theory (disable key?))
(defthm key-<-or->
(implies (and (key? x)
(key? y)
(not (equal x y))
(not (key< x y)))
(key< y x))
:hints (("Goal" :in-theory (enable key? key<))))
(defun bst-keys-below (x tr)
(if (bst-p tr)
(and (key< (bst-key tr) x)
(bst-keys-below x (bst-left tr))
(bst-keys-below x (bst-right tr)))
t))
(defun bst-keys-above (x tr)
(if (bst-p tr)
(and (key< x (bst-key tr))
(bst-keys-above x (bst-left tr))
(bst-keys-above x (bst-right tr)))
t))
(defun bst? (tr)
(or (null tr)
(and (bst-p tr)
(key? (bst-key tr))
(bst-keys-below (bst-key tr) (bst-left tr))
(bst-keys-above (bst-key tr) (bst-right tr))
(bst? (bst-left tr))
(bst? (bst-right tr)))))
(defun bst-empty? (x)
(null x))
(defun empty-bst ()
nil)
(defthm left-<
(implies (bst-p tr)
(< (acl2-count (bst-left tr))
(acl2-count tr)))
:hints (("Goal" :in-theory (enable bst-left bst-p weak-bst-p))))
(defthm right-<
(implies (bst-p tr)
(< (acl2-count (bst-right tr))
(acl2-count tr)))
:hints (("Goal" :in-theory (enable bst-right bst-p weak-bst-p))))
(defun bst-insert (x tr)
(if (bst-p tr)
(cond ((key< x (bst-key tr))
(bst (bst-insert x (bst-left tr))
(bst-key tr)
(bst-right tr)))
((key< (bst-key tr) x)
(bst (bst-left tr)
(bst-key tr)
(bst-insert x (bst-right tr))))
(t tr))
(bst (empty-bst) x (empty-bst))))
(defthm left-<-root
(implies (bst-left tr)
(< (acl2-count (bst-left tr))
(acl2-count tr)))
:hints (("Goal"
:in-theory (enable bst-left))))
(defthm right-<-root
(implies (bst-right tr)
(< (acl2-count (bst-right tr))
(acl2-count tr)))
:hints (("Goal"
:in-theory (enable bst-right))))
(defun bst-first (tr)
(if (bst-empty? (bst-left tr))
(bst-key tr)
(bst-first (bst-left tr))))
(defun bst-remove-first (tr)
(if (bst-empty? (bst-left tr))
(bst-right tr)
(bst (bst-remove-first (bst-left tr))
(bst-key tr)
(bst-right tr))))
(defun bst-delete (x tr)
(if (bst-p tr)
(cond ((key< x (bst-key tr))
(bst (bst-delete x (bst-left tr))
(bst-key tr)
(bst-right tr)))
((key< (bst-key tr) x)
(bst (bst-left tr)
(bst-key tr)
(bst-delete x (bst-right tr))))
((equal (bst-key tr) x)
(if (bst-empty? (bst-right tr))
(bst-left tr)
(bst (bst-left tr)
(bst-first (bst-right tr))
(bst-remove-first (bst-right tr))))
))
(empty-bst)))
(defun bst-contains (x tr)
(and (bst-p tr)
(cond ((key< x (bst-key tr))
(bst-contains x (bst-left tr)))
((key< (bst-key tr) x)
(bst-contains x (bst-right tr)))
(t
(equal (bst-key tr) x)))))
(defthm not-x-key<-x
(implies (key? x)
(not (key< x x)))
:hints (("Goal" :in-theory (enable key? key<))))
(defthm contains-after-insert
(implies (and (bst? tr)
(key? x))
(bst-contains x (bst-insert x tr)))
:hints (("Goal"
:use (:instance key-<-or-> (x x) (y (bst-key tr))))))
(defthm bst-keys-below-after-insert
(implies (and (bst? tr)
(key? x)
(key? top)
(bst-keys-below top tr)
(key< x top))
(bst-keys-below top (bst-insert x tr))))
(defthm bst-keys-above-after-insert
(implies (and (bst? tr)
(key? x)
(key? bottom)
(bst-keys-above bottom tr)
(key< bottom x))
(bst-keys-above bottom (bst-insert x tr))))
(defthm bst-after-insert
(implies (and (bst? tr)
(key? x))
(bst? (bst-insert x tr))))
(defthm still-contains-after-insert
(implies (and (bst? tr)
(key? x)
(key? y)
(bst-contains y tr))
(bst-contains y (bst-insert x tr))))
(defthm not-contains-if-keys-above
(implies (and (bst? tr)
(key? x)
(bst-keys-below x tr))
(not (bst-contains x tr))))
(defthm not-contains-if-keys-below
(implies (and (bst? tr)
(key? x)
(bst-keys-above x tr))
(not (bst-contains x tr))))
(defthm not-<-and->
(implies (and (key? x)
(key? y)
(key< x y))
(not (key< y x)))
:hints (("Goal" :in-theory (enable key? key<))))
;(defthm bst-p-if-exists
; (implies (and (bst? tr)
; (bst-left (bst-left tr)))
; (bst-p (bst-left (bst-left tr)))))
(defthm key-<-transitive
(implies (and (key? x) (key? y) (key? z)
(key< x y) (key< y z))
(key< x z))
:hints (("Goal" :in-theory (enable key< key?))))
(defthm bst-first-is-key
(implies (and (bst? tr)
(bst-p tr))
(key? (bst-first tr))))
(defthm bst-first-<-root
(implies (and (bst? tr)
(bst-p (bst-left tr)))
(key< (bst-first tr)
(bst-key tr)))
:hints (("Subgoal *1/2"
:use (:instance key-<-transitive
(x (bst-first (bst-left tr)))
(y (bst-key (bst-left tr)))
(z (bst-key tr))))))
#|(defthm bst-root-not-<-bst-first
(implies (and (bst? tr)
(bst-p tr))
(not (key< (bst-key tr)
(bst-first tr))))
:hints (("Goal"
:in-theory (disable key-<-transitive)
:use (:instance key-<-transitive
(x (bst-first (bst-left tr)))
(y (bst-key (bst-left tr)))
(z (bst-key tr))))))
(defthm contains-first
(implies (and (bst-p tr)
(bst? tr))
(bst-contains (bst-first tr) tr))
:hints (("Subgoal *1/4"
:use ((:instance key-<-transitive
(x (bst-first (bst-left tr)))
(y (bst-key (bst-left tr)))
(z (bst-key tr)))
(:instance bst-first-is-key
(tr (bst-left tr))
)
(:instance bst-first-<-root
(tr (bst-left tr)))))
("Subgoal *1/6"
:use ((:instance key-<-transitive
(x (bst-first (bst-left tr)))
(y (bst-key (bst-left tr)))
(z (bst-key tr)))))))
|#
(defaxiom contains-first
(implies (and (bst-p tr)
(bst? tr))
(bst-contains (bst-first tr) tr)))#|ACL2s-ToDo-Line|#
(defthm still-not-contains-after-remove-first
(implies (and (bst? tr)
(key? x)
)
(equal (bst-contains x (bst-remove-first tr))
(and (not (equal x (bst-first tr)))
(bst-contains x tr)))))
(defthm gone-after-delete
(implies (and (bst? tr)
(key? x))
(not (bst-contains x (bst-delete x tr)))))
calebegg
I opened a file that contains lots of proofs, some of which don't admit (and instead cause the theorem prover to just spin and spin). The proof pad UI hangs because
I think it would make sense to change admit so that the worker thread does the flushing as well as the reading-back. That way, the prover might work indefinitely, but the UI will not hang.