CS 798 Assignments
1 Basics (due Sep. 24)
2 Induction (due Sep. 27)
3 Lists (due Oct. 1)
4 Poly (due Oct. 5)
5 Tactics (due Oct. 12)
6 Logic (due Oct. 23)
7 Ind  Prop (due Nov. 8)
8 Proof  Objects (due Nov. 10)
9 Ind  Principles
10 Maps (due Nov. 13)
11 Imp (due Nov. 19)
12 Auto
13 Preparing for Volume II
14 Equiv (due mid Nov.)
15 Hoare (due late Nov.)
16 Hoare2, Hoare  As  Logic
17 Smallstep (due Dec. 3)
18 Types (not for credit)
19 Stlc (not for credit)
20 Stlc  Prop
7.0

CS 798 Assignments

Your work should be submitted to Marmoset, which is described on the course Web page.

Exercises will be scored according to the "star" level of difficulty indicated in the Coq file, using the following translation table (the score is the lower bound of the range of times in minutes each exercise is expected to take, as described in the Preface of "Software Foundations").

stars

 

score

1

 

1

2

 

5

3

 

10

4

 

30

Marking is automated (based on Coq compiler output) and no part marks will be awarded. Please do not try to fool the Coq compiler or the automated scoring; please answer the questions in the spirit in which they are asked. It is easy to forget the concluding "Qed."; you should check your work by compiling with coqc before submitting. Unless otherwise specified, assignments are due at 10:00 pm on the due date. Late assignments will not be graded, as solutions will be made available shortly after assignments are due.

1 Basics (due Sep. 24)

Complete all one-starred exercises in the Coq file Basics.v, plus the following exercises: mult_S_1, andb_true_elim2, boolean_functions, andb_eq_orb. The binary exercise will not be graded, but I recommend it (there is an ungraded follow-up in the next file which is also worthwhile).

Total points available: 31.

2 Induction (due Sep. 27)

Complete the following exercises in the Coq file Induction.v: basic_induction, double_plus, evenb_S, mult_comm, more_exercises, eqb_refl.

Total points available: 40.

The following exercises will not be graded, but I recommend them: destruct_induction, plus_swap, binary_commute (this is a follow-up to binary from the previous file). The five-star binary_inverse exercise will teach you a lot, and the material at the end of the file on formal versus informal proof is also valuable.

3 Lists (due Oct. 1)

Complete all one-starred exercises in the Coq file Lists.v, plus the following exercises: list_funs, alternate, bag_functions, bag_more_functions, list_exercises, eqblist_refl, remove_does_not_increase_count, rev_injective (your theorem should have the same name as the exercise, and please try to find the simpler solution), hd_error, option_elim_hd.

Total points available: 102.

The following exercises will not be graded, but I recommend them: bag_theorem, bag_count_sum, baz_num_elts.

4 Poly (due Oct. 5)

Complete the following exercises in the Coq file Poly.v: poly_exercises, more_poly_exercises, split, hd_error_poly, filter_even_gt7, partition, map_rev, flat_map, fold_length, fold_map (call your theorem fold_map_correct, as stated in the file), currying.

Total points available: 66.

The following exercises will not be graded, but I recommend them: mumble_grumble, combine_checks, implicit_args, fold_types_different, nth_error_informal, church_succ, church_add, church_mult, church_exp.

5 Tactics (due Oct. 12)

Complete the following exercises in the Coq file Tactics.v: silly_ex, apply_exercise1, apply_with_exercise, injection_ex_3, discriminate_ex_3, plus_n_n_injective, eqb_true, gen_dep_practice, combine_split, destruct_eqn_practice, eqb_sym, eqb_trans, split_combine, filter_exercise, forall_exists_challenge (call your theorem existsb_existsb).

Total points available: 137.

The following exercises will not be graded, but I recommend them: apply_rewrite, beq_nat_true_informal, beq_nat_symm_informal, index_after_last_informal.

6 Logic (due Oct. 23)

Complete all one-starred exercises in the Coq file Logic.v, plus the following exercises: and_exercise, and_assoc, not_implies_our_not, contrapositive, or_distributes_over_and, dist_exists_or, In_map_iff, In_app_iff, All, combine_odd_even, tr_rev_correct, evenb_double_conv, logical_connectives, eqb_list, All_forallb, excluded_middle_irrefutable, not_exists_dist.

Total points available: 152.

The following exercises will not be graded, but I recommend them: double_neg_inf, informal_not_PNP.

The five-starred classical_axioms exercise is a very nice challenge and you will learn a lot by doing it. Note that there are twenty different implications possible, but you don’t have to do twenty proofs; you have to choose which ones to prove in order to get all the others by transitivity. There are many different choices and proofs possible.

7 IndProp (due Nov. 8)

Complete the following exercises in the Coq file IndProp.v: ev_double, inversion_practice, even5_nonsense, ev_sum, ev_ev, ev_ev__ev, ev_plus_plus, le_exercises, leb_iff, exp_match_ex1, reg_exp_of_list_spec, re_not_empty, exp_match_ex2, reflect_iff, eqbP_practice.

Total points available: 193.

The following exercises will not be graded, but I recommend them: total_relation, empty_relation, R_provability, R_fact, subsequence, R_provability2, nostutter_defn, palindromes.

