---

4.7 Homework 6

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

                       Given:  October 12, 2021
                        Due:   October 26, 2021

PART 1:

In addition to working some problems from the course notes (see below), please prepare a one-slide talk and one-page proposal for your course project. You should be ready to present your proposal by Tuesday, October 19.

When called on in class, be prepared to present your idea using ONE slide only. Practice your presentation – you need to be able to present your idea in three minutes. This will be followed by 2 minutes for Q&A.

EXTRA CREDIT OPPORTUNITY:

NOTE: You may resubmit one problem from Homework #5 with your Homework #6 submission for 1/2 of the scored credit. Thus, if you didn’t submit a problem or didn’t finish it, then you may resubmit one problem.

PART 2:

The balance of this homework assignment is based on the material from Moore’s Recursion and Induction notes. Please read through section 13 before attempting to do the homework.

Your homework assignment is to provide solutions for problems 65-67 and 71-74.

Please do the proofs for 71 and 72 by hand. Also turn in ACL2 proof builder scripts for 71-74. 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 TA by the beginning of class on the due date. The solutions should be attached as a file named “hw6-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 "hw6-firstname-lastname.lisp").

In other words, all definitions related to the problems 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