Lecture Notes, Week 04

• Warmup
  • Currying and uncurrying are inverses of each other
  • Curried functions
  • Curried propositions
  • The Coq Proof Assistant in essence
  • A logical question and a pragmatic answer
  • 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
  • Exercise 01
  • 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
  • Rewriting in all the assumptions
  • Rewriting both in the goal and in all the assumptions
  • By default
  • Rewriting over fully applied lemmas
  • Postlude
  • Resources
  • Version
• Structural induction over Peano numbers
  • Resources
  • Peano numbers
  • The induction tactic
  • Proving that 0 is absorbing for multiplication on the right
  • Revisiting the first puzzle from Week 01
  • Exercise 02
  • Exercise 03
  • Resources
  • Version
• The exists tactic
  • Resources
  • Version
• Specifications
  • Resources
  • Properties of specifications
  • There is at most one recursive addition function
  • Interlude
  • Exercise 04
  • An ambiguous specification
  • Exercise 05
  • Interlude: Solution for Exercise 05
  • A vacuous specification
  • Exercise 06
  • A vacuous specification (continued and ended)
  • About proving that an implementation satisfies a specification
  • Exercise 07
  • Exercise 08
  • Exercise 09
  • Exercise 10
  • Partial solution for Exercise 10
  • Exercise 11
  • 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 12
  • Mirroring a tree is involutory
  • Exercise 13
  • Relation between the number of leaves and of the number of nodes of any given binary tree
  • Postlude
  • Resources
  • Version
• Exercises for Week 04
  • Exercise 00
  • Mandatory exercises
  • Optional exercises
  • Exercise for the overachievers (which means you, I mean, like, right, you right here you)
  • Exercise about ternary trees
  • Resources
  • Version
• Index of concepts for Week 04
  • Version