software-foundations

Working my way through the Software Foundations book.

I'm trying to do all of the suggested exercises from this page. Exercises I've done already are crossed off; I might do some others along the way, as well.

Basics:
- ~~factorial~~
- ~~plus_id_exercise~~
- ~~zero_nbeq_plus_1~~
- ~~boolean functions~~
- ~~andb_eq_orb~~
- ~~binary~~
- ~~decreasing~~
Induction:
- ~~basic_induction~~
- ~~plus_comm~~
- ~~mult_comm~~
- ~~evenb_n__oddb_Sn~~
- ~~binary_commute~~
- binary_inverse
Lists:
- bag_functions
- bag_theorem
- list_exercises
- list_design
- bag_count_sum
- rev_injective
Poly:
- split
- map_rev
- fold_length
- fold_map
MoreCoq:
- silly_ex
- rev_exercise1
- beq_nat_0_l.
- plus_n_n_injective
- beq_nat_true
- gen_dep_practice
- combine_split
- override_same
- destruct_eqn_practice
- beq_nat_sym
- beq_nat_trans
- split_combine
- override_permute
Prop:
- gorgeous_sum
- beautiful__gorgeous
- ev_ev__ev
- palindromes
MoreProp:
- total_relation
- empty_relation
- R_provability
- R_fact
- combine_odd_even
Logic:
- True
- contrapositive
- not_exists_dist
- dist_exists_or
- leibniz_equality
- all_forallb
- no_repeats
- pigeonhole principle
ProofObjects:
- double_even_pfobj
- trans_eq_example_redux
Imp:
- optimize_0plus_b
- bevalR
- update_same
- update_permute
- loop_never_stops
- no_whiles_terminating
- stack_compiler
- stack_compiler_correct
Hoare:
- valid_triples
- hoare_asgn_wrong
- hoare_asgn_examples_2
- hoare_asgn_example4
- swap_exercise
- if_minus_plus
- if1_hoare

x1957/software-foundations

software-foundations