(*** Introduction to Computational Logic, Coq part of Assignment 9 ***)
(***
Use Coq to complete the file below.  
If you have any questions, please use the discussion board.
http://www.ps.uni-saarland.de/courses/cl-ss11/forum/
***)

(*** A lemma analagous to Exercise 1 ***)
Lemma bool_dis : 
false <> true.
Proof.  pose (foo (x : bool) :=  if x then True else False).
intros e. change (foo false). rewrite e. exact I. Qed.
Print bool_dis.

(*** Exercise 1 ***)
Lemma nat_dis (x : nat) :
S x <> O.
(*** INSERT PROOF SCRIPT (using pose, change and rewrite) ***)

Lemma nat_dis' (x : nat) :
S x <> O.
(*** INSERT PROOF SCRIPT (using discriminate) ***)

(*** Here are two helpful functions you should know ab0ut. 
     Maybe you should temporarily set 'Display all low-level contents'
     before executing the following two prints. ***)
Print fst.
Print snd.

(*** Exercise 2 ***)
Lemma pair_injective (X Y : Type) (x x' : X) (y y' : Y) :
pair x y = pair x' y' -> x = x' /\ y = y'.
(*** INSERT PROOF SCRIPT (using f_equal) ***)

Lemma pair_injective' (X Y : Type) (x x' : X) (y y' : Y) :
pair x y = pair x' y' -> x = x' /\ y = y'.
(*** INSERT PROOF SCRIPT (using injection) ***)

(*** Exercise 3 ***)
Lemma bool_neq_nat : 
bool <> nat.
(*** INSERT PROOF SCRIPT ***)

(*** Exercise 4 ***)
Lemma Kaminski2 (f g : bool -> bool) (x : bool) :
f (f (f (g x))) = f (g (g (g x))).
(*** INSERT PROOF SCRIPT ***)

(*** nat_E, nat_Ep (natural induction) and nat_pr (primitive recursion) ***)
Definition nat_E :=
fun p u v => fix f x := 
match x as y return p y with 
| O => u 
| S x' => v x' (f x') 
end.

Definition nat_Ep (p : nat -> Prop) : 
p O -> (forall x, p x -> p (S x)) -> forall x, p x
:= nat_E p.

Definition nat_pr {X : Type} : X -> (nat -> X -> X) -> nat -> X :=
fun u v => 
fix f x := match x with 
| O => u 
| S x' => v x' (f x') 
end.

(*** Exercise 5 ***)
Lemma S_neq (x : nat) :  
S x <> x.
(*** INSERT PROOF SCRIPT (using the induction tactic) ***)

Lemma S_neq' (x : nat) :  
S x <> x.
(*** INSERT PROOF SCRIPT (using nat_Ep) ***)

Lemma S_neq'' :  
forall x:nat, S x <> x.
(*** INSERT PROOF SCRIPT (using the fix tactic) ***)

(*** even ***)
Fixpoint even (n : nat) : bool :=
match n with
| 0 => true
| 1 => false
| S (S n) => even n
end.

(*** Exercise 6 ***)
Lemma even_negb (n : nat) :
even n = negb (even (S n)).
(*** INSERT PROOF SCRIPT (using the induction tactic) ***)

(*** Exercise 7 ***)
Definition fac := nat_pr (*** COMPLETE THIS DEFINITION ***)
Compute fac 5.
Lemma fac_correct (x : nat) :
(*** COMPLETE THIS PROPOSITION ***)
(*** INSERT PROOF SCRIPT ***)

(*** AF and K ***)
Fixpoint AF (n : nat) : Type := match n with
| O => nat
| S n' => nat -> AF n'
end.

Fixpoint K (c n : nat) : AF n := 
match n as z return AF z with
| O => c
| S n' => fun _ => K c n'
end.

(*** Exercise 8 ***)
Definition K' (c : nat) : forall n:nat, AF n :=
nat_E (*** COMPLETE THIS DEFINITION ***)

Lemma K_K'_5 (c : nat) : K c 5 = K' c 5.
reflexivity. Qed.

Lemma K_K'_7 (c : nat) : K c 7 = K' c 7.
reflexivity. Qed.

(*** Exercise 9 ***)
Fixpoint P (n k : nat) : AF n := 
(*** INSERT THIS DEFINITION ***)

Lemma P_correct n k x :
P 0 k = k /\
P (S n) 0 x = K x n  /\
P (S n) (S k) x = P n k.
(*** INSERT PROOF SCRIPT ***)

Eval cbv in P 4 2. 

(*** sur, strong, Generalized Cantor ***)
Definition surjective {X Y : Type} (f : X -> Y) : Prop :=
forall y, exists x, f x = y.

Definition sur (X Y : Type) : Prop :=
exists f : X -> Y, surjective f.

Definition countable (X : Type) : Prop :=
sur nat X.

Definition strong (X : Type) : Prop :=
exists f : X -> X, forall x, f x <> x.

Lemma Cantor_generalized (X Y : Type) :
strong Y -> ~sur X (X -> Y).
Proof. intros [neg N] [f A]. pose (g x := neg (f x x)). 
destruct (A g) as [x B]. absurd (g x = f x x).
unfold g. exact (N _). rewrite B. reflexivity. Qed.

(*** Exercise 10 ***)
Lemma uncountable_nat_nat : ~ countable (nat -> nat).
(*** Direct Proof ***)
(*** INSERT PROOF SCRIPT ***)

Lemma uncountable_nat_nat' : ~ countable (nat -> nat).
(*** Using Cantor_generalized ***)
(*** INSERT PROOF SCRIPT ***)

(*** Exercise 11 ***)
Lemma countable_option_nat : countable (option nat).
(*** INSERT PROOF SCRIPT ***)

(* Natural Order *)

Fixpoint leb (x y: nat) : bool :=
match x, y with
| O, _ => true
| S _, O => false
| S x', S y' => leb x' y'
 end.

Coercion bool2Prop (x : bool) := if x then True else False.

Notation "s >= t" := (leb t s).
Notation "s <= t" := (leb s t).
Notation "s > t" := (leb (S t) s).
Notation "s < t" := (leb (S s) t).

Ltac stauto := (simpl in *|-* ; tauto). 

Lemma le_trans {x} y {z} :
x<=y -> y<=z -> x<=z.
Proof. revert y z. induction x. stauto.
destruct y. stauto.
destruct z. stauto.
intros A B. apply (IHx y z) ; stauto. Qed.

Lemma lt_trans' {x} y {z} :
x < y -> y < z -> S x < z.
Proof. intros A B. apply (le_trans (S y)) ; assumption. Qed.

(*** Exercise 12 ***)
Lemma le_O {x} : 
x <= O -> x = O.
(*** INSERT PROOF SCRIPT ***)

Lemma le_S x :
x <= S x.
(*** INSERT PROOF SCRIPT ***)

Lemma le_irr x :
x < x -> False.
(*** INSERT PROOF SCRIPT ***)

(*** Exercise 13 ***)
Lemma le_lt_trans {x} y {z} :
x <= y -> y < z -> x < z.
(*** INSERT PROOF SCRIPT ***)

Lemma lt_le_trans {x} y {z} :
x < y -> y <= z -> x < z.
(*** INSERT PROOF SCRIPT ***)