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

(*** Exercise 7.1 ***)
Goal forall (X : Type) (x : X) (xs : list X),
cons x xs <> nil.

(*** Prove with discriminate ***)

Goal forall (X : Type) (x : X) (xs : list X),
cons x xs <> nil.

(*** Prove with change (without discriminate) ***)

(*** Exercise 7.2 ***)
Goal forall (X : Type) (x y x' y' : X),
pair x y = pair x' y' -> y = y'.

(*** Prove with injection ***)

Goal forall (X : Type) (x y x' y' : X),
pair x y = pair x' y' -> y = y'.

(*** Prove with change (without injection) ***)

Goal forall (X : Type) (x x' : X) (xs xs' : list X),
cons x xs = cons x' xs' -> xs = xs'.

(*** Prove with injection ***)

Goal forall (X : Type) (x x' : X) (xs xs' : list X),
cons x xs = cons x' xs' -> xs = xs'.

(*** Prove with change (without injection) ***)

(*** Exercise 7.3 ***)
Goal forall x,
negb x <> x.

(*** Prove ***)

Goal forall x,
S x <> x.

(*** Prove ***)

Goal forall x y z,
x + y = x + z -> y = z.

(*** Prove ***)

(*** Exercise 7.4 ***)
Fixpoint eq_nat (x y : nat) : bool :=
match x, y with
| 0, 0 => true
| S x', S y' => eq_nat x' y'
| _, _ => false
end.

Lemma eq_nat_correct : forall x y : nat,
eq_nat x y = true <-> x = y.

Proof. induction x ; destruct y ; split ; simpl ; intros A ;
auto ; try discriminate A.
f_equal. now apply IHx, A.
apply IHx. injection A. auto. Qed. 

Fixpoint eq_list_nat (xs ys : list nat) : bool :=
(*** Define ***)

Goal forall xs ys : list nat,
eq_list_nat xs ys = true <-> xs = ys.

(*** Prove ***)

(*** Exercise 7.5 ***)
Definition decidable (X:Prop) : Prop := X \/ ~X.

Goal forall X:Type, forall f:X -> X -> bool,
 (forall x y, f x y = true <-> x = y)
 -> forall x y:X, decidable (x = y).
(*** Prove ***)

(*** Exercise 7.6 ***)
Goal bool <> option bool.

(*** Prove ***)

(*** Exercise 7.7 ***)
Definition smaller (X Y : Type) : Prop :=
~ exists f : X -> Y, forall y, exists x, f x = y.

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

Theorem Cantor (X Y : Type) :
strong Y -> smaller X (X -> Y).

(*** Prove ***)

(*** Exercise 7.8 ***)
Goal forall (X : Type) (Y : Prop) ,
X -> Y <-> (exists x : X, True) -> Y.

(*** Prove ***)

(*** Exercise 7.9 ***)
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_strict x :
~ x < x.

(*** Prove ***)

Lemma le_or x y :
x<=y -> x<y \/ x=y.

(*** Prove ***)

Lemma le_neg x y :
negb (x <= y) = (x > y).

(*** Prove ***)

Goal forall x y,
x<y \/ x=y \/ x>y.

(*** Prove ***)

(*** Exercise 7.10 ***)
Goal forall x y : bool,
x /\ y <-> andb x y.

(*** Prove ***)

Goal forall (b : bool) (X : Prop),
(b <-> X) -> (~b <-> ~X).

(*** Prove ***)

(*** Exercise 7.11 ***)
Goal forall x y, x <= y <-> exists z, x + z = y.

(*** Prove ***)

(*** Exercise 7.12 ***)
Lemma le_trans x y z :
x<=y -> y<=z -> x<=z.

Proof. revert y z. induction x ; simpl. now auto.
destruct y ; simpl. now auto.
destruct z ; simpl. now auto.
exact (IHx _ _). Qed.

Lemma size_induction (X : Type) (f : X -> nat) (p: X ->Prop) :
(forall x, (forall y, f y  < f x -> p y)  -> p x) 
-> forall x, p x.

Proof. intros A x. apply A. induction (f x) ; simpl. tauto.
intros y B. apply A. intros z C. apply IHn. 
exact (le_trans _ _ _ C B). Qed.

Lemma complete_induction (p: nat->Prop) :
(forall n, (forall m, m < n -> p m)  -> p n) 
-> forall n, p n.

(*** Prove using size_induction ***)

(*** Exercise 7.13 ***)
Goal forall p : nat -> Prop,
p 0 -> p 1 -> (forall n, p n -> p (S (S n))) -> forall n, p n.

(*** Prove this with an exact proof term using fix and match ***)

Goal forall p : nat -> Prop,
p 0 -> p 1 -> (forall n, p n -> p (S (S n))) -> forall n, p n.

(*** Prove this with complete_induction. ***)

(*** Exercise 7.14 ***)
Definition primrec 
(t : nat -> Type) (base : t 0) (step : forall n, t n -> t (S n)) 
: forall n : nat, t n
:= fix f n := match n as z return t z with
                | 0 => base
                | S n' => step n' (f n')
              end.

Definition multiplication (f : nat -> nat -> nat) : Prop :=
(*** Define ***)

Goal multiplication mult.

(*** Prove ***)

Goal forall f g x y,
multiplication f -> multiplication g -> f x y = g x y.

(*** Prove ***)

Definition multpr : nat -> nat -> nat :=
(*** Define ***)

Goal multiplication multpr.

(*** Prove ***)

(*** Exercise 7.15 ***)
Goal forall (f g : bool -> bool) (x : bool),
f (f (f (g x))) = f (g (g (g x))). 

(*** Prove ***)