Lecture Notes, Week 07

• Life after the midterm project
  • Interlude
  • Life after the midterm project, sanely
  • Resources
  • Version
• Functional equality
  • Resources
  • Version
• A study of isometries in the equilateral triangle
  • Credit
  • Resources
  • Domain of discourse
  • Rotations
  • Reflections
  • Performing two rotations in a row
  • A simple property with a proof by cases
  • Another simple property with a proof by cases
  • The reflexivity tactic, revisited
  • More language support for proofs by cases
  • Exercise 01
  • Resources
  • Version
• Soundness and completeness of equality predicates, revisited
  • Goal
  • Resources
  • An equality predicate for booleans
  • An equality predicate for Peano numbers
  • An equality predicate for the option type
  • Interlude
  • An equality predicate for pairs
  • An equality predicate for lists
  • Exercise 02
  • Exercise 03
  • Exercise 04
  • Exercise 05
  • Exercise 06
  • Exercise 07
  • Exercise 08
  • Exercise 09
  • Exercise 10
  • Exercise 11
  • Resources
  • Version
• The case of proofs by cases
  • Resources
  • A silly example
  • Soundness and completeness of an equality predicate for Booleans
  • About the Light of Inductil
  • Resources
  • Version
• Exercises for Week 07
  • Exercise 00
  • Mandatory exercises
  • Version
• Index of concepts for Week 07
  • Version