Library HW4

 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).

Definition term2 : P /\ Q -> R \/ P.

Definition term3 : P \/ Q -> (Q -> P) -> P.

Definition term4 : P -> ~~P.
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).

Definition swap_quantifiers2 :
(exists x : A, forall y : A, Q x y)
-> (forall y : A, exists x : A, Q x y).

Definition eq_transitive :
forall (x y z : A),
x = y
-> y = z
-> x = z.
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 Fixpoint and pattern-matching. 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.

Index