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

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 :=
  match n with 
    | O => 1
    | S m => n * factorial m
  end.



(** Problem 2

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

Fixpoint is_product_of_some_up_to n m1 m2 :=
  match m2 with
    | O => false
    | S O => false
    | S m2' => orb (beq_nat (m1 * m2) n) (is_product_of_some_up_to n m1 m2')
  end.

Fixpoint divisible_by_some_up_to n m :=
  match m with
    | O => false
    | S O => false
    | S m' => orb (is_product_of_some_up_to n m n) (divisible_by_some_up_to n m')
  end.

Definition primeb (n : nat) : bool :=
  match n with
    | O => false
    | S O => false
    | S m => negb (divisible_by_some_up_to n m)
  end.

(** Problem 3

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) := 
  fun npanq =>
    let (np, nq) := npanq
      in
      fun pvq =>
        match pvq with
          | or_introl p => np p
          | or_intror q => nq q
        end.


(** Problem 4

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) := fun npaq nnpvnq => 
  nnpvnq (or_introl (fun p => nnpvnq (or_intror (fun q => npaq (conj p q))))).


(** Problem 5

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 ->
peirce]. Or you could prove them in another direction. Or you could
choose one and show that it both implies and is implied by the other
two. *)

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

(* The first four probably form the simplest chain. The other eight
implications are below. *)

Definition dne_if_peirce : peirce -> dne := fun peirce P nnp => 
  peirce P False (fun np => ex_falso_quodlibet P (nnp np)).

Definition dml_if_dne : dne -> dml := fun dne P Q n_npanq => 
  dne (P \/ Q) (fun n_poq => n_npanq (conj (fun p => n_poq (or_introl p))
                                           (fun q => n_poq (or_intror q)))).

Definition exm_if_dml : dml -> exm := fun dml P => 
  dml P (~P) (fun npannp => let (np, nnp) := npannp in nnp np).

Definition peirce_if_exm : exm -> peirce := fun exm P Q piq_ip => 
  match exm P with
    | or_introl p => p
    | or_intror np => piq_ip (fun p => ex_falso_quodlibet Q (np p))
  end.


Definition exm_if_dne : dne -> exm := fun dne P => 
  dne (P \/ ~P) 
  (fun n_pvnp => n_pvnp (or_intror (fun p => n_pvnp (or_introl p)))).

Definition dml_if_exm : exm -> dml := fun exm P Q n_npanq => 
  match exm P, exm Q with
    | or_introl p, _ => or_introl p
    | _, or_introl q => or_intror q
    | or_intror np, or_intror nq => 
        ex_falso_quodlibet (P \/ Q) (n_npanq (conj np nq))
  end.

Definition dml_if_exm' : exm -> dml := fun exm P Q n_npanq => 
  match exm (P \/ Q) with
    | or_introl poq => poq
    | or_intror n_poq => 
        ex_falso_quodlibet (P \/ Q) (n_npanq (de_morgan1 P Q n_poq))
  end.

(* This is really just peirce_if_dne and dne_if_dml combined *)
Definition peirce_if_dml : dml -> peirce := fun dml P Q piq_ip => 
  let n_npanp (npanp : ~P /\ ~P) := 
    let (np, _) := npanp in 
      np (piq_ip (fun p => ex_falso_quodlibet Q (np p)))
  in
  match dml P P n_npanp with
    | or_introl p => p
    | or_intror p => p
  end.

(* And this is peirce_if_exm and exm_if_dml combined. Still not too pretty. *)
Definition peirce_if_dml' : dml -> peirce := fun dml P Q piq_ip => 
  let n_npannp (npannp : ~P /\ ~~P) := let (np, nnp) := npannp in nnp np
  in
  match dml P (~P) n_npannp with
    | or_introl p => p
    | or_intror np => piq_ip (fun p => ex_falso_quodlibet Q (np p))
  end.

Definition exm_if_peirce : peirce -> exm := fun peirce P => 
  peirce (P \/ ~P) False 
    (fun n_ponp => or_intror (fun p => n_ponp (or_introl p))).


Definition dne_if_dml : dml -> dne := fun dml P nnp => 
  match dml P P (fun np_a_np => let (np, _) := np_a_np in nnp np) with
    | or_introl p => p
    | or_intror p => p
  end.

Definition peirce_if_dne : dne -> peirce := fun dne P Q piq_ip => 
  dne P (fun np => np (piq_ip (fun p => ex_falso_quodlibet Q (np p)))).

Definition dne_if_exm : exm -> dne := fun exm P nnp => 
  match exm P with
    | or_introl p => p
    | or_intror np => ex_falso_quodlibet P (nnp np)
  end.

Definition dml_if_peirce : peirce -> dml := fun peirce P Q n_npanq =>
  peirce (P \/ Q) False (fun n_poq => 
    ex_falso_quodlibet (P \/ Q) 
    (n_npanq (conj (fun p => n_poq (or_introl p))
                   (fun q => n_poq (or_intror q))))).
                             


(** Problem 6

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

(* What is a property that [a] has and we would like [b] to have? Being
equal to [a]! *)
Definition leq_sym {A} (a b : A) : leq a b -> leq b a := 
  fun (aqb : leq a b) => aqb (fun x => leq x a) (refl_leq a).

(* What is a property that [b] has and we would like [c] to have? That
[a] is equal to it! *)
Definition trans_leq {A} (a b c : A) : leq a b -> leq b c -> leq a c := 
  fun aqb bqc => bqc (fun x => leq a x) aqb.


(** Problem 7

Prove that one is not zero.
*)

(* What is a property that [1] has, but [0] if [0] has it then [False]
can be proven? I.e. a [P] such that [P 1] can be proven, but [P 0]
yields false? Simply the function which assigns [False] to [0], and
e.g. [True] to [1]! *)

Definition one_not_zero : ~(leq (S O) O) := fun oqz =>
  oqz (fun x => match x with O => False | _ => True end) I.