5 Problem Sets

Each chapter of Logical Foundations and Programming Language Foundations contains associated exercises. Problem sets will typically be some subset of these exercises. For more information on the exercises see:

https://softwarefoundations.cis.upenn.edu/draft/lf-current/Preface.html#lab10.

We are maintaining a GitHub repository which is where you will find files for the problem sets. You can find it here:

https://github.com/plum-umd/cmsc631-hws

Simply clone this repository and modify the specified Coq source files to complete the problem sets.

5.1 #1: Basics and Induction

Due 09/05/2017

Basics.v: Do all 1-star exercises, as well as mult_S_1, andb_true_elim2, boolean_functions, and binary.

Induction.v: Do all 1-star exercises, as well as basic_induction, double_plus, mult_comm, more_exercises (only leb_refl, zero_nbeq_S, and andb_false_r), and binary_commute.

For the binary_commute exercise, please use the following signature for the bin_to_nat_pres_incr theorem:

Theorem bin_to_nat_pres_incr : forall (b : bin),

bin_to_nat (incr b) = 1 + bin_to_nat b.

5.2 #2: Lists and Poly

Due 09/12/2017

Lists.v: snd_fst_is_swap, fst_swap_is_snd, list_funs, bag_functions, list_exercises, beq_natlist, beq_id_refl, update_eq, and update_neq.

Poly.v: poly_exercises, more_poly_exercises, split, hd_error_poly, and flat_map.

5.3 #3: Tactics and Logic

Due 09/19/2017

Tactics.v: apply_exercise1, apply_with_exercise, plus_n_n_injective, beq_nat_true, gen_dep_practice, destruct_eqn_practice, beq_nat_sym

Logic.v: and_exercise, and_assoc, mult_eq_0, or_commut, contrapositive, not_both_true_and_false, iff_properties, or_distributes_over_and, dist_not_exists, dist_exists_or, In_map_iff, All, logical_connectives

5.4 #4: IndProp and Maps

Due 09/26/2017

IndProp.v: ev_double, inversion_practice, ev_sum, ev_ev__ev, le_exercises (only le_trans, le_plus_l, and leb_correct), exp_match_ex1, reflect_iff

Maps.v: t_update_eq, t_update_neq, t_update_shadow, beq_idP, t_update_same

5.5 #5: Imp and Equiv

Due 10/05/2017

Imp.v: optimize_0plus_b, ceval_example2, loop_never_stops, stack_compiler

For extra credit you may do stack_compiler_correct

Equiv.v: equiv_classes, skip_right, IFB_false, WHILE_true, CIf_congruence

5.6 #6: Hoare and Hoare2

Due 10/13/2017

Hoare.v: hoare_asgn_examples, hoare_asgn_examples_2, hoare_asgn_example4, swap_exercise, if_minus_plus

For extra credit you may do hoare_repeat

Hoare2.v: parity_formal, is_wp_formal, hoare_asgn_weakest

5.7 #7: Smallstep

Due 10/20/2017

Smallstep.v: redo_determinism, progress_bool, multistep_congr_2, step__eval, multistep__eval

5.8 #8: Types and STLC

Due 10/31/2017

Types.v: some_term_is_stuck, value_is_nf, finish_preservation, subject_expansion, normalize_ex

For extra credit you may do finish_progress

Stlc.v: step_example5, typing_example_2_full

5.9 #9: StlcProp, MoreStlc, and Typechecking

Due 11/16/2017

StlcProp.v: progress_from_term_ind, typable_empty__closed, type_soundness

Sub.v: sub_inversion_Bool, sub_inversion_arrow, canonical_forms_of_arrow_types

NOTE: Contrary to what the text in Sub says, please do not modify the language. Simply complete the exercises on the language as it exists. In particular, do not add products to the language. This will cause your submission not to compile on the submit server.

ProofObjects.v: eight_is_even, conj_fact, or_commut’’, leibniz_equality