Homework is generally due at 11pm PT on Sundays.

Due date | Files |
---|---|

09-05 | `Day01_intro.v` and `Day02_types.v` due at 11pm PT |

09-12 | `Day03_recursion.v` and `Day04_structures.v` due at 11pm PT |

09-19 | `Day05_lists.v` and `Day06_sorting.v` due at 11pm PT |

09-26 | `Day07_trees.v` and `Day08_sets.v` due at 11pm PT |

10-03 | `Day09_levenshtein.v` and `Day10_expressions.v` due at 11pm PT. First exam due 10-08 at 11:59pm PT. |

10-10 | `Day11_propositions.v` and `Day12_cases.v` due at 11pm PT |

10-17 | `Day13_induction.v` and `Day14_exists.v` due at 11pm PT |

10-24 | `Day15_induction2.v` due at 11pm PT |

10-31 | `Day16_indprop.v` and `Day17_indprop2.v` due at 11pm PT |

11-07 | `Day18_sorting.v` and `Day19_levenshtein.v` at 11pm PT |

11-14 | `Day20_latex.tex` and `Day21_translating.tex` and second exam due at 11pm PT |

11-21 | `Day22_sorting.tex` and `Day23_combo.tex` due at 11pm PT |

12-05 (!) | `Day24_sets.tex` due at 11pm PT. Any submissions before 11/29 will be graded before 12/02. |

12-05 | `Day25_relations.tex` and `Day26_countability.tex` due at 11pm PT |

12-12 | `Day27_graphs.tex` and third exam due at 11pm PT |

12-14 | Final exam slot, retakes |

Feel free to look at various chapters ahead of time, but know that we may change assignments up until a week before the due date!

Worksheets are not for credit; they are excellent practice, though, and they resemble the kinds of problems we like to set on exams.

Guides are meant to give you an overview of proof techniques or how to prepare for an upcoming test.

Office hours and mentor sessions are in the same Zoom room. The password is available on Slack.

All times are in Pacific Time. Look in `#csci-054-po`

on Slack for Zoom info. Look for more times to be announced after Tuesday 09/07.

Sunday | Monday | Tuesday | Wednesday | Thursday | Friday | Saturday |
---|---|---|---|---|---|---|

Summer 07:30pm--09:30pm | Prof Osborn 02:00pm--04:00pm | Prof Osborn 09:00--11:00 | Guy 09:00--11:00 | |||

LC 1 (Summer) 09:00--11:00 | LC 4 (Guy) 05:30pm--07:30pm | Chloe 11:00--1:00 | Lucas & David 06:00pm--08:00pm | |||

LC 2 (Eryn) 11:00-01:00pm | Eryn 05:00pm--07:00pm | LC 5 (Lucas) 03:00pm--05:00pm | ||||

LC 3 (Chloe) 01:00pm--02:00pm | LC 6 (David) 03:00pm--05:00pm |

Please see the syllabus for general course information. The course has three parts: programming, formal proof, and paper proof.

Day | Date | File | Plan |
---|---|---|---|

01 | 08-31 | Day01_intro | Coq, Emacs, how to read the book; boolean operations, truth tables, and DNA bases |

02 | 09-02 | Day02_types | numbers and recursive functions |

03 | 09-07 | Day03_recursion | more recursive functions |

04 | 09-09 | Day04_structures | pairs, options, lists, and trees |

05 | 09-14 | Day05_lists | list processing |

06 | 09-16 | Day06_sorting | insertion sort |

07 | 09-21 | Day07_trees | binary search trees |

08 | 09-23 | Day08_sets | list and tree representations of sets |

09 | 09-28 | Day09_levenshtein | the Levenshtein algorithm for edit distance |

10 | 09-30 | Day10_expressions | expressions and interpreters |

At this point, we'll have our first exam on gradescope, about programming.

Day | Date | File | Plan |
---|---|---|---|

11 | 10-05 | Day11_propositions | basic formal proof; Coq tactics; equality and logical propositions |

12 | 10-07 | Day12_cases | proofs by case analysis |

13 | 10-12 | Day13_induction | induction |

14 | 10-14 | Day14_exists | existential quantification |

15 | 10-21 | Day15_induction2 | induction on other structures |

16 | 10-26 | Day16_indprop | inductive propositions |

17 | 10-28 | Day17_indprop2 | inductive propositions, continued |

18 | 11-02 | Day18_sorting | permutations and sorting |

19 | 11-04 | Day19_levenshtein | proving the Levenshtein algorithm correct and optimal |

At this point, we'll have our second exam on gradescope, about formal proof.

Day | Date | File | Plan |
---|---|---|---|

20 | 11-09 | Day20_latex | mathematical typesetting in LaTeX |

21 | 11-11 | Day21_translating | translating formal proofs to paper |

22 | 11-16 | Day22_sorting | sort, informally |

23 | 11-18 | Day23_combinatorics | counting; sum rule, product rule, division rule, permutation, choose |

24 | 11-23 | Day24_sets | set theory |

25 | 11-30 | Day25_relations | relations and functions |

26 | 12-02 | Day26_countability | cardinality and (un)countability |

27 | 12-07 | Day27_graphs | graphs and paths and trees |

The third exam (on informal proof) is due the Sunday after the last week of classes (12/12). Grades will be distributed by the morning of 12/14.

Retakes of exam sections will take place during our final exam slot (14:00--17:00 PT, Tuesday December 14th), in-person but laptops allowed.

We're using Coq 8.12.2, Emacs 27.2 (macOS, Windows, on Linux see your package manager), and Proof General.

To configure your emacs, you'll want to download our init.el and install it to the appropriate location:

- On Mac OS/Linux: Put
`init.el`

in a folder in your home directory called`.emacs.d`

(the leading dot is important!), and be sure you have*no*file called`.emacs`

in your home directory. This is easiest in the terminal (`rm ~/.emacs ; mkdir -p ~/.emacs.d ; mv ~/Downloads/init.el ~/.emacs.d`

). - On Windows: Put
`init.el`

in a folder called`.emacs.d`

(the leading dot is important!) in`C:\Users\YOUR_USERNAME\AppData\Roaming\`

.

We’ll be using an experimental new volume of Software Foundations, which we're calling for now Discrete Math in Coq. Name suggestions are welcome!