Lecture Notes, Week 06

• About unfolding calls
  • Version
• The exists tactic, revisited
  • Exercise 01
  • Partial solution for Exercise 01
  • Exercise 02
  • Partial solution for Exercise 02
  • Interlude
  • Aftermath
  • Exercise 03
  • Exercise 04
  • Exercise 05
  • Postlude about vacuous specifications
  • Exercise 06
  • Postlude (continued)
  • Exercise 07
  • Postlude (ended)
  • Resources
  • Version
• Ex falso quodlibet
  • A property that does not hold
  • Exercise 08
  • Exercise 09
  • An equivalence
  • Exercise 10
  • Revisiting the proposition that does not hold
  • Exercise 11
  • Exercise 12
  • Resources
  • Version
• Soundness and completeness of equality predicates
  • Resources
  • Structural equality for Booleans
  • Structural equality for Peano numbers
  • Exercise 13
  • Structural equality for polymorphic values
  • Structural equality for optional values
  • Exercise 14
  • Structural equality for pairs
  • Exercise 15
  • Structural equality for binary trees
  • Exercise 16
  • Aftermath
  • Resources
  • Version
• A simple problem
  • Exercise 17
  • Exercise 18
  • Exercise 19
  • Exercise 20
  • Exercise 21
  • Exercise 22
  • Exercise 23
  • Exercise 24
  • Exercise 25
  • Exercise 26
  • Exercise 27
  • Interlude
  • Exercise 28
  • Postlude
  • Exercise 29
  • 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 30
  • Resources
  • Version
• Exercises for Week 06
  • Exercise 00
  • Mandatory exercises
  • Optional exercises
  • Version
• Index of concepts for Week 06
  • Version