|
Homework Assignment 4 Interactive Computer Theorem Proving CS294-9, Fall 2006 UC Berkeley |
|
Submit your solution file for this assignment as an attachment
by e-mail with
the subject "ICTP HW4" by the start of class on September 28.
You should write your solutions entirely on your own, which includes not
consulting any solutions to these problems that may be posted on the web.
Template source file |
Proof terms |
| Fill in a proof term for each theorem stated below. You should resist the urge to use tactic based proving to find the proof terms, since that defeats the purpose of these exercises! |
Propositional logic |
Section propositional.
Variables P Q R : Prop.
Here's an example of what a solution should look like. You should remove
the Admitted and add an explicit proof term.
|
Definition example : P -> P :=
fun p : P => p.
Definition term1 : (P -> Q -> R) -> (Q -> P -> R).
Admitted.
Definition term2 : P /\ Q -> R \/ P.
Admitted.
Definition term3 : P \/ Q -> (Q -> P) -> P.
Admitted.
Definition term4 : P -> ~~P.
Admitted.
End propositional.
First-order logic |
Section firstorder.
Variable A : Set.
Variable Q : A -> A -> Prop.
Definition swap_quantifiers :
(forall (x : A) (y : A), Q x y)
-> (forall (y : A) (x : A), Q x y).
Admitted.
Definition swap_quantifiers2 :
(exists x : A, forall y : A, Q x y)
-> (forall y : A, exists x : A, Q x y).
Admitted.
Definition eq_transitive :
forall (x y z : A),
x = y
-> y = z
-> x = z.
Admitted.
End firstorder.
Induction principles |
| In this section, you'll derive some induction principles manually using recursive functions. |
Section my_nat_ind.
Variable P : nat -> Prop.
Variable base : P O.
Variable ind : forall n, P n -> P (S n).
Give an alternate definition of nat_ind using only nat and its constructors.
|
Parameter my_nat_ind : forall (n : nat), P n.
End my_nat_ind.
Require Import List.
Section my_list_ind.
Variable A : Set.
Variable P : list A -> Prop.
Variable base : P nil.
Variable ind : forall x ls, P ls -> P (x :: ls).
Give an alternate definition of list_ind following the same guidelines
as for the last part (except, of course, that this time it's only list
and its constructors that you can refer to).
|
Parameter my_list_ind : forall (ls : list A), P ls.
End my_list_ind.