Lecture Notes, Week 03

• Warmup
  • Currying and uncurrying are inverses of each other
  • Resources
  • Version
• The rewrite tactic
  • Resources
  • Rewriting from left to right in the current goal
  • Rewriting a specific occurrence from left to right in the current goal
  • Rewriting from left to right in an assumption
  • Rewriting a specific occurrence from left to right in an assumption
  • Rewriting from right to left
  • Rewriting left and right
  • By default
  • Rewriting over fully applied lemmas
  • Postlude
  • Resources
  • Version
• Structural induction over Peano numbers
  • Resources
  • Peano numbers
  • The induction tactic
  • Resources
  • Version
• The exists tactic
  • Resources
  • Version
• Specifications
  • Resources
  • Properties of specifications
  • There is at most one recursive addition function
  • Interlude
  • Exercise 01
  • Solution for Exercise 01
  • An ambiguous specification
  • Exercise 02
  • Interlude: Solution for Exercise 02
  • A vacuous specification
  • Exercise 03
  • A vacuous specification (continued and ended)
  • About proving that an implementation satisfies a specification
  • Exercise 04
  • Exercise 05
  • Exercise 06
  • Exercise 07
  • Partial solution for Exercise 07
  • Exercise 08
  • Halcyon’s dream
  • Postlude
  • Executive summary
  • Resources
  • Version
• Structural induction over binary trees
  • Resources
  • Polymorphic binary trees with payloads in the leaves
  • Interlude
  • Three specifications
  • Exercise 09
  • Mirroring a tree is involutory
  • Exercise 10
  • Relation between the number of leaves and of the number of nodes of any given binary tree
  • Postlude
  • Resources
  • Version
• Exercises for Week 03
  • Exercise 00
  • Mandatory exercises
  • Optional exercises
  • Version
• Index of concepts for Week 03
  • Version