Homework Assignment 4 Interactive Computer Theorem Proving CS2949, Fall 2006 UC Berkeley 
Submit your solution file for this assignment as an attachment
by email 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.
Firstorder 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 and
patternmatching. Your definition shouldn't use any values defined
elsewhere besides 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.