Homework Assignment 1|
Interactive Computer Theorem Proving
CS294-9, Fall 2006
Submit your solution file for this assignment
by e-mail 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.
Meta-note: 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.
Ltacelimer e := try exact e; let H := fresh "H" in (generalize e; intro H).
Ltactrue_i := elimer I.
Ltacfalse_e Hfalse := destruct Hfalse.
Ltacimp_i := intro.
Ltacimp_e Himp Hant := elimer (Himp Hant).
Ltacand_i := split.
Ltacand_e1 Hand := elimer (proj1 Hand).
Ltacand_e2 Hand := elimer (proj2 Hand).
Ltacor_i1 := left.
Ltacor_i2 := right.
Ltacor_e Hor := destruct Hor.
Ltacnot_i := intro.
Ltacnot_e Hno Hyes := destruct (Hno Hyes).
Ltacforall_i := intro.
Ltacforall_e Hall x := elimer (Hall x).
Ltacexists_i x := exists x.
Ltacexists_e Hex := destruct Hex.
Plus the predefined tactics |
We open a |
We want to prove some theorems about arbitary propositions, so we declare
three propositional variables, scoped within this |
VariablesP 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
off-limits 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
Theoremgrand_challenge_problem : P -> P.
|Truth is true.|
Theoremtruth : True.
|False implies anything|
Theoremcontradiction_P : False -> P.
Theoremand_associates : (P /\ Q) /\ R -> P /\ (Q /\ R).
|Dropping conjuncts preserves truth.|
Theoremcut_out_the_middle_man : P /\ Q /\ R -> P /\ R.
|One or the other is true! Can you figure out which?|
Theoremmake_up_your_mind : True \/ False.
Theoremor_commutes : P \/ Q -> Q \/ P.
Theoremor_associates : (P \/ Q) \/ R -> P \/ (Q \/ R).
|Something is fishy about the hypotheses, so we can deduce anything.|
Theoremsomething_fishy : (P -> Q) -> P -> ~Q -> R.
|The law of contraposition holds only in this direction in constructive logic.|
Theoremcontrapositive : (P -> Q) -> ~Q -> ~P.
We'll prove some theorems that draw their individuals an
unspecified set |
VariableA : Set.
Here's an arbitrary individual in |
Variablee : A.
|Here's a unary function symbol.|
Variablef : A -> A.
|Here are two unary predicate symbols.|
VariablesP P' : A -> Prop.
|Here's a binary predicate symbol.|
VariableQ : A -> A -> Prop.
|Prove the following theorems using only the natural deduction tactics introduced in class:|
Theoremindeed : (forall x : A, P x) -> P (f e).
Theoremofcourse : (forall x : A, P (f x)) -> (exists y : A, P y).
(exists x : A, forall y : A, Q x y)
-> (forall y : A, exists x : A, Q x y).
(forall x : A, ~(P x))
-> ~(exists x : A, P x).
|We can push a conjunction inside universal quantifications.|
Theoremcoalesce1 : (forall x : A, P x) /\ (forall x : A, P' x)
-> (forall x : A, P x /\ P' x).
|We can push a universal quantification inside a conjunction.|
Theoremcoalesce2 : (forall x : A, P x /\ P' x)
-> (forall x : A, P x) /\ (forall x : A, P' x).
|This one doesn't have any deeper meaning. :-)|
(forall x : A, P x -> P' e)
-> ((forall y : A, P' y) \/ (exists z : A, P z))
-> P' e.
|A straightforward fact about equality and functions|
Theoremreverse_congruence : forall x : A, forall y : A,
x = y -> f y = f x.
If the set |
Theoremsmall_world : (exists x : A, forall y : A, x = y)
-> e = f e.
|A complicated theorem about equality and functions|
Theoremnasty : 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.
When you're done, you'll know that your solutions are all correct if there
are no more occurrences of |