CS195X: Software Foundations

About the Course

As developers, how do we convince ourselves that the programs we write
are correct?  What does “correctness” even mean, particularly at
the ouset of designing a program?  Depending on the correctness
notion, does it suffice to test random inputs, or is the property
sufficiently crucial that we want authoritative proof that it holds?
And as programs evolve, how can we reuse any certification effort to
verify the new versions of our programs?

In this course, we will focus on correctness properties for
*programming languages*, and examine in detail two techniques
for verifying those properties.  One approach (Redex) allows for quick
exploration and random testing, while the other (Coq) allows for
computer-verified proof.  This course will provide a technical guide
to using these two tools, leading up to non-trivial projects in both.
The prerequisite for this course is CSCI 1730.

Course Management

We are going to use the cs195x.2012-13.s mailing list. Go to 
lists.cs.brown.edu and subscribe to the list.

Instructor:   Ben Lerner
Office hours: Wednesday, 1-3pm, or by appointment

Course textbook

We are using the Software Foundations textbook
by Pierce et al.  I will be posting chapters from this book
incrementally on this course site; the full book is freely available
should you want to read ahead.

Using Course Software

The standard versions of course software are Coq 8.4pl1 (if you
install it on OS X, the latest version is simply 8.4) and DrRacket
5.3.  If you are using the i-lab machines, Coq is installed in the
course directory.  To use it with emacs, add the following line to
your .emacs file:

(load-file "/course/cs195x/share/emacs/site-lisp/pg-setup.el")

You can also use coqide, in /course/cs195x/bin. Note: there is
an installation of Coq 8.2pl2 in /usr/bin.  Due to tstaff policy, by
default course directories do not take precedence over system ones in
your path, so merely typing "coqide" will run the wrong
version.  Version 8.4 is almost backwards-compatible with
earlier versions, but some proofs require small changes to work.  Be
sure you use the course version!

DrRacket is installed in /pro/plt/software/racket/5.3/, and if you are
a member of the cs195xstudent group, then by default it should be in
your path.  Email me to confirm you are in the course, and I will add
you to the student group if you aren't already in it.

Lecture notes and assignments

Date	Lecture notes	Assignment
1/23/13	Basics_inclass	Due 1/28: Basics.v
1/25/13	More practice with Basics_inclass	Due 1/30: Lists.v
1/28/13	Lists	No homework assigned
1/30/13	Polymorphism	Due 2/4: hw3.v and the Cases support library
2/1/13	More information on Coq	No homework assigned
2/4/13	Inductive propositions, part 1	Due 2/11: Hw4, part 1: Exercises in Prop-part1.v (and the Cases support library)
2/6/13	Inductive propositions, and More on inductive propositions	Due 2/11: Hw4, part 2: selection of exercises in MoreProp: `ex_set`, `tree`, `mytype`, `foo`, `p_provability`, and `no_longer_than_ind`.
2/8/13	Snow day; no class
2/11/13	Logic	Due 2/15: Hw5.v and the MIU puzzle
2/13/13	More in Logic	Worked examples in Logic.v
2/15/13	More about Logic	Worked examples, even/odd induction, strong induction principles
2/18/13	Presidents' Day; no class
2/20/13	Introduction to IMP. Also, the SfLib support library	Finish the proof of correctness for `optimize_0plus`, construct a similar optimization for `bexp`s that uses `optimize_0plus`, define a similar correctness claim, and prove your optimization sound.
2/22/13	More IMP: state, identifiers, subtleties of equivalence on states	No assignment
2/25/13	IMP Commands	Due 3/1: Hw 6: Imp.v. Prove update_example, update_shadow, update_permute, pup_to_n, pup_to_2_ceval, loop_never_stops, no_whilesR, no_whiles_eqv; define s_execute, s_compile, and prove s_compile_correct. Three hints for s_compile_correct: You'll need to generalize-dependent something that is not obvious, to get a strong enough inductive hypothesis. You'll likely need to prove a lemma about how evaluation commutes with stack-concatenation. And, you'll need to think carefully about the error cases in s_execute, or else that lemma (and/or the final proof for s_compile_correct) won't go through.
2/27/13	Equivalences in IMP	For Friday, work through IFB_false, swap_if_branches, and WHILE_true. Why do you need WHILE_true_nonterm as its own lemma? You do not need to hand these in.
3/1/13	Binary relations and Small-step semantics	Due 3/6: Hw 7, part 1: Proving equivalence between fixpoint, big-step-with-numbers, big-step-with-terms, small-step-with-constants, and small-step-with-value formulations of the Numbers+Plus language. (Support file: Rel.v)
3/4/13	The rest of small-step semantics	Due 3/6: Hw 7, part 2: Defining and using evaluation contexts for IMP
3/6/13	No lecture notes; review of techniques and Q&A	Hw 7 is extended until 3/8
3/8/13	Types for a simple numbers-and-booleans language	Recommended for Monday: finish the proofs of Progress and Preservation in Types.v for this language
3/11/13	The simply-typed lambda calculus
3/13/13	The simply-typed lambda calculus: building towards preservation

