|
Homework Assignment 0 Interactive Computer Theorem Proving CS294-9, Fall 2006 UC Berkeley |
Installing Coq |
This section deals with getting Coq, the main tool we'll use in this class,
up and running.
|
The Proof General Emacs mode |
|
Inductive list : Set :=
| nil : list
| cons : nat -> list -> list.
| Do the same for this recursive definition of a list append function. |
Fixpoint append (ls1 ls2 : list) {struct ls1} : list :=
match ls1 with
| nil => ls2
| cons x ls1' => cons x (append ls1' ls2)
end.
Now let's prove that append is associative. Move the cursor after the
period in the following |
Theorem append_associative : forall ls1 ls2 ls3,
append (append ls1 ls2) ls3 = append ls1 (append ls2 ls3).
In the other buffer, you should see a representation of the initial proof
state. The formula we want to prove is displayed below a double-dashed line.
We need to specify tactics to direct Coq in performing the proof.
Hit the period key at the end of the next line to send the first batch of
instructions, which say that we want to proceed by induction on the first
quantified argument ls1.
|
induction ls1; simpl; intros.
You should now see two subgoals displayed in the other buffer; one for the
base (nil) case of the proof and one for the inductive (cons) case. Now
we have some named variables appearing above the double-dashed line. Their
presence tells us that we need to prove the formula for any values
of those variables. You can probably see that the formula in this case is
obviously true, so advance the proof by hitting period at the end of the next
line.
|
trivial.
|
In a less trivial case, we might have made a mistake and wish to back up.
Position the cursor at the start of the previous proof line and
press C-c C-RET to undo the proof interaction back to that point. After
undoing, you can advance forward again by hitting the period key at the end of
the line you want to return to, or by using C-c C-RET again with the cursor
positioned anywhere on the line to fast-forward to.
Now we're ready to finish the proof. If you haven't already, fast-forward the proof state back to directly after the lone trivial tactic. This leaves us
with the task of giving the inductive step of the proof.
We have our most complicated proof state yet. Not only are there variables of types nat and list above the double line, but we also have a logical
assumption IHls1 that expresses the induction hypothesis. We can finish the
proof by rewriting the goal using the IH's quantified equality:
|
rewrite IHls1; trivial.
| Finally, we add this named theorem to the environment: |
Qed.
Print append_associative.
| And that's that. There's no need to "turn in" this assignment, but definitely let me know if you run into any problems getting this basic interaction to work. |