There are some more difficult ungraded exercises that are still worthwhile if you have the time: pumping (especially if you have learned about regular expressions before), filter_challenge, NoDup, pigeonhole_principle (doing this without excluded_middle is quite long and difficult, so it is up to you if you attempt it), and the extended exercise on a verified regular-expression matcher.

I do not recommend the palindrome_converse exercise. It requires the invention of a pretty complicated inductive hypothesis and at least one long, messy proof. The filter_challenge2 exercise is not as complicated but fairly lengthy.

8 ProofObjects (due Nov. 10)

Complete all exercises in the Coq file ProofObjects.v except for leibniz_equality__equality.

Total points available: 25.

9 IndPrinciples

There are no required exercises in the Coq file IndPrinciples.v, and there is no associated Marmoset project. I encourage you to complete the exercises if you find the topic of interest.

10 Maps (due Nov. 13)

Complete the following exercises in the Coq file Maps.v: t_apply_empty, t_update_eq, t_update_neq, t_update_shadow, eqb_stringP, t_update_same, t_update_permute.

Total points available: 36.

11 Imp (due Nov. 19)

Complete the following exercises in the Coq file Imp.v: optimize_0plus_b_sound, bevalR, ceval_example2, pup_to_n, loop_never_stops, no_whiles_eqv, stack_compiler, stack_compiler_correct.

Total points available: 95.

The following exercises will not be graded, but I recommend them: XtimesYinZ_spec, no_whiles_terminating. It is up to you whether or not you choose to do the rest of the exercises in the file. I would suggest saving your energy for upcoming material, which will make exercises like these easier.

12 Auto

There are no exercises associated with the Coq file Auto.v.

This marks the end of Volume I, Logical Foundations. The files below are from Volume II, Programming Language Foundations.

13 Preparing for Volume II

Here is one possible arrangement.
  • Make a new PLF directory. (It doesn’t have to be called that.)

  • Copy _CoqProject, Imp.v, Maps.v from the old LF directory to the new PLF directory. (If you’ve been working on it, make sure to use a version that compiles.)

  • Change "LF" in _CoqProject and in the From LF Require line at the top of Imp.v to "PLF".

  • Compile Imp.v and Maps.v.

  • You can now start working on Equiv.v in the new PLF directory (and subsequent files in PLF).

14 Equiv (due mid Nov.)

Complete the following exercises in the Coq file Equiv.v: skip_right, IFB_false, swap_if_branches, WHILE_true, seq_assoc, assign_aequiv, CSeq_congruence, CIf_congruence, fold_constants_com_sound, inequiv_exercise.

Total points available: 75.

The following exercises will not be graded, but I recommend them: equiv_classes, WHILE_false_informal, WHILE_true_nonterm_informal, fold_bexp_BEq_informal, better_subst_equiv.

The optimize_0plus exercise and the earlier exercises in the case study of nondeterminism are not difficult, but you will be tired of doing this kind of work at this point and ready to move on. The same is true of the optional exercises at the end of the file. If you are really motivated, go ahead.

15 Hoare (due late Nov.)

Complete the following exercises in the Coq file Hoare.v: hoare_asgn_fwd, swap_exercise, if_minus_plus.

Total points available: 25.

The following exercises will not be graded, but I recommend them: assertions, triples, valid_triples, hoare_asgn_examples, hoare_asgn_wrong, hoare_asgn_fwd_exists, hoare_asgn_examples_2, hoare_asgn_example4, hoarestate1, if1_hoare, hoare_repeat.

You might consider doing hoare_havoc if you have worked on the nondeterminism material in Equiv.v.

16 Hoare2, HoareAsLogic

These files are left as optional reading and exercises.

17 Smallstep (due Dec. 3)

Complete the following exercises in the Coq file Smallstep.v: test_step_2, redo_determinism, value_not_same_as_normal_form1, value_not_same_as_normal_form2, value_not_same_as_normal_form3, progress_bool, step_deterministic, smallstep_bool_shortcut, test_multistep_2, test_multistep_3, test_multistep_4, normal_forms_unique, multistep_congr_2, eval__multistep, step__eval, multistep__eval, interp_tm, normalize_ex, normalize_ex.

Total points available: 120.

The following exercises will not be graded, but I recommend them: smallstep_bools, properties_of_altered_step, eval__multistep_inf, combined_properties, par_body_n__Sn, par_body_n, compiler_is_correct (requires you to have done the stack compiler exercise from Imp.v).

18 Types (not for credit)

Complete the following exercises in the Coq file Types.v: some_term_is_stuck, value_is_nf, step_deterministic, succ_hastype_nat__hastype_nat, finish_progress, finish_preservation, preservation_alternate_proof, normalize_ex, normalize_ex.

Total points available: about 50.

The following exercises will not be graded, but I recommend them: finish_progress_informal, finish_preservation_informal, subject_expansion. The variation exercises can be useful to strengthen your understanding of the implications of typing rules.

19 Stlc (not for credit)

Complete the following exercises in the Coq file Stlc.v: substi_correct, step_example5, typing_example_2_full, typing_example_3, typing_nonexample_3.

Total points available: about 35.

20 StlcProp

There were no required exercises from the Coq file StlcProp.v in earlier offerings, because this material was only sketched in lecture. I would have required the following: progress_from_term_ind, typable_empty__closed, type_soundness, types_unique, which would have totalled 30 points.

Again, the variations exercises are useful to strengthen intuition, and stlc_arith is a good extended exercise for the enthusiast.