#|

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))))

;;;;Move forward
(defun tree-step (tree) (cdr tree))

;;;;Get current tip
(defun collect-tip (tree) (caar tree))

;;;;Use       that      once      in      a       stateish       alist
(defun one-simple-step (alist) "
>     (one-simple-step     '((tree   (0)    (1))    (collected-tips)))
((tree (1)) (collected-tips 0))
"
(let ((tree  (cdr (assoc 'tree alist)))
      (tips (cdr (assoc 'collected-tips  alist))))
 (list (cons 'tree (tree-step  tree))
  (cons 'collected-tips (cons (collect-tip tree) tips)))))

(defun take-n-steps (n alist) "
> (take-n-steps 3
(list (cons 'tree (make-simple-cons-tree  5 nil))
 (cons 'collected-tips nil)))
((tree      (0)      (1))      (collected-tips       0      0      0))
"
 (if (zp n) alist
  (take-n-steps (1- n) (one-simple-step alist))))

#|
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. 
|#