I was thinking about the many... Areas that needed expansion in my HPR
episode.
Anyway, it's cool that we had sh and a Makefile for asdf3 projects
that could be certified acl2 books. But it was ambiguous why we might
do that, I have made a better trivial example here.
The triviality is a challenge and deliberate.
|#
(in-package "ACL2-USER")
;;;; Let's make a "maze" of sublists, but there's only one direction.
;;;; The sublists will have car 0, except for the last one.
;;;; We will have two thms about tips found exploring the maze.
(defun make-simple-cons-tree (n tree)"
> (make-simple-cons-tree 3 nil)
((0) (0) (1)) ; our maze
"
(if (zp n) (reverse tree) ; we fill it the wrong way
(make-simple-cons-tree (1- n)
(cons (list (if (= 1 n) 1 0)) tree))))
#|
That is pretty close to enough of an idea of graph search
(well we might like graphs that aren't linear and directional)
acl2 can now trivially prove specific cases:
|#
(thm ; 4 steps won't collect '1 (at the fifth position)
(implies
(and (equal tree-len 5)
(equal no-steps 4)
(equal tree (make-simple-cons-tree tree-len nil))
(equal alist (list (cons 'tree tree)))
(equal new-alist (take-n-steps no-steps alist))
(equal new-tips (cdr (assoc 'collected-tips new-alist))))
(not (member 1 new-tips))))
;; Remembering (1) was in the fifth position of tree.
;;;; But if there are enough steps, 1 is in the collected-tips
(thm ; 5 steps will collect '1 (at the fifth position)
(implies
(and (equal tree-len 5)
(equal no-steps 5)
(equal tree (make-simple-cons-tree tree-len nil))
(equal alist (list (cons 'tree tree)))
(equal new-alist (take-n-steps no-steps alist))
(equal new-tips (cdr (assoc 'collected-tips new-alist))))
(member 1 new-tips)))
#|
This is the first step of ACL2's The Method.
Of course acl2 can prove this - it can just do the specific case of
admitted (well-defined, total) functions and check if it's true.
With (1) at fifth position and (0) otherwise,
4 steps proven to not-be-enough, 5 steps proven to be enough
The next step is to make tree-len a free variable (and (natp
tree-len)) And define no-steps relative to tree-len (< no-steps
tree-len) (natp no-steps) (should also (imply (not (member 1
new-tips)))) If we make that change, acl2 finds a failure after a few
thousand steps. It needs defuns, defthms and maybe :hints from us
about how to induct upon tree-len, no-steps and new-tips.
defthms generally make rewrite rules- after proving the theorem once,
when acl2 realises it's in the pre-condition for a theorem it knows,
it substitutes the precondition (first clause of 'implies) for the
hopefully simpler known result.
|#