# 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).   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 `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
This page has been generated by coqdoc