Recursion and Induction, Nov. 1, 2011

• Problem statement: simple-demo-challenge.lisp
• Problem solution: simple-demo-solution.lisp

• Problem statement: rotate-challenge.lisp
• Problem solution: rotate-solution.lisp
• Alternate problem solution: rotate-alt.lisp

Main points made today:

• Sometimes you can take a low-level tactical approach, focusing on the key checkpoints printed at the end of the proof -- either pre-induction, if you don't expect induction to be needed, else post-induction.
• Sometimes, as in the rotate example, you need to think of some high-level strategy, as is typical in mathematical proofs.
• Rewriting is a key proof technique in ACL2. We spent a little time on it, including the notion of formulating rewrite rules that can replace an expression by a "simpler" expression.

Other important points discussed today

• Feel free to join the acl2-help email list and look at documentation, both easily accessible from the ACL2 home page
• Don't take on too ambitious a project.
• More examples are available under the ACL2-TUTORIAL documentation topic, and in particular its subtopic, ANNOTATED-ACL2-SCRIPTS, where you can find a challenge problem (with separate file of solutions) from the TPHOLs08 conference.