; This exercise is a re-working of the distributed book:
; books/sorting/convert-perm-to-how-many.lisp
; See convert-perm-to-how-many.lisp in the present directory for a cleaned-up
; version of the events below.
(in-package "ACL2")
(include-book "sorting/perm" :dir :system)
(defun how-many (e x)
(cond
((endp x) ; or, (atom x)
0)
((equal e (car x))
(1+ (how-many e (cdr x))))
(t
(how-many e (cdr x)))))
; We aim to prove that (perm x y) is the same as checking that for all e,
; (how-many e x) is (how-many e y). We can do that by defining the function
; (perm-counter-example x y) -- the counterexample generator -- that attempts
; to find an e that occurs a different number of times in x than in y.
; Thus, the following definition is modeled after the definition of perm.
(defun perm-counter-example (x y)
(cond ((atom x)
(car y))
((not (memb (car x) y))
(car x))
(t (perm-counter-example (cdr x) (rm (car x) y)))))
; Goal:
#||
(defthm convert-perm-to-how-many
(equal (perm x y)
(equal (how-many (perm-counter-example x y) x)
(how-many (perm-counter-example x y) y))))
||#
; This seems difficult, so we'll split it into two. If you skip-proofs the
; -forward and -backward lemmas just below, you'll see that the above proves
; with :hints
; (("Goal"
; :use
; ((:instance
; convert-perm-to-how-many-forward
; (a (perm-counter-example x y)))
; convert-perm-to-how-many-backward)))
(defthm convert-perm-to-how-many-forward
(implies (perm x y)
(equal (how-many a x)
(how-many a y)))
:rule-classes nil)
; The following takes some work:
#||
(defthm convert-perm-to-how-many-backward
(implies (equal (how-many (perm-counter-example x y) x)
(how-many (perm-counter-example x y) y))
(perm x y))
:rule-classes nil)
||#
; The first checkpoint after induction:
#||
Subgoal *1/3'
(IMPLIES (AND (CONSP X) (NOT (MEMB (CAR X) Y)))
(NOT (EQUAL (HOW-MANY (CAR X) X)
(HOW-MANY (CAR X) Y))))
||#
; So we prove:
(defthm not-memb-implies-how-many-is-0
(implies (not (memb a x))
(equal (how-many a x) 0)))
; We try convert-perm-to-how-many-backward again, and now there are only two
; checkpoints after induction. The first of those is:
#||
Subgoal *1/1.2'
(IMPLIES (AND (CONSP X)
(MEMB (CAR X) Y)
(NOT (EQUAL (HOW-MANY (CAR X) (CDR X))
(HOW-MANY (CAR X) (RM (CAR X) Y))))
(EQUAL (PERM-COUNTER-EXAMPLE (CDR X)
(RM (CAR X) Y))
(CAR X))
(EQUAL (+ 1 (HOW-MANY (CAR X) (CDR X)))
(HOW-MANY (CAR X) Y)))
(PERM (CDR X) (RM (CAR X) Y)))
||#
; The second and third hypotheses together suggest the following nice rewrite
; rule.
(defthm how-many-rm
(equal (how-many a (rm b x))
(if (and (equal a b)
(memb a x))
(1- (how-many a x))
(how-many a x))))
; Success!
(defthm convert-perm-to-how-many-backward
(implies (equal (how-many (perm-counter-example x y) x)
(how-many (perm-counter-example x y) y))
(perm x y))
:rule-classes nil)
; Now we're done:
(defthm convert-perm-to-how-many
(equal (perm x y)
(equal (how-many (perm-counter-example x y) x)
(how-many (perm-counter-example x y) y)))
:hints
(("Goal"
:use
((:instance
convert-perm-to-how-many-forward
(a (perm-counter-example x y)))
convert-perm-to-how-many-backward))))