diff options
Diffstat (limited to 'expr.tex')
| -rw-r--r-- | expr.tex | 7 |
1 files changed, 3 insertions, 4 deletions
@@ -127,7 +127,6 @@ Since the program is reversed for use in \textsf{pn\_eval}, we can rewrite the p Suppose the original expression was \textsf{e = eadd e1 e2}, we now consider \textsf{pn\_eval v env ((rev (rpn v e1) ++ rev (rpn v e2)) ++ rest)} in the evaluation of \textsf{rpnadd}. - Due to associativity of \textsf{++}, we can reanalyse this as \textsf{pn\_eval v env (rev (rpn v e1) ++ (rev (rpn v e2) ++ rest))}, which allows for application of the induction hypothesis with \textsf{rev (rpn v e2) ++ rest} as the \enquote{rest of the program}, i.e., the \textsf{rest}. @@ -146,13 +145,13 @@ The proof of the lemma now follows by applying the assertion of the induction st \coq{83}{85} -We now return to the proof of the correctness theorem, repeated here: +We now return to the proof of the correctness theorem: -\coq{87}{88} +\coq{87}{89} We outsource this proof to our proof on \textsf{pn\_eval} using \textsf{rest = result = []}. -\coq{89}{93} +\coq{90}{93} The result of the call to \textsf{pn\_eval} from \textsf{rpn\_eval} is now known, and we can simplify the \textsf{rpn\_eval} call further to the point of reflexivity. |