Verified Functional Algorithms 2024/25 fall

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 delayed

LF

Preface.v

• Goal: talk about the course

Basics.v

• Goal: base FP language, proof language, simple proofs

1. Data and Functions
   • Enum-like Inductive, Definition, Compute, bool, match-with-end
   • tactics: simpl, reflexivity
2. Proof by Simplification, Proof by Rewriting
   • tactics: intros
   • exercise: plus_id_exercise, mult_n_1
3. Proof by Case Analysis
   • bullets
   • tactics: destruct X as eqn:Y

Induction.v

• Goal: induction on natural numberss

1. Separate compilation
2. Proof by Induction
   • tactics: induction
3. Proofs Within Proofs
   • tactics: assert
4. Formal vs. Informal Proof
5. More exercises
   • tactics: replace

Lists.v

• Goal: look at data structures

1. Pairs of Numbers
2. Lists of Numbers
3. Bags via Lists
4. Reasoning About Lists, Induction on Lists, List Exercises

involution_injective, rev_injective

1. Options
2. Partial Maps

Poly.v

• Goal: look at almost std. lib. definitions, exercises

1. Polymorphic Lists
2. Polymorphic Pairs
3. Polymorphic Options, Functions as Data, Anonymous Functions
4. Map
5. Fold
6. Functions That Construct Functions

Tactics.v

1. Goal: provide tools to theoretically prove almost anything
2. The [apply] Tactic
   • tactics: apply
3. The [apply with] Tactic
   • tactics: apply with
4. The [injection] and [discriminate] Tactics
   • tactics: injection, discriminate
5. Using Tactics on Hypotheses
   • tactics: apply in
6. Varying the Induction Hypothesis
   • tactics: generalize dependent
7. Unfolding Definitions, Using [destruct] on Compound Expressions
   • tactics: unfold
8. Additional Exercises

Logic.v

• Goal: more tools for easier proving of logic idioms

1. the Prop type, Logical Connectives
2. Falsehood and Negation
3. Truth, Logical Equivalence
4. Setoids and Logical Equivalence
5. Existential Quantification
6. Programming with Propositions
7. Applying Theorems to Arguments
8. Functional Extensionality
9. Propositions vs. Booleans, Working with Decidable Properties
10. Classical vs. Constructive Logic

IndProp.v

• Goal: Safely adding theories/assumptions

1. The Collatz Conjecture, Transitive Closure, Permutations, Evenness
2. Using Evidence in Proofs
3. Induction on Evidence
4. 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
5. A Digression on Notation
6. 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)
7. Case Study: Improving Reflection

Maps.v

• Goal: more data structures and exercises

1. The Coq Standard Library, Identifiers, Total Maps
2. Partial Maps

Imp.v

• Goal: exercise tactic(al)s and inductives

1. Arithmetic and Boolean Expressions, Coq Automation
   • tactics: ;, try, repeat, lia, clear, rename, assumption, contradiction, constructor
2. Evaluation as a Relation
3. Expressions With Variables, Commands, Evaluating Commands
4. Additional Exercises

AltAuto.v

• Goal: automatically proving (large number) of simple cases

1. Tacticals; The try Tactical; The Sequence Tactical ; (Simple Form)
2. The Sequence Tactical ; (Local Form)
3. The repeat Tactical
4. Tactics that Make Mentioning Names Unnecessary
5. Automatic Solvers
   • tactics: lia, congurence, intuition
6. Search Tactics
   • tactics: auto, eauto
7. Ltac Functions

VFA

Perm.v

• Goal: Correctness proofs require us to state the correctness condition. Permutations can be used to specify sorting algorithms.

1. The Less-Than Order on the Natural Numbers, Swapping, Permutations
   • permut_example, not_a_permutation
2. An Inversion Tactic
3. Summary: Comparisons and Permutations
   • Forall_perm

Sort.v

• Goal: One simple functional algorithm we can prove correct: Insertion sort.

1. The Insertion-Sort Program, Specification of Correctness, Proof of Correctness
   • insert_sorted, sort_sorted, insert_perm, sort_perm, insertion_sort_correct
2. Validating the Specification
   • sorted'_sorted, sorted'_sorted
3. Proving Correctness from the Alternative Spec
   • insert_sorted'

Multiset.v

• Goal: An alternative way of specifying sorting algorithms.

1. Multisets
   • union_assoc, union_comm, union_swap
2. Specification of Sorting, Verification of Insertion Sort
   • insert_contents, sort_contents, insertion_sort_correct
3. 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

1. 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
2. Recursive Functions That are Not Structurally Recursive
   • selsort'_perm

Merge.v

• Goal: More VFA practice; Functional induction

1. 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.

1. BST Implementation, Invariant
   • empty_tree_BST, insert_BST
2. Correctness of BST Operations
   • bound_default
3. BSTs vs. Higher-order Functions
   • lookup_insert_shadow, lookup_insert_same, lookup_insert_permute
4. 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)
5. A Faster [elements] Implementation
   • fast_elements_eq_elements
6. An Algebraic Specification of [elements]
   • kvs_insert_split (hint: induction on e1, (b)destruct until you can rewrite IHe1; then bdall)
7. Model-based Specifications
   • in_fst, in_map_of_list, not_in_map_of_list,bound_relate, lookup_relate, insert_relate
8. 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 "...".'

1. Extraction
2. Lightweight Extraction to [int]
3. Insertion Sort, Extracted
   • sort_int_correct
4. Binary Search Trees, Extracted
   • lookup_insert_eq (hint: bdall), lookup_insert_neq (hint: bdall and Abs_inj)
5. Performance Tests

ADT.v

• Goal: How to write and prove modular code in Coq.

1. The Table ADT, Implementing [Table] with Functions
   • NatFunTableExamples
2. Implementing [Table] with Lists
   • lists_table
3. Implementing [Table] with BSTs
4. Tables with an [elements] Operation
5. Model-based Specification
   • list_etable_abs
6. Summary of ADT Verification

Redblack.v

• Goal: Verifying Redblack searchtree operations (quite realistic algorithms)

1. Implementation
2. Case-Analysis Automation
3. The BST Invariant
   • balanceP, insP, ins_BST
   • insert_BST (hint: destruct ins k v t and use ins_BST on some hypthesis)
4. 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
5. 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
6. Performance of Extracted Code