Lectures
| Week | Date | Topic | Notes |
|---|---|---|---|
| 1. | 1. sept | Logical Foundations Basics, Induction, | |
| 2. | 8. sept | Lists, Polymorphism | |
| 3. | 15. sept | Tactics, Logics in Coq | |
| 4. | 22. sept | Inductively defined Propositions, ProofObjects | |
| 5. | 29. sept | (cont.) IndProp, ProofObjects | |
| 6. | 6. oct | Maps. | |
| 7. | 13. oct | Simple Imperative Programs, More Automation. | |
| 8. | 20. oct | Program Equivalence | Tactics: specialize, pose, remember, assert |
| 9. | 27. oct | Hoare Logic I | |
| 10. | 3. nov | Hoare Logic I | |
| 11. | 10. nov | Hoare Logic II | |
| 12. | 17. nov | Small-step Operational Semantics | |
| 13. | 24. nov | Type Systems | |
| 14. | 1. dec | The Simply Typed Lambda-Calculus | |
| 15. | 8. dec | Properties of STLC | |
| 16. | 15. dec | delayed (daughter fell ill), will record and upload ASAP |
Note: After "Properties of STLC" we have a few chapters to consider but it is not too important that we look at any of them. Probably we shift/extend deadlines by at least one week at some point.
You can browse the material here: Logical Foundations and Programming Language Foundations. To learn it you should download the source files and solve exercises in Coq: lf.tgz and plf.tgz. Submit completed files to Moodle (available soon).
Year 2023
Plan
- 2 lectures per week
- show terse, prove all
- students submit their versions
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
Lectures
| Lecture # | Chapter | Notes |
|---|---|---|
| 1 | Preface.v | |
| Basics.v | ||
| Induction.v | ||
| Lists.v | ||
| Poly.v | ||
| Tactics.v | ||
| Logic.v | ||
| IndProp.v | ||
| Maps.v | ||
| Imp.v | ||
| AltAuto.v | ||
| AltAuto.v | ||
| Perm.v | ||
| Sort.v | ||
| Multiset.v | ||
| Selection.v | ||
| Merge.v | ||
| SearchTree.v | ||
| Extract.v | ||
| ADT.v | ||
| Redblack.v |
LF
Preface.v
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
- exercise: nandb, andb3
- plus-, mult-like Inductive, nat-s, Fixpoint
- exercise: factorial, ltb
- 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
- exercise: andb_true_elim2, zero_nbeq_plus_1, andb_eq_orb, identity_fn_applied_twice
Induction.v
- Goal: induction on nat-s
- Separate compilation
- Proof by Induction
- tactics: induction
- exercise: mul_0_r, plus_n_Sm, add_comm, add_assoc, double_plus
- Proofs Within Proofs
- tactics: assert
- Formal vs. Informal Proof
- More exercises
- tactics: replace
- exercise: add_shuffle3, mul_comm, mult_assoc, leb_refl, eqb_refl
Lists.v
- Goal: data structures
- Pairs of Numbers
- exercise: snd_fst_is_swap
- Lists of Numbers
- exercise: list_funs, alternate,
- Bags via Lists
- exercise: bag_functions
- Reasoning About Lists, Induction on Lists, List Exercises
- exercise: list_exercises, eqblist, count_member_nonzero, rev_injective
- Options
- exercise: hd_error
- Partial Maps
- eqb_id_refl, update_eq, update_neq
Poly.v
- Goal: almost std. lib. definitions, exercises
- Polymorphic Lists
- exercises: poly_exercises, more_poly_exercises
- Polymorphic Pairs
- exercises: split
- Polymorphic Options, Functions as Data, Anonymous Functions
- filter_even_gt7, partition
- Map
- map_rev, flat_map
- Fold
- fold_length
- Functions That Construct Functions
Tactics.v
- Goal: tools to prove almost anything
- The [apply] Tactic
- tactics: apply
- exercises: silly_ex, apply_exercise1
- The [apply with] Tactic
- tactics: apply with
- exercises: trans_eq_exercise
- The [injection] and [discriminate] Tactics
- tactics: injection, discriminate
- exercises: injection_ex3, discriminate_ex3
- Using Tactics on Hypotheses
- tactics: apply in
- Varying the Induction Hypothesis
- tactics: generalize dependent
- exercises: eqb_true, gen_dep_practice
- Unfolding Definitions, Using [destruct] on Compound Expressions
- tactics: unfold
- exercises: combine_split, destruct_eqn_practice
- Additional Exercises
- exercises: -eqb_sym, eqb_trans, filter_exercise
Logic.v
- Goal: tools for the logic idioms
- the Prop type, Logical Connectives
- exercises: and_exercise, and_assoc, or_commut
- Falsehood and Negation
- exercises: not_implies_our_not, contrapositive, not_both_true_and_false
- Truth, Logical Equivalence
- exercises: iff_properties
- Setoids and Logical Equivalence
- Existential Quantification
- exercises: dist_not_exists, dist_exists_or
- Programming with Propositions
- exercises: In_map_iff (long?), All_In
- Applying Theorems to Arguments
- Functional Extensionality
- exercises: tr_rev_correct, even_double_conv,
- Propositions vs. Booleans, Working with Decidable Properties
- exercises: logical_connectives,eqb_list_true_iff, All_forallb,
- Classical vs. Constructive Logic
- exercises: excluded_middle_irrefutable, not_exists_dist
IndProp.v
- Goal: Adding theories (safely)
- The Collatz Conjecture, Transitive Closure, Permutations, Evenness
- exercises: ev_double
- Using Evidence in Proofs
- inversion_practice, ev5_nonsense
- Induction on Evidence
- ev_sum, ev_ev__ev
- 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
- exp_match_ex1, re_not_empty, 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
- reflect_iff,eqbP_practice
Maps.v
- Goal: data structure, exercise
- The Coq Standard Library, Identifiers, Total Maps
- t_apply_empty, t_update_eq, t_update_neq, t_update_shadow, t_update_same, t_update_permute
- 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
- optimize_0plus_b_sound
- Evaluation as a Relation
- beval_iff_bevalR
- Expressions With Variables, Commands, Evaluating Commands
- ceval_example2
- Additional Exercises
- execute_app, s_compile_correct_aux, s_compile_correct
AltAuto.v
- Goal:
- Coq Automation
- re_opt (keep toplevel struct., delay inversion)
- Decision Procedures, Search Tactics
- tactics: lia, auto, info_auto.
- weak_pumping (copy solution, then simplify)
AltAuto.v
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
- 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
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)
- 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_rest_length, select_fst_leq, select_smallest, select_in,
- 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 SearchTree, Invariant
- empty_tree_BST, insert_BST
- Correctness of BST Operations
- bound_default
- 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]
- elements_empty,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))
- 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