(** Formal Type Theory, Autumn 2009, Exercise set 1

NAME(S) OF SUBMITTER(S):
                        
COMMENTS ON THE EXERCISE:


Send this file (with the problems solved) to ftt09@cs.helsinki.fi by 
2009-11-12 08:00+02
*)

Require Import natbool.
Require Import poly.
Require Import logic.

(** Problem 1 (1 point)

Write a function [factorial : nat -> nat] that calculates the factorial
of its argument, i.e. [factorial n] evaluates to the same as [1 * 2 *
... * n]. Recall that [factorial 0] should be [1]. *)

(*
Fixpoint factorial (n : nat) : nat := 
  ... fill out ... 
*)



(** Problem 2 (2 points)

Write a function [primeb : nat -> bool] so that [primeb n] evaluates to
[true] if and only if [n] is a prime number, i.e. it is divisible only
by itself and by 1. 0 and 1 are not prime numbers. Define whatever
auxiliary functions you need. Initially, you only have the operations
defined in natbool.v available. *)

(* 
Definition primeb (n : nat) : bool := 
  ... fill out ...
*)



(** Problem 3 (1 points)

Prove the other direction of [de_morgan1] by filling out the following
definition. This is a proof, so the only requirement is that your
function has the correct type. *)
   
(*
Definition de_morgan1rev P Q : ~P /\ ~Q -> ~(P \/ Q) := 
  ... fill out ... 
*)



(** Problem 4 (2 points)

The reverse direction of [de_morgan2] is not provable constructively.
However, a slight variant of it is: we add a double negation to the
result type. Prove this.
*)

(*
Definition de_morgan2rev' P Q : ~(P /\ Q) -> ~~(~P \/ ~Q) :=
  ... fill out ...
*)


(** Problem 5 (3 points)

Coq can be made to support classical logic by adding a suitable axiom,
i.e. assuming that we have a term of a certain type even though we
cannot construct one. There are several possible choices for such an
axiom, and some of them are listed below. Prove that these are all
equivalent by proving enough implications between them so that one could
derive any one from the other by chaining the implications. For
instance, you could prove [peirce -> dne], [dne -> exm], [exm -> dml]
and [dml -> peirce]. Or you could prove them in another direction, or
chain them altogether differently. *)

(* Peirce's law *)
Definition peirce := forall P Q : Prop, ((P -> Q) -> P) -> P.
(* Double negation elimination *)
Definition dne := forall P : Prop,  ~~P -> P.
(* Excluded middle *)
Definition exm := forall  P : Prop,  P \/ ~P.
(* The missing De Morgan's law *)
Definition dml := forall P Q : Prop, ~(~P /\ ~Q) -> P \/ Q.

(* Provide your definitions here, e.g 

Definition dne_if_peirce : peirce -> dne := ... fill out ...
etc.
*)


(** Problem 6 (1 points)

Intuitively, [a] and [b] would be equal if for every property [P] we
would have [P a <-> P b]. Instead, we defined [leq] simply as a
unidirectional implication. Show that we can derive the other direction
of the implication by proving the symmetry of [leq].

Also prove the transitivity of [leq].
*)

(*
Definition sym_leq {A} (a b : A) : leq a b -> leq b a := 
  ... fill out ... 
*)

(* 
Definition trans_leq {A} (a b c : A) (aqb : leq a b) (bqc : leq b c) : leq a c := 
  ... fill out ... 
*)


(** Problem 7 (2 points)

Prove that one is not zero.
*)

(* 
Definition one_not_zero : ~(leq (S O) O) :=
  ... fill out ... 
*)