Coq Cheat Sheet

Keeping the tactics and incidental commands of Coq straight is
challenging.  The full documentation can be found here.
Here's a quick-reference for the commands we've encountered so far:

Command	Description
Theorem, Lemma, Example, Goal	The main structuring elements of Coq. Typical syntax is `Theorem theoremName : statement of theorem. Proof. proof statements... Qed.` `Goal` is the same, but has no name (or opening colon). Don't forget the periods!
`tactic1 ; tactic2`	Used to sequence tactics: run `tactic1`, then run `tactic2` in every subgoal generated by `tactic1`
`tacticA ; [ tactic1 \| ... \| tacticN ]`	The more general form of sequencing. Run `tacticA`, then run `tactici` in the i^th generated subgoal. This will produce an error if there aren't exactly N subgoals.
`repeat tactic`	Runs `tactic` zero or more times, until it fails. Be careful; if the tactic always succeeds, repeat will never terminate.
`solve tactic` or `solve [tac1 \| ... \| tacN]`	Tries to completely solve the current goal using (one of) the supplied tactic(s). If it can't, then the tactic as a whole fails.
`try tactic`	Tries `tactic`, and if it doesn't succeed, does nothing to the goal. This is particularly useful in combination with solve: `try solve [simpl; auto]` will simplify the goal and solve it, or else do nothing. `try T` is equivalent to `first [T \| idtac]`.
`first [tac1 \| ... \| tacN]`	Tries applying `tac1`, and if it fails, moves on to the next one. If any tactic succeeds, the whole tactic succeeds; if none do, the whole tactic fails.
`idtac` and `fail`	The no-op tactic that always succeeds, and the no-op tactic that always fails. These are useful when writing your own tactics, and rather useless otherwise.
`auto`, `auto ##`, or `auto with HintDatabase`	Attempts to solve the goal using a limited amount of intros, reflexivity, assumptions, and applications. See UseAuto for more details.
`omega`	Solves arithmetic goals that rely only on addition/subtraction, multiplication by constants, (in-)equalities, and logical operators (and/or/implies/not), or states that they are false. It's not available by default; `Require Import Omega.` to use it.
`simpl`	Simplifies the expression as much as possible: applies functions to their arguments, executes match statements when possible, and then tries to simplify functions calls some more. Variants: `simpl in H` tries to simplify the hypothesis named H, and `simpl in *` tries simplifying everywhere. `simpl expr` will only simplify the named function, rather than the entire expression.
`reflexivity`	Solves a goal of the form `foo=foo`. It will try simplifying first, so for instance it can solve `1+5 = 2+4`
`assumption`	Solves a goal if there's any assumption that is exactly equal to the goal (after simplification)
`intros` or `intros nameA nameB ... nameC`	Introduces a premise of the goal into the context, either with a generated name or with the ones supplied by the programmer. If no names are provided, it will introduce as many premises as possible -- so be careful that it does not introduce more than are wanted! If only one name is wanted, use the singular `intro` instead. The effect of `intros` typically takes two forms: Applying `intro H` to a goal of the form `A -> B` yields `H : A ===== B` Applying `intros` to a goal of the form `forall (x : T), P` yields `x : T ===== P`
`apply expr` or `apply expr with (var := expr)`	Applying a hypothesis `H : A -> B` to a goal of the form `B` changes the goal to `A`: since `H` says that A implies B, then if we could only prove A, we could use H to derive B. This is a form of backward reasoning from goals to givens. On the other hand, we can apply H to a hypothesis of the form `a : A` to obtain a `B` hypothesis: this is a form of forward reasoning, from givens to goals. If the hypothesis being used contains variables that cannot be inferred from the goal, then you need to specify `with (var:=value)` to tell Coq what values to use. For instance, `lt_trans : forall p q r, p < q -> q < r -> p < r` can't be used without specifying a value for `q`, since it is not mentioned in the conclusion.
`eapply expr`	Much like `apply`, but allows you to leave out variables that Coq can't guess. Instead, Coq will create existential variables, written `?1234` (or some other number), which you must eventually instantiate before the end of the proof. This approach is particularly useful when the variables to be guessed can be inferred, just not at the current point of the proof.
`exists expr`	Used to solve a goal of the form `exists x, P` by supplying the particular `x` for which you can prove `P`
`Inductive` definitions	Defines new inductive data types. These can get quite elaborate, but the simplest examples roughly match intuition from data type declarations in ML or Haskell. See the definitions of `bool` and `nat` in Basics, and `natlist` and `list` in Lists
`remember expr as var`	Creates a new variable named `var` and an equation `Heqvar : var = expr`. It also automatically replaces `expr` with `var` everwhere it can. This technique is useful when you need to keep a subexpression around, to do case analysis on it later. (But see the second form of `destruct`, below.)
`destruct expr`	Given an expression whose type is inductive, split the current goal into several subgoals, one for each constructor of the inductive type. In each one, substitute the appropriate constructor in place of the given expression. (Note: most often, you want to destruct a single variable, but it could be useful to destruct entire expressions.) So for example, `destruct`ing a boolean value will result in two subgoals, where that value is turned into `true` and `false` respectively. Destructing a list value `l` will result in two cases: one for `nil`, and one with two new variables `a` and `l0` such that `l = a :: l0`. Variants: `destruct expr as [ name1 name2 \| name3 name4 name5 ... \| ... ]` destructs the expression and introduces any new hypotheses using the supplied names.
`destruct expr eqn:Name`	Much like `destruct` above, except it remembers the expression being destructed, and creates a new hypothesis `Name : expr = value`, where `value` is one of the possible destructed values. For example, `destruct (beq_nat x y) eqn:Exy` will produce two subgoals, with `Exy : beq_nat x y = true` in the first and `Exy : beq_nat x y = false` in the second. This is almost the same thing as `remember expr as v; destruct v`, except the equation is named differently and is symmetric from the version produced by remember/destruct: the destructed value is on the right, rather than on the left.
`split`	Useful for splitting a conjunction or an iff into its two components. Can be used in the goal or in hypotheses.
`left`, `right`	Useful for picking one branch out of a disjunction in the goal. CANNOT be used in a hypothesis, because we cannot know which branch was used in building the disjunction. Equivalent to applying `or_introl` and `or_intror`.
`generalize dependent expr`	Takes an expression expr in the context and generalizes it into a forall-quantified variable in the goal, along with every hypothesis in the context that mentioned the expression. Useful for undoing over-eager introduction of variables, and for strengthening the goal in preparation for an inductive proof.
`specialize H with expr`	The "inverse" of generalize; this takes a forall-quantified hypothesis and instantiates it at a specific value. This has the unfortunate side effect of destroying the original forall-quantified hypothesis, so frequently you'll want to write `assert (S := H); specialize S with expr` to copy `H` to a new hypothesis that you can then specialize independently.
`induction expr`	Like `destruct`, this tries to prove the current goal by splitting it into one subgoal per constructor for the inductive data type. Unlike `destruct`, you get inductive hypotheses that let you assume the current goal for structurally-smaller instances of the expression. See any of the examples of induction on numbers or lists, for an intuition of how this works. We'll see more precise details later.
`rewrite H` or `rewrite <- H`	Given a hypothesis `H : foo = bar`, saying `rewrite H` will replace all occurrences of foo with bar in the current goal. If you want to replace bar with foo, use the `rewrite <- H` form. Variants: `rewrite H in H'` tries to rewrite the hypothesis `H'`, and `rewrite H in ` tries to rewrite everywhere possible. `rewrite H at n` tries to rewrite the n^th* occurrence of foo in the goal. You can combine these variants in the obvious ways.
`replace e1 with e2` or `replace e1 with e2 by tactic`	Replaces the first expression with the second, and generates a new goal to prove `e1 = e2`. If you supply `by tactic`, then it tries to prove that equality goal with the given tactic. (Note that the tactic could be the general form of a branching sequence of tactics, provided you parenthesize the whole thing.) You can also replace values `in H`ypotheses.
`change e1 with e2`	Much like `replace`, except Coq tries to prove the replacement equality automatically. You can apply this in the goal or in hypotheses.
`subst` or `subst v`	Looks for all equations of the form `var = value` or `value = var`, rewrites them and eliminates `var`. If you supply a variable `v`, it only rewrites equations involving that variable. The tactic will fail if you have equations that mention the variable on both sides (e.g., `a = 2 * a`)
`Notation "x ++ y" : (app x y) (at level N, left associativity) : list_scope.`	`Notation`s let you extend the grammar of Coq with syntactic sugar. Alphanumeric things in the notation string are treated as variables (which can be arbitrary expressions); the expression after the first colon uses those variables to define what the notation means. The level declaration defines precedence levels, and the notation can have left, right or no associativity. Finally, the scope at the end acts as a namespace, so that different notations can be turned on or off as needed. You won't have to write many notations yourself in this course.
`Locate "_ ++ _".`	Used find out where and how a notation is defined. The underscores are wildcards, so you don't have to know in advance the variable names used in the notation declaration.
`Check expr.`	Used to find out the type of the expression.