; This exercise is a re-working of the distributed book:
; books/sorting/ordered-perms.lisp
(in-package "ACL2")
(include-book "sorting/perm" :dir :system)
(defun orderedp (x)
(if (endp x)
t
(if (endp (cdr x))
t
(and (lexorder (car x) (car (cdr x)))
(orderedp (cdr x))))))
#|| Goal:
(defthm ordered-perms
(implies (and (true-listp a)
(true-listp b)
(orderedp a)
(orderedp b))
(equal (equal a b)
(perm a b)))
:rule-classes nil)
||#
; The first checkpoint after induction looks difficult, so let's start with the
; second.
(defthm rm-preserves-orderedp
(implies (orderedp x)
(orderedp (rm a x))))
; The first checkpoint after induction still looks difficult, so let's start
; with the other that remains.
(defthm rm-preserves-true-listp
(implies (true-listp x)
(true-listp (rm a x))))
; We can better understand the term (EQUAL (CDR A) (RM (CAR A) B)) from the
; remaining checkpoing if we expand the RM call, so as to break into the cases
; that (CAR A) is or is not (CAR B). So we provide this for ordered-perms:
; :hints (("Goal" :expand ((rm (car a) b))))
; The resulting checkpoint is:
#||
(IMPLIES (AND (CONSP A)
(CONSP (CDR A))
(LEXORDER (CAR A) (CADR A))
(CONSP B)
(NOT (EQUAL (CAR A) (CAR B)))
(EQUAL (CDR A)
(CONS (CAR B) (RM (CAR A) (CDR B))))
(TRUE-LISTP (CDR A))
(TRUE-LISTP (CDR B))
(ORDEREDP (CDR A))
(LEXORDER (CAR B) (CADR B))
(ORDEREDP (CDR B)))
(NOT (MEMB (CAR A) (CDR B))))
||#
; So we prove the following, thinking of a as (CAR A) and x as (CDR B).
; Let's make it local, since it seems like too specialized a lemma to be worthy
; of exporting.
(local
(defthm lexorder-car-implies-not-memb
(implies (and (lexorder a (car x))
(orderedp x)
(not (equal a (car x))))
(not (memb a x)))))
; Now we're done, even without the :expand hint. Note the defthmd rather than
; defthm -- usually we'll keep this disabled so that we don't consider
; rewriting every equality!
(defthmd ordered-perms
(implies (and (true-listp a)
(true-listp b)
(orderedp a)
(orderedp b))
(equal (equal a b)
(perm a b))))