Homework Assignment 0 Interactive Computer Theorem Proving CS2949, 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 command and press the period key.

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 doubledashed 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 doubledashed 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 Cc CRET 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 Cc CRET again with the cursor
positioned anywhere on the line to fastforward to.
Now we're ready to finish the proof. If you haven't already, fastforward 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. 