Lecture Notes, Week 07

• Functional equality
  • Postlude
  • Resources
  • Version
• The ring tactic
  • Interlude
  • Resources
  • Version
• Existential declarations, revisited
  • Exercise 01
  • Solution for Exercise 01
  • Exercise 02
  • Interlude
  • Exercise 03
  • Interlude
  • Exercise 04
  • Resources
  • Version
• More about the exists tactic
  • Exercise 05
  • Partial solution for Exercise 05
  • Exercise 06
  • Partial solution for Exercise 06
  • Interlude
  • Aftermath
  • Exercise 07
  • Exercise 08
  • Exercise 09
  • Postlude about vacuous specifications
  • Exercise 10
  • Postlude (continued)
  • Exercise 11
  • Postlude (ended)
  • Resources
  • Version
• Ex falso quodlibet
  • A property that does not hold
  • Exercise 12
  • Exercise 13
  • Interlude
  • Exercise 13
  • An equivalence
  • Exercise 14
  • Revisiting the proposition that does not hold
  • Exercise 15
  • Exercise 16
  • Resources
  • Version
• Soundness and completeness of equality predicates
  • Resources
  • Structural equality for Booleans
  • Structural equality for Peano numbers
  • Exercise 17
  • Structural equality for polymorphic values
  • Structural equality for optional values
  • Exercise 18
  • Structural equality for pairs
  • Exercise 19
  • Structural equality for binary trees
  • Exercise 20
  • Aftermath
  • Resources
  • Version
• A simple problem
  • Exercise 21
  • Exercise 22
  • Exercise 23
  • Partial solution for Exercise 23
  • Exercise 24
  • Exercise 25
  • Exercise 26
  • Exercise 27
  • Exercise 28
  • Exercise 29
  • Exercise 30
  • Exercise 31
  • Interlude
  • Exercise 32
  • Postlude
  • Exercise 33
  • Credit
  • Version
• The situation so far
  • Goal
  • Resources
  • Toplevel forms
  • Keywords
  • Tactics
  • Reasoning equationally about recursive functions
  • Proofs by induction
  • Proof strategies
  • The Coq Proof Assistant inside: normalization steps
  • The Coq Proof Assistant inside: where to rewrite
  • The Coq Proof Assistant inside: all the syntactic sugar
  • Exercise 34
  • Resources
  • Version
• Exercises for Week 07
  • Exercise 00
  • Mandatory exercises (to be carried out after the midterm project)
  • Optional exercises
  • Version
• Index of concepts for Week 07
  • Version