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

Set Implicit Arguments.

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

(* zerop *)

Inductive zerop : nat -> Prop :=
| zeropI : zerop O.

(*** Exercise 8.1 ***)
Goal ~zerop 2.
(*** prove using exact ***)

Goal ~zerop 2.
(*** prove using remember ***)

Goal ~zerop 2.
(*** prove using assert ***)

Goal ~zerop 2.
(*** prove using inversion ***)

(*** Exercise 8.2 ***)
Definition zerop_cast1 (X:nat -> Type) (n:nat) : zerop n -> X O -> X n :=
(*** define ***)

Definition zerop_cast2 (X:nat -> Type) (n:nat) : zerop n -> X n -> X O :=
(*** define ***)

Lemma zerop_cast1_eq X (x:X O) : zerop_cast1 X zeropI x = x.
(*** prove ***)

Lemma zerop_cast2_eq X (x:X O) : zerop_cast2 X zeropI x = x.
(*** prove ***)

Lemma zerop_cast12_eq X n (A:zerop n) (x:X O) : zerop_cast2 X A (zerop_cast1 X A x) = x.
(*** prove ***)

Lemma zerop_cast21_eq X n (A:zerop n) (x:X n) : zerop_cast1 X A (zerop_cast2 X A x) = x.
(*** prove ***)

(*** Exercise 8.4 ***)
Lemma ex_eq_ref (X : Type) (x : X) :  eq x x.
(*** prove ***)

Lemma ex_eq_sym (X : Type) (x y : X) :  eq x y -> eq y x.
(*** prove ***)

Lemma ex_eq_trans (X : Type) (x y z : X) :  eq x y -> eq y z -> eq x z.
(*** prove ***)

Lemma ex_eq_f_equal (X Y : Type) (f : X -> Y) (x y : X) :  
eq x y -> eq (f x) (f y).
(*** prove ***)

Lemma ex_eq_rewrite_R (X : Type) (x y : X) (p : X -> Prop) :
eq x y -> p x -> p y.
(*** prove ***)

(* even *)

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

(*** Exercise 8.5 ***)
Goal ~ even 1.
(*** prove without inversion ***)

Goal forall n, even (S (S n)) -> even n.
(*** prove without inversion ***)

Lemma even_notS n :
even n -> ~even (S n).
Proof. revert n. apply even_ind.
intros A. inversion A.
intros n A B C. inversion C. tauto. Qed.

Lemma even_nSn n :
(~even n -> even (S n)) /\ (~even (S n) -> even n).
Proof. induction n.
split. intros A. contradiction (A evenO). intros. constructor.
split. intros A. apply evenS. apply IHn. exact A.
intros A. apply IHn. intros B. apply A. constructor. exact B.
Qed.

Lemma even_dec n : even n \/ ~even n.
Proof. induction n. left. constructor.
destruct IHn as [A|A].
right. apply even_notS. exact A.
left. apply even_nSn. intros B. inversion B. contradiction (A H0).
Qed.

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

(*** Exercise 8.6 ***)
Lemma evenib n :  even n <-> evenb n.
(*** prove ***)

(*** Exercise 8.7 ***)
Lemma even_sum m n : even m -> even n -> even (m+n).
(*** prove by induction on proof terms ***)

Lemma even_sum' m n : even (m+n) -> even m -> even n.
(*** prove by induction on proof terms ***)

(*** Exercise 8.8 ***)
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.
(*** prove ***)

Lemma le_O (y : nat) :
le O y.
Proof. induction y ; constructor. exact IHy. Qed.

Lemma le_S (x y : nat) :
le x y -> le (S x) (S y).
Proof. intros A. induction A; constructor. assumption. Qed.

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

Lemma leb_S (x y : nat) :
leb x y -> leb x (S y).
(*** prove ***)

Lemma leb_refl ( x : nat) :
leb x x.
(*** prove ***)

Lemma leb_le (x y : nat) :
le x y -> leb x y.
(*** prove ***)

Lemma le_leb (x y : nat) :
leb x y -> le x y.
(*** prove ***)

Lemma le_leb_e (x y : nat) :
le x y <-> leb x y.
(*** prove ***)

Lemma le_dec (x y : nat) :
le x y \/ ~le x y.
(*** prove ***)

(*** Exercise 8.10 ***)
Lemma le_Sleft1 (x y : nat) :
le (S x) y -> le x y.
(*** prove ***)

Lemma le_Sleft (x y : nat) :
le (S x) (S y) -> le x y.
(*** prove ***)

Lemma le_antisym (x y : nat) :
le x y -> le y x -> x = y.
(*** prove ***)

Goal forall x, le x 0 -> x = 0.
(*** prove ***)

Goal forall x, ~ le (S x) x.
(*** prove ***)