Set Implicit Arguments.

Inductive var : Type :=
| varN : nat -> var.

Inductive ty : Type :=
| tyN : ty (* nat *)
| tyF : ty -> ty -> ty. (* function type *)

Inductive tm : Type :=
| tmO : tm (* zero *)
| tmS : tm -> tm (* successor *)
| tmC : tm -> tm -> tm -> tm (* case *)
| tmV : var -> tm (* variable *)
| tmL : var -> ty -> tm -> tm (* lambda *)
| tmA : tm -> tm -> tm (* application *)
| tmF : tm -> tm. (* fix *)

Inductive free (x : var) : tm -> Prop :=
| freeS t : free x t -> free x (tmS t)
| freeC t t1 t2 : free x t \/ free x t1 \/ free x t2 -> free x (tmC t t1 t2)
| freeV : free x (tmV x)
| freeL y T t : x<>y -> free x t -> free x (tmL y T t)
| freeA t1 t2 : free x t1 \/ free x t2 -> free x (tmA t1 t2)
| freeF t : free x t -> free x (tmF t).

Definition closed (t : tm) : Prop :=
forall x : var, ~ free x t.

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

Definition eq_var (x y : var) : bool :=
match x, y with varN x', varN y' => eq_nat x' y' end.

Fixpoint subst (t : tm) (x : var) (s : tm) : tm :=
  match t with
    | tmO => t
    | tmS t' => tmS (subst t' x s)
    | tmC t0 t1 t2 => tmC (subst t0 x s) (subst t1 x s) (subst t2 x s)
    | tmV y => if eq_var x y then s else t
    | tmL y T t' => if eq_var x y then t else tmL y T (subst t' x s)
    | tmA t1 t2 => tmA (subst t1 x s) (subst t2 x s)
    | tmF t' => tmF (subst t' x s)
  end.

Inductive nvalue : tm -> Prop :=
| nvalueO : nvalue tmO
| nvalueS t : nvalue t -> nvalue (tmS t).

Inductive value : tm -> Prop :=
| valueN t : nvalue t -> value t
| valueL x T t : value (tmL x T t).

Inductive step : tm -> tm -> Prop :=
| stepCO t1 t2 : step (tmC tmO t1 t2) t1
| stepCS t t1 t2 : nvalue t -> step (tmC (tmS t) t1 t2) t2
| stepA x T t s : value s -> step (tmA (tmL x T t) s) (subst t x s)
| stepF x T t : step (tmF (tmL x T t)) (subst t x (tmF (tmL x T t)))
| stepDS t t' : step t t' -> step (tmS t) (tmS t')
| stepDC t t' t1 t2 : step t t' -> step (tmC t t1 t2) (tmC t' t1 t2)
| stepDA t1 t1' t2 : step t1 t1' -> step (tmA t1 t2) (tmA t1' t2)
| stepDAR x T t t2 t2' : step t2 t2' -> step (tmA (tmL x T t) t2) (tmA (tmL x T t) t2').

Definition context : Type := var -> option ty.
Definition empty : context := fun _ => None.
Definition update (g : context) (x : var) (T : ty) : context :=
fun y => if eq_var x y then Some T else g y.

Inductive type : context -> tm -> ty -> Prop :=
| typeO g : type g tmO tyN
| typeS g t : type g t tyN -> type g (tmS t) tyN
| typeC g t t1 t2 T : type g t tyN -> type g t1 T -> type g t2 (tyF tyN T) -> type g (tmC t t1 t2) T
| typeV g x T : g x = Some T -> type g (tmV x) T
| typeL g x T t T' : type (update g x T) t T' -> type g (tmL x T t) (tyF T T')
| typeA g t1 t2 T T2 : type g t1 (tyF T2 T) -> type g t2 T2 -> type g (tmA t1 t2) T
| typeF g x T1 T2 t : type (update g x (tyF T1 T2)) t (tyF T1 T2) ->
  type g (tmF (tmL x (tyF T1 T2) t)) (tyF T1 T2).

Lemma value_normal t t' :
value t -> step t t' -> False.
Admitted.

Lemma step_deterministic t t1 t2 :
step t t1 -> step t t2 -> t1 = t2.
Admitted.

Lemma type_unique g t T1 T2 :
type g t T1 -> type g t T2 -> T1 = T2.
Admitted.

Lemma substitution g t T x s S :
type (update g x S) t T -> type empty s S -> type g (subst t x s) T.
Admitted.

Lemma preservation t T t' :
type empty t T -> step t t' -> type empty t' T.
Admitted.

Lemma progress t T :
type empty t T -> value t \/ exists t', step t t'.
Admitted.

Module Example.
(* fix f x y => match x with 0 => y | S x' => S (f x' y) end *)

Definition f : var := varN 0.
Definition x : var := varN 1.
Definition y : var := varN 2.
Definition x' : var := varN 3.

Definition pcf_add : tm :=
  tmF (tmL f (tyF tyN (tyF tyN tyN))
        (tmL x tyN
          (tmL y tyN
            (tmC (tmV x) (tmV y)
              (tmL x' tyN (tmS (tmA (tmA (tmV f) (tmV x')) (tmV y)))))))).

End Example.

Inductive sem : tm -> tm -> Prop :=
| semV v : value v -> sem v v
| semS t u : sem t u -> nvalue u -> sem (tmS t) (tmS u)
| semCO t t1 t2 v : sem t tmO -> sem t1 v -> sem (tmC t t1 t2) v
| semCS t t1 t2 u v : sem t (tmS u) -> sem (tmA t2 u) v -> sem (tmC t t1 t2) v
| semA t1 t2 x T t v2 v : sem t1 (tmL x T t) -> sem t2 v2 -> sem (subst t x v2) v -> sem (tmA t1 t2) v
| semF x T t v : sem (subst t x (tmF (tmL x T t))) v -> sem (tmF (tmL x T t)) v.

Goal forall t t', sem t t' -> value t'.
Proof. intros t t' A. induction A ; auto using value, nvalue. Qed.

Tactic Notation "inv" hyp(A) := inversion A ; subst ; clear A.

Lemma eq_var_correct x y :
eq_var x y = true <-> x = y.

Proof. destruct x, y ; simpl ; split.
revert n0 ; induction n ; intros n0 A ; destruct n0 ; inv A.
  reflexivity. apply IHn in H0 ; inv H0 ; reflexivity.
revert n0 ; induction n ; intros n0 A ; destruct n0 ; inv A.
  reflexivity. firstorder. Qed.

Fixpoint freeb (x : var) (t : tm) : bool :=
  match t with
    | tmO => false
    | tmS t' => freeb x t'
    | tmC t0 t1 t2 => orb (freeb x t0) (orb (freeb x t1) (freeb x t2))
    | tmV y => eq_var x y
    | tmL y _ t' => if eq_var x y then false else freeb x t'
    | tmA t1 t2 => orb (freeb x t1) (freeb x t2)
    | tmF t' => freeb x t'
  end.

Fixpoint eq_ty (S T : ty) : bool :=
match S, T with
| tyN, tyN => true
| tyF S1 S2, tyF T1 T2 => andb (eq_ty S1 T1) (eq_ty S2 T2)
| _, _ => false
end.