Lecture Notes, Week 05

• Three properties of the Leibniz equality
  • Reflexivity
  • Symmmetry
  • Transitivity
  • Resources
  • Version
• The clear tactic
  • A worked-out example
  • Resources
  • Version
• Specifications that depend on other specifications
  • Resources
  • The recursive specification of the addition function
  • A specification of the multiplication function
  • Proving that O is left-absorbing for multiplication
  • Interlude
  • Proving that 1 is left-neutral for multiplication
  • Exercise 01
  • Solution for Exercise 01
  • Exercise 02
  • Solution for Exercise 02
  • Exercise 03
  • Exercise 04
  • Exercise 05
  • Exercise 06
  • Solution for Exercise 06
  • Postlude
  • Resources
  • Version
• More about soundness and completeness
  • Resources
  • A Eureka lemma
  • Decomposing values using the injection tactic
  • False implies anything
  • Exercise 07
  • Soundness of recursive addition, revisited
  • Completeness of recursive addition, revisited
  • Proving properties as corollaries of other properties
  • Exercise 08
  • Resources
  • Version
• Proving the correctness of unit tests
  • Resources
  • A specification of the addition function
  • A unit-test function for addition
  • Correctness of the unit-test function
  • Computation, proof step after proof step
  • Exercise 09
  • From explicit to implicit proof steps to carry out a computation
  • Exercise 10
  • Resources
  • Version
• Backward and forward proofs
  • Resources
  • A backward proof
  • Exercise 11
  • Exercise 12
  • Exercise 13
  • Exercise 14
  • Exercise 15
  • Postlude
  • Resources
  • Version
• Reasoning equationally about recursive functions using fold-unfold lemmas
  • Resources
  • A concrete example
  • Exercise 16
  • Solution for Exercise 16
  • Exercise 17
  • Solution for Exercise 17
  • Exercise 18
  • Solution for Exercise 18
  • Exercise 19
  • Solution for Exercise 19
  • Exercise 20
  • Solution for Exercise 20
  • Exercise 21
  • Exercise 22
  • Solution for Exercise 22
  • Interlude
  • Mirror, mirror
  • Exercise 23
  • Executive summary: when to use the induction tactic?
  • Resources
  • Version
• Reasoning equationally about accumulator-based recursive functions
  • Resources
  • A series of exercises
  • Exercise 24
  • Exercise 25
  • Exercise 26
  • Exercise 27
  • Exercise 28
  • Exercise 29
  • Exercise 30
  • Exercise 31
  • Exercise 32
  • Solution for Exercise 32
  • Exercise 33
  • Solution for Exercise 33
  • Exercise 34
  • Solution for Exercise 34
  • Exercise 35
  • Solution for Exercise 35
  • Exercise 36
  • Exercise 37
  • Exercise 38
  • Exercise 39
  • Exercise 40
  • Exercise 41
  • Exercise 42
  • Exercise 43
  • Exercise 44
  • Resources
  • Version
• Exercises for Week 05
  • Exercise 00
  • Standard mandatory exercise
  • Mandatory exercise in the form of a mini-project
  • Remaining mandatory exercises, modulo your time quota for LPP this week
  • Version
• Index of concepts for Week 05
  • Version