Lecture Notes, Week 03

• Formalizing a proof with the Coq Proof Assistant
  • Goal
  • Resources
  • A sample of informal proofs
  • A first informal proof
  • Food for thought
  • Interlude about the first informal proof
  • A second informal proof
  • A third informal proof
  • Interlude about the third informal proof
  • TCPA: a domain-specific language for writing proofs
  • The first informal proof, formalized
  • Interlude about the first formal proof
  • Checkpoint
  • The second informal proof, formalized
  • The third informal proof, formalized
  • Interlude about the third formal proof
  • Exercise 01
  • Exercise 02
  • Exercise 03
  • Solution for Exercise 03
  • Exercise 04
  • Exercise 05
  • Exercise 06
  • Resources
  • Version
• The intro tactic
  • Resources
  • A simple example
  • What’s in a name?
  • Common naming conventions
  • The intros tactic
  • Naming, e.g., conjunctions vs. naming components of conjunctions
  • Naming the components of nested conjunctions
  • Naming, e.g., disjunctions vs. naming components of disjunctions
  • Naming the components of nested conjunctions and disjunctions
  • Resources
  • Version
• The revert tactic
  • Resources
  • The simple example, revisited
  • Practical use of the revert tactic
  • Interlude
  • Using the revert tactic with several arguments
  • Resources
  • Version
• Proving logical properties with the Coq Proof Assistant
  • Goal
  • Resources
  • Logical conjunction
  • Proving a nested logical conjunction
  • Logical conjunction associates to the right
  • Interlude about not drifting to the right when proving a flat conjunction
  • Logical equivalence
  • Logical disjunction
  • Creating subgoals
  • Exercise 07
  • Solution for Exercise 07
  • Improved solution for Exercise 07
  • Exercise 08
  • Exercise 09
  • Exercise 10
  • Exercise 11
  • Exercise 12
  • On the implication of an implication
  • Exercise 13
  • Logical negation
  • Three proofs of the modus tollens rule of inference
  • Exercise 14
  • Interlude: Solution for Exercise 14
  • Exercise 15
  • Interlude: Solution for Exercise 15
  • Exercise 16
  • Partial solution for Exercise 16
  • Exercise 17
  • Exercise 18
  • Postlude
  • Resources
  • Version
• Exercises for Week 03
  • Exercise 00
  • Mandatory exercises
  • Optional exercises
  • Exercise about types
  • Hint for the exercise about types
  • Exercise about propositions
  • A mindfulness exercise
  • Version
• Index of concepts for Week 03
  • Version