Require Import Program.Equality.
Set Implicit Arguments.

Inductive ty : Type :=
| Nat : ty
| Bool : ty.

Inductive tm : ty -> Type :=
| tmT : tm Bool
| tmF : tm Bool
| tmI T : tm Bool -> tm T -> tm T -> tm T
| tmO : tm Nat
| tmS : tm Nat -> tm Nat
| tmP : tm Nat -> tm Nat
| tmZ : tm Nat -> tm Bool.

Inductive value : forall T : ty, tm T -> Prop :=
| valueF : value tmT
| valueT : value tmF
| valueO : value tmO
| valueS t : value t -> value (tmS t).

Inductive step : forall T : ty, tm T -> tm T -> Prop :=
| stepIT T (t1 t2 : tm T) : step (tmI tmT t1 t2) t1
| stepIF T (t1 t2 : tm T) : step (tmI tmF t1 t2) t2
| stepPO : step (tmP tmO) tmO
| stepPS t : value t -> step (tmP (tmS t)) t
| stepZO : step (tmZ tmO) tmT
| stepZS t : value t -> step (tmZ (tmS t)) tmF
| stepDI t t' T (t1 t2 : tm T) : step t t' -> step (tmI t t1 t2) (tmI t' t1 t2)
| stepDS t t' : step t t' -> step (tmS t) (tmS t')
| stepDP t t' : step t t' -> step (tmP t) (tmP t')
| stepDZ t t' : step t t' -> step (tmZ t) (tmZ t').

Lemma value_normal (T : ty) (t t' : tm T) :
value t -> step t t' -> False.

Proof. intros A B.
induction B ; dependent destruction A ; auto. Qed.

Lemma step_deterministic (T : ty) (t t1 t2 : tm T) :
step t t1 -> step t t2 -> t1 = t2.

Proof. intros A ; revert t2.
induction A ; intros t2' B ; dependent destruction B
; f_equal ; auto
; exfalso ; eauto using value_normal, value. Qed.

Lemma Progress (T : ty) (t : tm T) :
value t \/ exists t', step t t'.

Proof with now eauto using step, value.
induction t ; eauto using value.
(* if *) destruct IHt1. dependent destruction H... destruct H...
(* S *) destruct IHt. trivial... destruct H...
(* P *) destruct IHt. dependent destruction H... destruct H...
(* Z *) destruct IHt. dependent destruction H... destruct H... Qed.

Definition ty_den (T : ty) : Type :=
match T with Bool => bool | Nat => nat end.

Fixpoint eval (T : ty) (t : tm T) : tm T :=
  match t with
    | tmT => tmT
    | tmF => tmF
    | tmO => tmO
    | tmS t' => tmS (eval t')
    | tmP t' => match eval t' with tmS v => v | _ => tmO end
    | tmZ t' => match eval t' with tmO => tmT | _ => tmF end
    | tmI T t t1 t2 => match eval t with tmT => eval t1 | _ => eval t2 end
  end.

Lemma eval_value (T : ty) (t : tm T) :
value (eval t).

Proof with now auto using value.
induction t ; auto using value ; simpl.
dependent destruction IHt1 ; rewrite <-x...
dependent destruction IHt ; rewrite <-x...
dependent destruction IHt ; rewrite <-x...
dependent destruction IHt ; rewrite <-x... Qed.