(** Homework Assignment 4#<br>#
#<a href="http://www.cs.berkeley.edu/~adamc/itp/">#Interactive Computer Theorem
Proving#</a><br>#
CS294-9, Fall 2006#<br>#
UC Berkeley *)

(** Submit your solution file for this assignment as an attachment
  #<a href="mailto:adamc@cs.berkeley.edu?subject=ICTP HW4">#by e-mail#</a># 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.

  #<a href="HW4.v">#Template source file#</a>#
  *)

(** * 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.