Lecture Notes, Week 06

• Structuring programs, structuring proofs
  • A theorem for the main function, auxiliary lemmas for auxiliary functions
  • Eureka lemmas
  • Executive summary
  • Help! My recursive function doesn’t espouse my inductive data type!
  • Resources
  • Version
• About unfolding calls
  • Version
• Two more goodies to go
  • The eqn keyword
  • The remember tactic
  • Resources
  • Version
• Lambda-lifting and lambda-dropping
  • Lambda-lifted programs and lambda-lifted proofs
  • Lambda-dropped programs and lambda-dropped proofs
  • Conclusion
  • Resources
  • Version
• Induction and induction proofs: a recapitulation
  • Resources
  • The unit value
  • Booleans
  • Peano numbers
  • Binary trees with payloads in the leaves
  • Binary trees with payloads in the nodes
  • Variadic trees
  • Lists
  • Aftermath
  • Postlude
  • Exercise 01
  • Solution for Exercise 01
  • Exercise 02
  • And if there is only one summand
  • And if there are no summands
  • Resources
  • Version
• Mystery functions
  • Credits
  • Resources
  • Mystery functions
  • A mystery function that is unique
  • A mystery function that is not so mysterious
  • Resources
  • Version
• Tidbits, and some advice to boot
  • On uniformity and unity
  • Food for thought
  • Regarding induction hypotheses
  • Bits of advice
  • Regarding self reference
  • Version
• Exercises for Week 06
  • Exercise 00
  • Mandatory exercises
  • Optional exercises
  • Version
• Index of concepts for Week 06
  • Version