Homework Assignment 1 Interactive Computer Theorem Proving CS2949, Fall 2006 UC Berkeley 
Submit your solution file for this assignment
by email with
the subject "ICTP HW1" by the start of class on September 7.
You should write your solutions entirely on your own, since that's the only
way to develop the intuitions needed to do this kind of stuff!
OK, to start, grab the template source file. Metanote: Since this is the first time we're offering a class like this, any feedback you can provide on this and future homework assignments would be very helpful. If something is too hard or too easy, we'd love to hear about it in a comment in your solution file. (Comments are the things bracketed between parentheses and stars.) 
Some useful tactics 
Here is some support code to help you build proofs using the same natural
deduction terminology that we used in class. It's safe to skip over these.
One potential gotcha that's important to remember: For tactics that take arguments, when one of the arguments contains spaces, enclose it in parentheses to avoid scary error messages. 
Ltac
elimer e := try exact e; let H := fresh "H" in (generalize e; intro H).
Ltac
true_i := elimer I.
Ltac
false_e Hfalse := destruct Hfalse.
Ltac
imp_i := intro.
Ltac
imp_e Himp Hant := elimer (Himp Hant).
Ltac
and_i := split.
Ltac
and_e1 Hand := elimer (proj1 Hand).
Ltac
and_e2 Hand := elimer (proj2 Hand).
Ltac
or_i1 := left.
Ltac
or_i2 := right.
Ltac
or_e Hor := destruct Hor.
Ltac
not_i := intro.
Ltac
not_e Hno Hyes := destruct (Hno Hyes).
Ltac
forall_i := intro.
Ltac
forall_e Hall x := elimer (Hall x).
Ltac
exists_i x := exists x.
Ltac
exists_e Hex := destruct Hex.
Plus the predefined tactics assumption , assert , reflexivity ,
and rewrite

Propositional Logic 
We open a , which is a mechanism for controlling the scoping of
variables and assumptions.

Section
propositional.
We want to prove some theorems about arbitary propositions, so we declare
three propositional variables, scoped within this only.

Variables
P Q R : Prop.
OK, here's where the interactive part starts. Prove these simple theorems
in propositional logic. Use a natural deduction style, by way of the tactics
defined in the beginning of this source file. They're the same that we used
in class. Coq has lots of other tactics available, but we'll consider them
offlimits just for this assignment.
Each problem is given in the form:
This essentially states the theorem as an axiom. Your job is to make it a bonafide theorem by replacing Admitted with a proof script and , as
in this example:

Theorem
grand_challenge_problem : P > P.
imp_i.
assumption.
Qed
.
Truth is true. 
Theorem
truth : True.
Admitted.
False implies anything 
Theorem
contradiction_P : False > P.
Admitted.
/\ is associative.

Theorem
and_associates : (P /\ Q) /\ R > P /\ (Q /\ R).
Admitted.
Dropping conjuncts preserves truth. 
Theorem
cut_out_the_middle_man : P /\ Q /\ R > P /\ R.
Admitted.
One or the other is true! Can you figure out which? 
Theorem
make_up_your_mind : True \/ False.
Admitted.
\/ is commutative.

Theorem
or_commutes : P \/ Q > Q \/ P.
Admitted.
\/ is associative.

Theorem
or_associates : (P \/ Q) \/ R > P \/ (Q \/ R).
Admitted.
Something is fishy about the hypotheses, so we can deduce anything. 
Theorem
something_fishy : (P > Q) > P > ~Q > R.
Admitted.
The law of contraposition holds only in this direction in constructive logic. 
Theorem
contrapositive : (P > Q) > ~Q > ~P.
Admitted.
End
propositional.
Firstorder logic 
Section
firstorder.
We'll prove some theorems that draw their individuals an
unspecified set A .

Variable
A : Set.
Here's an arbitrary individual in A .

Variable
e : A.
Here's a unary function symbol. 
Variable
f : A > A.
Here are two unary predicate symbols. 
Variables
P P' : A > Prop.
Here's a binary predicate symbol. 
Variable
Q : A > A > Prop.
Prove the following theorems using only the natural deduction tactics introduced in class: 
If P holds for any value, then it must hold for f e .

Theorem
indeed : (forall x : A, P x) > P (f e).
Admitted.
If P holds for anything f returns, then P holds of something.

Theorem
ofcourse : (forall x : A, P (f x)) > (exists y : A, P y).
Admitted.
Swapping exists and forall in this way is always legal.

Theorem
swap_quantifiers :
(exists x : A, forall y : A, Q x y)
> (forall y : A, exists x : A, Q x y).
Admitted.
If P maps everything to false, then we can't find anything it maps to
true.

Theorem
nobody :
(forall x : A, ~(P x))
> ~(exists x : A, P x).
Admitted.
We can push a conjunction inside universal quantifications. 
Theorem
coalesce1 : (forall x : A, P x) /\ (forall x : A, P' x)
> (forall x : A, P x /\ P' x).
Admitted.
We can push a universal quantification inside a conjunction. 
Theorem
coalesce2 : (forall x : A, P x /\ P' x)
> (forall x : A, P x) /\ (forall x : A, P' x).
Admitted.
This one doesn't have any deeper meaning. :) 
Theorem
one_or_the_other :
(forall x : A, P x > P' e)
> ((forall y : A, P' y) \/ (exists z : A, P z))
> P' e.
Admitted.
A straightforward fact about equality and functions 
Theorem
reverse_congruence : forall x : A, forall y : A,
x = y > f y = f x.
Admitted.
If the set A has only one member, then we can derive a particular
equality.

Theorem
small_world : (exists x : A, forall y : A, x = y)
> e = f e.
Admitted.
A complicated theorem about equality and functions 
Theorem
nasty : forall x : A, forall y : A, forall z : A,
f (f x) = x
> f z = f x
> f y = f z
> f (f (f (f (f x)))) = f y.
Admitted.
End
firstorder.
When you're done, you'll know that your solutions are all correct if there
are no more occurrences of Admitted and you haven't erased any of the
lines that were in the template file.
