(*** Introduction to Computational Logic, Coq part of Assignment 10 ***)
(*** Solutions ***)
(***
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/
***)

Coercion bool2Prop (x : bool) := if x then True else False.
Ltac stauto := (simpl ; tauto). 

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

Inductive even : nat -> Prop :=
| evenO : even 0
| evenS : forall n, even n -> even (S (S n)).

(*** Exercise 1 ***)
Lemma ex5811 n :
even n -> even (4+n).
(*** INSERT PROOF SCRIPT ***)

(*** Exercise 2 ***)
Lemma ex58221 :
~ even 3.
(*** INSERT PROOF SCRIPT ***)

Lemma ex5822 n :
even (4+n) -> even n.
(*** INSERT PROOF SCRIPT ***)

(*** Exercise 3 ***)
Lemma even_sum m n :
even m -> even n -> even (m+n).
(*** INSERT PROOF SCRIPT ***)

Lemma even_sum' m n :
even (m+n) -> even m -> even n.
(*** INSERT PROOF SCRIPT ***)

(*** Exercise 4 ***)
Lemma evenib n :  even n <-> evenb n.
(*** INSERT PROOF SCRIPT ***)

(*** Exercise 5 ***)
Definition evenp (n : nat) : Prop :=
forall p : nat -> Prop,
p 0 ->
(forall n, p n -> p (S (S n))) ->
p n.

Lemma evenip n :  even n <-> evenp n.
(*** INSERT PROOF SCRIPT ***)

(*** Exercise 6 ***)
Inductive eq2 (X : Type) : X -> X-> Prop :=
| eq2_I : forall x : X, eq2 X x x.

Lemma eq2_E (X : Type) (x y : X) :
eq2 X x y -> forall p : X -> Prop, p y -> p x.
(*** INSERT PROOF SCRIPT ***)

(*** leb ***)
Fixpoint leb (x y: nat) : bool :=
match x, y with
| O, _ => true
| S _, O => false
| S x', S y' => leb x' y'
 end.
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).
Lemma le_refl x :
x <= x.
Proof. induction x ; stauto. Qed.
Lemma le_O {x} : 
x <= O -> x = O.
Proof.  destruct x ; stauto. Qed.
Lemma le_S x :
x <= S x.
Proof. induction x ; stauto. Qed.
Lemma le_or {x y} :
x<=y -> x<y \/ x=y.
Proof. revert y. induction x ; destruct y ; try stauto.
intros A. destruct (IHx y A) as [B|B]. stauto. 
rewrite B. stauto. Qed.
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 le_rwk {x y} :
x <= y -> x <= S y.
Proof. intros A.  apply (le_trans y).
exact A. exact (le_S _). Qed.

(*** Exercise 7 ***)
Inductive lei : nat -> nat -> Prop :=
| leiO : forall x : nat, lei O x
| leiS : forall x y, lei x y -> lei (S x) (S y).

Lemma lei_refl x :
lei x x.
(*** INSERT PROOF SCRIPT ***)

Lemma lei_trans x y z :
lei x y -> lei y z -> lei x z.
(*** INSERT PROOF SCRIPT ***)

Lemma leib x y :
leb x y <-> lei x y.
(*** INSERT PROOF SCRIPT ***)

(*** Exercise 8 ***)
Lemma ex8a (p : Prop) : p \/ p -> p + p.
(*** INSERT PROOF SCRIPT ***)

Lemma ex8b (p : Prop) : p \/ False -> p + False.
(*** INSERT PROOF SCRIPT ***)

(*** div2 ***)
Definition Div2 : Type :=
forall n : nat, {k | n = 2*k} + {k | n = S (2*k)}.

Lemma plus_S x y :
x + S y = S (x + y).
Proof. induction x. reflexivity.
simpl. f_equal. exact IHx. Defined.

Definition div2c : Div2.
unfold Div2. induction n. 
left. exists 0. reflexivity.
destruct IHn as [[k A]|[k A]].
right. exists k. f_equal. exact A.
left. exists (S k). rewrite A. simpl. 
rewrite plus_S. reflexivity. Defined.

Print div2c.
Compute div2c 11.

Definition divmod2 (n : nat) : nat + nat.
destruct (div2c n) as [[k _]|[k _]]. 
exact (inl nat k). exact (inr nat k). Defined.

Compute divmod2 9.

(*** Exercise 9 ***)
Definition forget {X Y} {p : X -> Prop} {q : Y -> Prop} :
sig p + sig q -> X + Y.
(*** INSERT DEFINITION AS A PROOF SCRIPT ***)

Print forget.

Compute (forget (div2c 13)).

Lemma forget_div2c (n : nat) :
forget (div2c n) = divmod2 n.
(*** INSERT PROOF SCRIPT ***)

(*** bool2sum ***)
Definition bool2sum (b : bool) :  (b : Prop) + ~b :=
if b as z return z + ~z then inl _ I else inr _ (fun f => f).

(*** Exercise 10 ***)
(*** Recall the type Search of a search function. ***)
Definition Search : Type :=
forall (p : nat -> bool) (n : nat),
{x | x <= n /\ p x} + (forall x, x <= n -> ~ p x).

(*** Define a type SearchMax that will ensure that the return value is the maximum x <= n such that p x, if such an x exists. ***)
Definition SearchMax : Type :=
(*** INSERT DEFINITION ***)

Definition searchMaxc : SearchMax.
(*** INSERT DEFINITION AS A PROOF SCRIPT ***)

Compute searchMaxc (fun x => x + x > 8) 5.