Kontrollitud funktsionaalsed algoritmid 2022/23 sügis

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.

Lectures

Lecture	Chapter	Notes
(1) 30. aug	Basics.v
(2) 1. sept	Basics.v	Basics.v due 15.09
(3) 6. sept	Induction.v
(4) 8. sept	Induction.v (Panopto only)	Induction.v due 15.09
(5) 13. sept	Lists.v
(6) 15. sept	Lists.v Poly.v	Induction.v due 27.09
(7) 20. sept	Poly.v Tactics.v	Induction.v due 27.09
(8) 22. sept	Tactics.v Logic.v	Tactics.v due 29.09
(9) 27. sept	Logic.v
(10) 29. sept	Logic.v IndProp.v	Logic.v due 11.10
(11) 4. oct	IndProp.v
(12) 6. oct	no lecture (daughters adenoid surgery)
(13) 11. oct	IndProp.v
(14) 13. oct	IndProp.v	IndProp.v due 20.10
(15) 18. oct	Maps.v, Imp.v	Maps.v due 27.10
(16) 20. oct	Imp.v, AltAuto.v	Imp.v due 27.10
(17) 25. oct	AltAuto.v Perm.v	AltAuto.v due 3.11
(18) 27. oct	Sort.v
(19) 1. nov	Sort.v Multiset.v
(20) 3. nov	Multiset.v Selection.v	Sort.v and Multiset.v due 10.11
(21) 8. nov	Selection.v
(22) 10. nov	Selection.v Merge.v	Selection.v due 17.11
(23) 15. nov	Merge.v SearchTree.v	Merge.v due 22.11
(24) 17. nov	SearchTree.v
(25) 22. nov	SearchTree.v	{$^*$}) Lemma find_app missing.
(26) 24. nov	SearchTree.v, ADT.v	SearchTree.v due 1.12
(27) 29. nov	Extract.v	SearchTree.v due 13.12
(28) 1. dec	Redblack.v	Redblack.v is not HW this year.
(29) 6. dec	Redblack.v (Panopto only)	Redblack.v is not HW this year.

{$^*$}) Missing lemma for lookup_relate (in SearchTree.v):

 Lemma find_app : forall (V : Type) (d : V) (k : key) (l1 l2 : list (key * V)),
     find d k (map_of_list (l1 ++ l2)) = find (find d k (map_of_list l2)) k (map_of_list l1).

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
   • exercise: nandb, andb3
   • plus-, mult-like Inductive, nat-s, Fixpoint
   • exercise: factorial, ltb
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
   • exercise: andb_true_elim2, zero_nbeq_plus_1, andb_eq_orb, identity_fn_applied_twice

Induction.v

• Goal: induction on natural numberss

1. Separate compilation
2. Proof by Induction
   • tactics: induction
   • exercise: mul_0_r, plus_n_Sm, add_comm, add_assoc, double_plus
3. Proofs Within Proofs
   • tactics: assert
4. Formal vs. Informal Proof
5. More exercises
   • tactics: replace
   • exercise: add_shuffle3, mul_comm, mult_assoc, leb_refl, eqb_refl

Lists.v

• Goal: look at data structures

1. Pairs of Numbers
   • exercise: snd_fst_is_swap
2. Lists of Numbers
   • exercise: list_funs, alternate,
3. Bags via Lists
   • exercise: bag_functions
4. Reasoning About Lists, Induction on Lists, List Exercises
   • exercise: list_exercises, eqblist, count_member_nonzero, involution_injective, rev_injective
5. Options
   • exercise: hd_error
6. Partial Maps
   • eqb_id_refl, update_eq, update_neq

Poly.v

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

1. Polymorphic Lists
   • exercises: poly_exercises, more_poly_exercises
2. Polymorphic Pairs
   • exercises: split
3. Polymorphic Options, Functions as Data, Anonymous Functions
   • filter_even_gt7, partition
4. Map
   • map_rev, flat_map
5. Fold
   • fold_length
6. Functions That Construct Functions

Tactics.v

1. Goal: provide tools to theoretically prove almost anything
2. The [apply] Tactic
   • tactics: apply
   • exercises: silly_ex, apply_exercise1
3. The [apply with] Tactic
   • tactics: apply with
   • exercises: trans_eq_exercise
4. The [injection] and [discriminate] Tactics
   • tactics: injection, discriminate
   • exercises: injection_ex3, discriminate_ex3
5. Using Tactics on Hypotheses
   • tactics: apply in
6. Varying the Induction Hypothesis
   • tactics: generalize dependent
   • exercises: eqb_true, gen_dep_practice
7. Unfolding Definitions, Using [destruct] on Compound Expressions
   • tactics: unfold
   • exercises: combine_split, destruct_eqn_practice
8. Additional Exercises
   • exercises: eqb_sym, eqb_trans, filter_exercise

Logic.v

• Goal: more tools for easier proving of logic idioms

1. the Prop type, Logical Connectives
   • exercises: and_exercise, and_assoc, or_commut
2. Falsehood and Negation
   • exercises: not_implies_our_not, contrapositive, not_both_true_and_false
3. Truth, Logical Equivalence
   • exercises: or_distributes_over_and
4. Setoids and Logical Equivalence
5. Existential Quantification
   • exercises: dist_not_exists, dist_exists_or
6. Programming with Propositions
   • exercises: In_map_iff (long?), In_app_iff, All_In
7. Applying Theorems to Arguments
8. Functional Extensionality
   • exercises: even_double_conv,
9. Propositions vs. Booleans, Working with Decidable Properties
   • exercises: logical_connectives,eqb_list_true_iff, eqb_neq, All_forallb,
10. Classical vs. Constructive Logic
    • exercises: excluded_middle_irrefutable, not_exists_dist

IndProp.v

• Goal: Safely adding theories/assumptions

1. The Collatz Conjecture, Transitive Closure, Permutations, Evenness
   • exercises: ev_double
2. Using Evidence in Proofs
   • inversion_practice, ev5_nonsense
3. Induction on Evidence
   • ev_sum, ev_ev__ev
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
   • 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)
7. Case Study: Improving Reflection
   • reflect_iff,eqbP_practice

Maps.v

• Goal: more data structures and exercises

1. 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
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
   • optimize_0plus_b_sound
2. Evaluation as a Relation
   • beval_iff_bevalR
3. Expressions With Variables, Commands, Evaluating Commands
   • ceval_example2
4. Additional Exercises
   • execute_app, s_compile_correct_aux, s_compile_correct

AltAuto.v

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

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

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