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

(*** Untyped Lambda Calculus ***)

Inductive order : Type :=
| Less : order
| Equal : order
| Greater : order.

Fixpoint order_nat (m n : nat) : order :=
match m,n with
| O, O => Equal
| O, S _ => Less
| S _, O => Greater
| S m, S n => order_nat m n
end.

Inductive ter : Type :=
| R : nat -> ter
| L : ter -> ter
| A : ter -> ter -> ter.

Check L (L (A (A (R 1) (R 0)) (R 0))).

Fixpoint shift (d k : nat) (s : ter) :=
match s with
| A s1 s2 => A (shift d k s1) (shift d k s2)
| L s' => L (shift (S d) k s')
| R n => match order_nat n d with
           | Less => R n
           | _ => R (n + k)
         end
end.

Fixpoint subst (d : nat) (s t : ter) :=
match s with
| A s1 s2 => A (subst d s1 t) (subst d s2 t)
| L s' => L (subst (S d) s' t)
| R n => match order_nat n d with
           | Less => R n
           | Equal => shift 0 d t
           | Greater => R (pred n)
         end
end.

Compute subst 0 (L (A (R 1) (R 0))) (L (R 0)).

Definition eq_nat (m n : nat) : bool :=
match order_nat m n with Equal => true | _ => false end.

Fixpoint eq_ter (s t : ter) : bool :=
match s, t with
| R m, R n => eq_nat m n
| A s1 s2, A t1 t2 => andb (eq_ter s1 t1) (eq_ter s2 t2)
| L s', L t' => eq_ter s' t'
| _, _ => false
end.

Definition beta_top (s t : ter) : bool :=
match s with
| A (L s1') s2 => eq_ter t (subst 0 s1' s2)
| _ => false
end.

Fixpoint beta (s t : ter) : bool :=
  orb (beta_top s t)
  (match s, t with
     | R _ , _ => false
     | L s', L t' => beta s' t'
     | A s1 s2, A t1 t2 =>
       orb (andb (beta s1 t1) (eq_ter s2 t2)) 
       (andb (beta s2 t2) (eq_ter s1 t1))
     | _, _ => false
   end).

Definition omega : ter := (L (A (R 0) (R 0))).
Compute (beta (A omega omega) (A omega omega)).

Goal beta (A omega omega) (A omega omega) = true.
Proof. reflexivity. Qed.

Fixpoint normal (s : ter) : bool :=
match s with
| R _ => true
| L s' => normal s'
| A (L _) _ => false
| A s1 s2 => andb (normal s1) (normal s2)
end.

Compute normal omega.
Compute normal (A omega omega).

Inductive red : ter -> ter -> Prop :=
| redR : forall s, red s s
| redS : forall t s u, beta s t = true -> red t u -> red s u.

Lemma beta_red s t : beta s t = true -> red s t.

Proof. intros A. apply (@redS t). exact A. apply redR. Qed.

Definition normal_form (s t : ter) : Prop :=
normal t = true /\ red s t.

Goal normal_form 
(A (L (A (R 0) (A (R 0) (R 8)))) (L (R 0))) 
(R 7).

Proof. split. reflexivity.
apply (@redS (A (L (R 0)) (A (L (R 0)) (R 7)))). reflexivity.
apply (@redS (A (L (R 0)) (R 7))). reflexivity.
apply beta_red. reflexivity. Qed.

(*** Exercise 4.7 ***)
(*** Find the normal form of ((fun x y => x) y).
     y is argument reference 1 in the representation below.
 ***)
Goal exists t, normal_form (A (L (L (R 1))) (R 1)) t.
(*** INSERT PROOF ***)

(*** Find the normal form of ((fun f => f x y) (fun u v => u)).
     x is argument reference 0 in the representation below.
     y is argument reference 1 in the representation below.
 ***)
Goal exists t, normal_form (A (L (A (A (R 0) (R 1)) (R 2))) (L (L (R 1)))) t.
(*** INSERT PROOF ***)

(* Exercise 4.8 *)
Definition Nat : Prop := forall X : Prop, X -> (X -> X) -> X.
Definition O : Nat := fun X x _ => x.
Definition S (n : Nat) : Nat := fun X x f => n X (f x) f.
Compute S (S O).
Definition plus (m n : Nat) : Nat := m Nat n S.
Compute plus (S (S O)) (S (S (S O))).
Definition times (m n : Nat) : Nat := m Nat O (plus n).
Compute times (S (S O)) (S (S (S O))).

Definition power (m n : Nat) : Nat :=
(*** INSERT DEFINITION ***)

Compute power (S (S O)) (S (S O)).
Compute power (S (S O)) (S (S (S O))).
Compute power (S (S (S O))) (S (S O)).

(*** Exercise 4.9 ***)
Definition Prod (X Y : Prop) : Prop := forall Z : Prop, (X -> Y -> Z) -> Z.
Definition pair (X Y : Prop) (x : X) (y : Y) : Prod X Y :=
(*** INSERT DEFINITION ***)
Definition fst (X Y : Prop) (u : Prod X Y) : X :=
(*** INSERT DEFINITION ***)
Definition snd (X Y : Prop) (u : Prod X Y) : Y :=
(*** INSERT DEFINITION ***)

Compute (fun (X Y:Prop) (x:X) (y:Y) => fst (pair x y)).
Compute (fun (X Y:Prop) (x:X) (y:Y) => snd (pair x y)).

(*** Exercise 4.10 ***)
Definition fac (n:Nat) :=
(*** INSERT DEFINITION ***)

Compute (fac O).
Compute (fac (S O)).
Compute (fac (S (S O))).
Compute (fac (S (S (S O)))).
Compute (fac (S (S (S (S O))))).

(*** Propositions and Proofs ***)
(*** Exercise 4.11 ***)
Goal forall X : Prop,  
~~(X \/ ~X).
(*** INSERT PROOF ***)

Goal forall X Y : Prop,
~~(~(X /\ Y) -> ~X \/ ~Y).
(*** INSERT PROOF ***)

(*** Exercise 4.12 ***)
Definition decidable (P:Prop) : Prop := P \/ ~P.

Goal decidable (forall X, ~(X \/ ~X)).
(*** INSERT PROOF ***)

Goal decidable (exists X, ~(X \/ ~X)).
(*** INSERT PROOF ***)