---

4.6 Homework 5: The Proof Builder

                        Homework Assignment 5
                               CS 389r
                         Unique Number: 53119
                             Fall, 2021

                       Given:  October  5, 2021
                        Due:   October 14, 2021

This homework assignment is based on the material from Moore’s Recursion and Induction notes. Please read through section 11 before attempting to do the homework. Starting with this problem set, you will make use of the ACL2 proof builder. https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____PROOF-BUILDER

Your homework assignment is to provide solutions for problems 52 – 54, 56 – 58, 61.

Please do all of these problems by hand, but also turn in two of these proofs using the ACL2 proof builder and its ability to output the instructions used to demonstrate your proof.

The solutions produced using the proof builder must be submitted electronically as an ACL2 DEFTHM event that can be processed by the ACL2 system. We will show how to use the ACL2 proof builder in class to produce such a log.

Email your proof builder solutions to the class teaching assistant by the beginning of class on the due date. The solutions should be attached as a file named “hw5-firstname-lastname.lisp” where firstname and lastname are your first and last name. The file should execute from start to finish in ACL2. You can test this by starting ACL2 and executing the command (ld “hw5-firstname-lastname.lisp”). In other words, all definitions related to the two problems you selected should be included in the file. We will inspect your definitions and your theorems with proof builder instructions in addition to executing the file.

When you use the proof builder, limit your use of the ACL2 proof builder commands to those listed below:

[ACL2-pc::=]
     (atomic macro) attempt an equality (or equivalence) substitution

[ACL2-pc::bk]
    (atomic macro) move backward one argument in the enclosing term

[ACL2-pc::casesplit]
    (primitive) split into two cases

[ACL2-pc::cg]
    (macro) change to another goal.

[ACL2-pc::change-goal]
    (primitive) change to another goal.

[ACL2-pc::comm]
    (macro) display instructions from the current interactive session

[ACL2-pc::commands]
    (macro) display instructions from the current interactive session

[ACL2-pc::comment]
    (primitive) insert a comment

[ACL2-pc::contradict]
    (macro) same as contrapose

[ACL2-pc::contrapose]
    (primitive) switch a hypothesis with the conclusion, negating both

[ACL2-pc::demote]
    (primitive) move top-level hypotheses to the conclusion

[ACL2-pc::dive]
    (primitive) move to the indicated subterm

[ACL2-pc::doc]
    (macro) access documentation inside the proof-checker

[ACL2-pc::drop]
    (primitive) drop top-level hypotheses

[ACL2-pc::dv]
    (atomic macro) move to the indicated subterm

[ACL2-pc::equiv]
    (primitive) attempt an equality (or congruence-based) substitution

[ACL2-pc::exit]
    (meta) exit the interactive proof-checker

[ACL2-pc::expand]
    (primitive) expand the current function call without simplification

[ACL2-pc::goals]
    (macro) list the names of goals on the stack

[ACL2-pc::help]
    (macro) proof-checker help facility

[ACL2-pc::hyps]
    (macro) print the hypotheses

[ACL2-pc::in-theory]
    (primitive) set the current proof-checker theory

[ACL2-pc::induct]
    (atomic macro) generate subgoals using induction

[ACL2-pc::nx]
   (atomic macro) move forward one argument in the enclosing term

[ACL2-pc::p]
    (macro) prettyprint the current term

[ACL2-pc::p-top]
    (macro) prettyprint the conclusion, highlighting the current term

[ACL2-pc::pp]
    (macro) prettyprint the current term

[ACL2-pc::print]
    (macro) print the result of evaluating the given form

[ACL2-pc::print-all-concs]
    (macro) print all the conclusions of (as yet unproved) goals

[ACL2-pc::print-all-goals]
    (macro) print all the (as yet unproved) goals

[ACL2-pc::print-main]
    (macro) print the original goal

[ACL2-pc::promote]
    (primitive) move antecedents of conclusion's implies term to
    top-level hypotheses

[ACL2-pc::r]
    (macro) same as rewrite

[ACL2-pc::restore]
    (meta) remove the effect of an UNDO command

[ACL2-pc::retrieve]
    (macro) re-enter the proof-checker

[ACL2-pc::rewrite]
    (primitive) apply a rewrite rule

[ACL2-pc::s]
    (primitive) simplify the current subterm

[ACL2-pc::s-prop]
    (atomic macro) simplify propositionally

[ACL2-pc::save]
    (macro) save the proof-checker state (state-stack)

[ACL2-pc::show-rewrites]
    (macro) display the applicable [rewrite] rules

[ACL2-pc::sl]
    (atomic macro) simplify with lemmas

[ACL2-pc::split]
    (atomic macro) split the current goal into cases

[ACL2-pc::sr]
    (macro) same as SHOW-REWRITES

[ACL2-pc::th]
    (macro) print the top-level hypotheses and the current subterm

[ACL2-pc::top]
    (atomic macro) move to the top of the goal

[ACL2-pc::undo]
    (meta) undo some instructions

[ACL2-pc::up]
    (primitive) move to the parent (or some ancestor) of the current
    subterm

[ACL2-pc::use]
    (atomic macro) use a lemma instance