;; A hint for Exam Question 4.
#| Here is a general theorem that the compiler behaves as expected.
It is sufficiently general so that it can be proved by induction on
the structure of expressions (with specialized instantiations of the
other variables such as stk, prog1, and prog2).
(thm
;;compile-is-correct-general
(implies (exprp exp)
(equal (run (modify nil
:pc (len prog1)
:locals alist
:stack stk
:program (append
prog1
(exp-compile exp)
prog2))
(nbr-of-steps exp))
(modify nil
:pc (+ (len prog1)
(len (exp-compile exp)))
:locals alist
:stack (push (exp-eval exp alist) stk)
:program (append prog1
(exp-compile exp)
prog2))))
:hints (("Goal"
:do-not generalize)))
----------------------------------------------------------------------
Here is ACL2's naive first attemp of proving the above thm by induction:
We will induct according to a scheme suggested by (EXP-EVAL EXP ALIST).
If we let (:P ALIST EXP PROG1 PROG2 STK) denote *1 above then the
induction scheme we'll use is
[Here is one case of the induction scheme.]
(IMPLIES (AND (EQUAL (LEN EXP) 2)
(EQUAL (CAR EXP) 'INC)
(:P ALIST (SECOND EXP) PROG1 PROG2 STK))
(:P ALIST EXP PROG1 PROG2 STK))
Subgoal *1/4
(IMPLIES
(AND (EQUAL (LEN EXP) 2)
(EQUAL (CAR EXP) 'INC)
(EQUAL (RUN (modify nil
:pc (LEN PROG1)
:locals ALIST
:stack STK
:program (APPEND PROG1
(EXP-COMPILE (SECOND EXP))
PROG2))
(NBR-OF-STEPS (SECOND EXP)))
(modify nil
:pc (+ (LEN PROG1)
(LEN (EXP-COMPILE (SECOND EXP))))
:locals ALIST
:stack (PUSH (EXP-EVAL (SECOND EXP) ALIST)
STK)
:program (APPEND PROG1
(EXP-COMPILE (SECOND EXP))
PROG2)))
(EXPRP EXP))
(EQUAL (RUN (modify nil
:pc (LEN PROG1)
:locals ALIST
:stack STK
:program (APPEND PROG1
(EXP-COMPILE EXP)
PROG2))
(NBR-OF-STEPS EXP))
(modify nil
:pc (+ (LEN PROG1)
(LEN (EXP-COMPILE EXP)))
:locals ALIST
:stack (PUSH (EXP-EVAL EXP ALIST) STK)
:program (APPEND PROG1
(EXP-COMPILE EXP)
PROG2))))
Using the definition of (EXP-COMPILE EXP) for the case when (CAR EXP) is 'INC:
(IMPLIES
(AND (EQUAL (LEN EXP) 2)
(EQUAL (CAR EXP) 'INC)
(EQUAL (RUN (modify nil
:pc (LEN PROG1)
:locals ALIST
:stack STK
:program (APPEND PROG1
(EXP-COMPILE (SECOND EXP))
PROG2))
(NBR-OF-STEPS (SECOND EXP)))
(modify nil
:pc (+ (LEN PROG1)
(LEN (EXP-COMPILE (SECOND EXP))))
:locals ALIST
:stack (PUSH (EXP-EVAL (SECOND EXP) ALIST)
STK)
:program (APPEND PROG1
(EXP-COMPILE (SECOND EXP))
PROG2)))
(EXPRP EXP))
(EQUAL (RUN (modify nil
:pc (LEN PROG1)
:locals ALIST
:stack STK
:program (APPEND PROG1
(EXP-COMPILE (SECOND EXP))
'((PUSH 1) (ADD))
PROG2))
(+ 2 (NBR-OF-STEPS (SECOND EXP))))
(modify nil
:pc (+ 2
(LEN PROG1)
(LEN (EXP-COMPILE (SECOND EXP))))
:locals ALIST
:stack (PUSH (EXP-EVAL EXP ALIST) STK)
:program (APPEND PROG1
(EXP-COMPILE (SECOND EXP))
'((PUSH 1) (ADD))
PROG2))))
-----------------------------------------------------------------------
One problem with proving the above term is that the :program in the
hypothesis is not the same as the :program in the conclusion.
We define a ``better'' induction scheme:
(defun
induct-hint (exp stk prog1 prog2)
(cond ((symbolp exp)
(list stk prog1 prog2))
((integerp exp)
(list stk prog1 prog2))
((equal (len exp) 2)
(let ((op (first exp)))
(cond ((equal op 'inc)
(induct-hint (second exp)
stk
prog1
(append '((PUSH 1)(ADD))
prog2)))
...)))))
We will induct according to a scheme suggested by
(INDUCT-HINT EXP STK PROG1 PROG2). If we let
(:P ALIST EXP PROG1 PROG2 STK) denote *1 above then the induction scheme
we'll use is
[Here is one case of the induction scheme.]
(IMPLIES (AND (EQUAL (LEN EXP) 2)
(EQUAL (CAR EXP) 'INC)
(:P ALIST
(SECOND EXP)
PROG1
(APPEND '((PUSH 1) (ADD)) PROG2)
STK))
(:P ALIST EXP PROG1 PROG2 STK))
Subgoal *1/3
(IMPLIES
(AND (EQUAL (LEN EXP) 2)
(EQUAL (CAR EXP) 'INC)
(IMPLIES (EXPRP (SECOND EXP))
(EQUAL (RUN (modify nil
:pc (LEN PROG1)
:locals ALIST
:stack STK
:program (APPEND PROG1
(EXP-COMPILE (CADR EXP))
'((PUSH 1) (ADD))
PROG2))
(NBR-OF-STEPS (SECOND EXP)))
(modify nil
:pc (+ (LEN PROG1)
(LEN (EXP-COMPILE (SECOND EXP))))
:locals ALIST
:stack (PUSH (EXP-EVAL (SECOND EXP) ALIST)
STK)
:program (APPEND PROG1
(EXP-COMPILE (SECOND EXP))
'((PUSH 1) (ADD))
PROG2)))))
(IMPLIES (EXPRP EXP)
(EQUAL (RUN (modify nil
:pc (LEN PROG1)
:locals ALIST
:stack STK
:program (APPEND PROG1
(EXP-COMPILE EXP)
PROG2))
(NBR-OF-STEPS EXP))
(modify nil
:pc (+ (LEN PROG1)
(LEN (EXP-COMPILE EXP)))
:locals ALIST
:stack (PUSH (EXP-EVAL EXP ALIST)
STK)
:program (APPEND PROG1
(EXP-COMPILE EXP)
PROG2)))))
Using the definition of (EXP-COMPILE EXP) for the case when (CAR EXP) is 'INC:
(IMPLIES
(AND (EQUAL (LEN EXP) 2)
(EQUAL (CAR EXP) 'INC)
(IMPLIES (EXPRP (SECOND EXP))
(EQUAL (RUN (modify nil
:pc (LEN PROG1)
:locals ALIST
:stack STK
:program (APPEND PROG1
(EXP-COMPILE (CADR EXP))
'((PUSH 1) (ADD))
PROG2))
(NBR-OF-STEPS (SECOND EXP)))
(modify nil
:pc (+ (LEN PROG1)
(LEN (EXP-COMPILE (SECOND EXP))))
:locals ALIST
:stack (PUSH (EXP-EVAL (SECOND EXP) ALIST)
STK)
:program (APPEND PROG1
(EXP-COMPILE (SECOND EXP))
'((PUSH 1) (ADD))
PROG2)))))
(IMPLIES (EXPRP EXP)
(EQUAL (RUN (modify nil
:pc (LEN PROG1)
:locals ALIST
:stack STK
:program (APPEND PROG1
(EXP-COMPILE (SECOND EXP))
'((PUSH 1) (ADD))
PROG2))
(+ 2
(NBR-OF-STEPS (SECOND EXP))))
(modify nil
:pc (+ 2
(LEN PROG1)
(LEN (EXP-COMPILE (SECOND EXP))))
:locals ALIST
:stack (PUSH (+ (EXP-EVAL (SECOND EXP) ALIST) 1)
STK)
:program (APPEND PROG1
(EXP-COMPILE (SECOND EXP))
'((PUSH 1) (ADD))
PROG2)))))
So at least the :program in the hypothesis is the same as the :program in
the conclusion.
|#