Exam
Requirements met for final assessment:
- wild boar, cuckoo, bufflehead, locust (checked on Dec 16th)
- vulture, shearwater, adder (checked on Jan 19th)
Exercises
- Basics.v
- Definition, Fixpoint, simpl, reflexivity: nandb, test_nandb*,andb3, test_andb3*, factorial, test_factorial*
- intros, rewrite: plus_id_exercise, mult_S_1
- destruct: andb_true_elim2, zero_nbeq_plus_1, andb_eq_orb
- Induction.v
- induction: mult_0_r, plus_n_Sm, plus_comm, plus_assoc, double_plus, evenb_S
- Lists.v
- snd_fst_is_swap, fst_swap_is_snd
- app_nil_r, rev_app_distr, rev_involutive
- Tactics.v (also requires Poly.v)
- apply:silly_ex, rev_exercise1
- injection, discriminate: injection_ex_3, discriminate_ex_3
- IndProp.v (also requires Logic.v)
- inversion: SSSSev__even, even5_nonsense
- Theory Exercise 1 (tex)
- Deadline: Oct. 9th
- Smallstep.v (also requires Maps.v and Imp.v)
- value_not_same_as_normal_form (three versions), multistep_congr_2, eval__multistep, step__eval, multistep__eval
- Types.v
- value_is_nf, progress, preservation
- Stlc.v
- step_example5, typing_example_2_full, typing_example_3, typing_nonexample_3
- StlcProp.v
- progress', typable_empty__closed, soundness, unique_types
- StlcArith
- progress, preservation
- MoreStlc.v
- complete: subst, step, has_type, progress, appears_free_in, context_invariance, free_in_context, substitution_preserves_typing, preservation
- Theory Exercise 2 (tex)
- Deadline: Nov. 20th
- DepT.v
- vtail', vtail, vmap, unzip, tabulate, get, ev_eq, IsT1, IsTP, rewriteNat, IsTL, IsTAddOne, IsTLR, insert'_induction, insert, sort
- RecordSub.v
- sub_inversion_arrow, canonical_forms_of_arrow_types
Solutions for this task can no longer be submitted.
2. Induction.v
Solutions for this task can no longer be submitted.
3. Lists.v
Solutions for this task can no longer be submitted.
4. Tactics.v
Solutions for this task can no longer be submitted.
5. IndProp.v
Solutions for this task can no longer be submitted.
6. Exercise1
Solutions for this task can no longer be submitted.
7. Smallstep.v
Solutions for this task can no longer be submitted.
8. Types.v
Solutions for this task can no longer be submitted.
9. Stlc.v
Solutions for this task can no longer be submitted.
10. StlcProp.v
Solutions for this task can no longer be submitted.
11. StlcArith.v
Solutions for this task can no longer be submitted.
12. MoreStlc.v
Solutions for this task can no longer be submitted.
13. Exercise2
Solutions for this task can no longer be submitted.
14. DepT.v
Solutions for this task can no longer be submitted.
15. RecordSub.v
Solutions for this task can no longer be submitted.
16. ExamDecember
Solutions for this task can no longer be submitted.
17. ExamJanuary
Solutions for this task can no longer be submitted.