Lectures & Homework
We will go through a number of chapters in LF and VFA. For homework, you need to submit the same chapter files. Some chapters introduce new tactics or syntax but most are about practicing theorem proving in some new aspect. See the goals for each chapter.
Note that if you submit homework past the due date, the points for that submission will be multiplied by 0.6.
Lectures
| Lecture | Chapter | Notes |
|---|---|---|
| (1) 5. sept | Basics.v | |
| (2) 6. sept (video) | Basics.v | Basics.v due on 13. Sept. |
| (3) 12. sept | Induction.v | |
| (4) 13. sept (video) | Induction.v | Induction.v due on 20. Sept. |
| (5) 19. sept | Motivations, Lists.v | |
| (6) 20. sept (video) | Lists.v | Lists.v due on 27. Sept. |
| (7) 26. sept | Poly.v | |
| (8) 27. sept (video) | Poly.v Tactics.v | Poly.v due on 4. Oct. |
| (9) 3. oct | Tactics.v Logic.v | Tactics.v due on 10. Oct. |
| (10) 4. oct (video) | Logic.v | |
| (11) 10. oct | Logic.v | |
| (12) 11. oct (video) | Logic.v | Logic.v due on 21. Oct. |
| (13) 17. oct | IndProp.v | |
| (14) 18. oct (video) | IndProp.v | |
| (15) 24. oct | IndProp.v | |
| (16) 25. oct (video) | IndProp.v | Logic.v due on 7. Nov. |
| (17) 31. oct | ProofObjects.v | |
| (18) 1. Nov (video) | ProofObjects.v AltAuto.v | ProofObjects.v due on 8. Nov. |
| (19) 7. Nov | AltAuto.v | AltAuto.v due on 14. Nov. |
| (18) 8. Nov (video) | Perm.v | Perm.v due on 15. Nov. |
| (20) 14. Nov | Sort.v | |
| (21) 15. Nov (video) | Sort.v | Sort.v due on 22. Nov. |
| (22) 21. Nov | Multiset.v | Multiset.v due on 29. Nov. |
| (23) 22. Nov (video) | Selection.v | (video from 2022) |
| (24) 28. Nov | Selection.v Merge.v | Selection.v due on 5. Dec. |
| (25) 29. Nov (video) | Merge.v | Merge.v due on 6. Dec. |
| (26) 5. Dec | no lecture | |
| (27) 6. Dec (video) | SearchTree.v (video from 2022) | |
| (28) 12. Dec | SearchTree.v | Forgot to hit Record :( but there is a recap of proofs with the next video |
| (29) 13. Dec (video) | SearchTree.v | SearchTree.v due on 3. Jan |
| (30) 19. Dec | Wrap-up, Extract.v | Extract.v due on 10. Jan |
| (31) 20. Dec (video) | Redblack.v | (Submitting Redblack.v is optional) |
LF
Preface.v
- Goal: talk about the course
Basics.v
- Goal: base FP language, proof language, simple proofs
- Data and Functions
- Enum-like Inductive, Definition, Compute, bool, match-with-end
- tactics: simpl, reflexivity
- Proof by Simplification, Proof by Rewriting
- tactics: intros
- exercise: plus_id_exercise, mult_n_1
- Proof by Case Analysis
- bullets
- tactics: destruct X as eqn:Y
Induction.v
- Goal: induction on natural numberss
- Separate compilation
- Proof by Induction
- tactics: induction
- Proofs Within Proofs
- tactics: assert
- Formal vs. Informal Proof
- More exercises
- tactics: replace
Lists.v
- Goal: look at data structures
- Pairs of Numbers
- Lists of Numbers
- Bags via Lists
- Reasoning About Lists, Induction on Lists, List Exercises
involution_injective, rev_injective
- Options
- Partial Maps
Poly.v
- Goal: look at almost std. lib. definitions, exercises
- Polymorphic Lists
- Polymorphic Pairs
- Polymorphic Options, Functions as Data, Anonymous Functions
- Map
- Fold
- Functions That Construct Functions
Tactics.v
- Goal: provide tools to theoretically prove almost anything
- The [apply] Tactic
- tactics: apply
- The [apply with] Tactic
- tactics: apply with
- The [injection] and [discriminate] Tactics
- tactics: injection, discriminate
- Using Tactics on Hypotheses
- tactics: apply in
- Varying the Induction Hypothesis
- tactics: generalize dependent
- Unfolding Definitions, Using [destruct] on Compound Expressions
- tactics: unfold
- Additional Exercises
Logic.v
- Goal: more tools for easier proving of logic idioms
- the Prop type, Logical Connectives
- Falsehood and Negation
- Truth, Logical Equivalence
- Setoids and Logical Equivalence
- Existential Quantification
- Programming with Propositions
- Applying Theorems to Arguments
- Functional Extensionality
- Propositions vs. Booleans, Working with Decidable Properties
- Classical vs. Constructive Logic
IndProp.v
- Goal: Safely adding theories/assumptions
- The Collatz Conjecture, Transitive Closure, Permutations, Evenness
- Using Evidence in Proofs
- Induction on Evidence
- Inductive Relations
- le_exercises (not all induction H, e.g., Sn_le_Sm__n_le_m: inversion, lt_ge_cases, leb_complete: ind n+destr m), subsequence
- A Digression on Notation
- Case Study: Regular Expressions
- tactics: remember
- weak_pumping (hint: finish 1st App case and copy-paste the rest, lemmas: app_length, add_le_cases, rewrite app_assoc, plus_le, pumping_constant_0_false hint: destruct s1 in MStarApp case)
- Case Study: Improving Reflection
Maps.v
- Goal: more data structures and exercises
- The Coq Standard Library, Identifiers, Total Maps
- Partial Maps
Imp.v
- Goal: exercise tactic(al)s and inductives
- Arithmetic and Boolean Expressions, Coq Automation
- tactics: ;, try, repeat, lia, clear, rename, assumption, contradiction, constructor
- Evaluation as a Relation
- Expressions With Variables, Commands, Evaluating Commands
- Additional Exercises
AltAuto.v
- Goal: automatically proving (large number) of simple cases
- Tacticals; The try Tactical; The Sequence Tactical ; (Simple Form)
- The Sequence Tactical ; (Local Form)
- The repeat Tactical
- Tactics that Make Mentioning Names Unnecessary
- Automatic Solvers
- tactics: lia, congurence, intuition
- Search Tactics
- tactics: auto, eauto
- Ltac Functions
VFA
Perm.v
- Goal: Correctness proofs require us to state the correctness condition. Permutations can be used to specify sorting algorithms.
- The Less-Than Order on the Natural Numbers, Swapping, Permutations
- permut_example, not_a_permutation
- An Inversion Tactic
- Summary: Comparisons and Permutations
- Forall_perm
Sort.v
- Goal: One simple functional algorithm we can prove correct: Insertion sort.
- The Insertion-Sort Program, Specification of Correctness, Proof of Correctness
- insert_sorted, sort_sorted, insert_perm, sort_perm, insertion_sort_correct
- Validating the Specification
- sorted'_sorted, sorted'_sorted
- Proving Correctness from the Alternative Spec
- insert_sorted'
Multiset.v
- Goal: An alternative way of specifying sorting algorithms.
- Multisets
- union_assoc, union_comm, union_swap
- Specification of Sorting, Verification of Insertion Sort
- insert_contents, sort_contents, insertion_sort_correct
- Equivalence of Permutation and Multiset Specifications
- perm_contents
- contents_nil_inv (hint: specialize), contents_cons_inv, contents_insert_other
- contents_perm (hint: pose proof (H a) and specialize (H z))
- same_contents_iff_perm, sort_specifications_equivalent
Selection.v
- Goal: VFA practice, Function and termination measure
- The Selection-Sort Program, Proof of Correctness
- select_perm (hint: eauto surprisingly powerful)
- select_rest_length
- selsort_perm (hint: induction n, destruct l; use "apply select_perm in E" to fix the first element of the permutation; then use perm_skip and Permutation_length)
- selection_sort_perm, select_fst_leq, select_smallest, select_in, le_all__le_one
- cons_of_small_maintains_sort (hint: destruct on bl and its length; use select_in and Forall_forall)
- selsort_sorted, selection_sort_sorted, selection_sort_is_correct
- Recursive Functions That are Not Structurally Recursive
- selsort'_perm
Merge.v
- Goal: More VFA practice; Functional induction
- Merge Sort
- split_perm (hint: Permutation_trans and Permutation_middle)
- sorted_merge1 (hint: bdestruct and auto do most work),
- sorted_merge (hint: induction on l1 and l2, use sorted_merge1)
- mergesort_sorts, merge_perm (hint: induction on l1 and l2)
- mergesort_perm (hint: mergesort_ind)
SearchTree.v
- Goal: Functional algorithms typically use non-trivial data structures -- which require specification.
- BST Implementation, Invariant
- empty_tree_BST, insert_BST
- Correctness of BST Operations
- bound_default
- BSTs vs. Higher-order Functions
- lookup_insert_shadow, lookup_insert_same, lookup_insert_permute
- Converting a BST to a List
- elements_complete (hint: in_app_iff),
- elements_preserves_forall (hint: Forall_app),
- elements_preserves_relation
- elements_correct (Hint: induction on BST t, then use in_app_iff, then elements_preserves_relation + bdall)
- elements_complete_inverse, elements_correct_inverse, sorted_app,
- sorted_elements (hint: map_app, sorted_app, Forall_map, Forall_forall, elements_preserves_forall)
- A Faster [elements] Implementation
- fast_elements_eq_elements
- An Algebraic Specification of [elements]
- kvs_insert_split (hint: induction on e1, (b)destruct until you can rewrite IHe1; then bdall)
- Model-based Specifications
- in_fst, in_map_of_list, not_in_map_of_list,bound_relate, lookup_relate, insert_relate
- Efficiency of Search Trees
Extract.v
- Goal: We see how to use the verified functional algorithm.
- Note: might need to change the working directory using 'Cd "...".'
- Extraction
- Lightweight Extraction to [int]
- Insertion Sort, Extracted
- sort_int_correct
- Binary Search Trees, Extracted
- lookup_insert_eq (hint: bdall), lookup_insert_neq (hint: bdall and Abs_inj)
- Performance Tests
ADT.v
- Goal: How to write and prove modular code in Coq.
- The Table ADT, Implementing [Table] with Functions
- NatFunTableExamples
- Implementing [Table] with Lists
- lists_table
- Implementing [Table] with BSTs
- Tables with an [elements] Operation
- Model-based Specification
- list_etable_abs
- Summary of ADT Verification
Redblack.v
- Goal: Verifying Redblack searchtree operations (quite realistic algorithms)
- Implementation
- Case-Analysis Automation
- The BST Invariant
- balanceP, insP, ins_BST
- insert_BST (hint: destruct ins k v t and use ins_BST on some hypthesis)
- Verification
- balance_lookup
- lookup_ins_eq
- lookup_ins_neq (hint: bdall and Abs_inj)
- lookup_insert_eq, lookup_insert_neq (hint: destruct (ins k v t)), lookup_insert
- Efficiency
- RB_blacken_parent
- RB_blacken_root
- ins_RB (hint: similar start "destruct (IHt1 n0); clear IHt1. ..." in all 3 cases)
- insert_RB
- redblack_balanced
- Performance of Extracted Code