Set Implicit Arguments.
Require Import EqNat.
Tactic Notation "inv" hyp(A) := inversion A ; subst ; clear A.

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

Inductive ty : Type :=
| Nat : ty (* nat *)
| Fun : ty -> ty -> ty. (* function type *)

Inductive tm : Type :=
| tmV : var -> tm (* variable *)
| tmL : var -> ty -> tm -> tm (* lambda *)
| tmA : tm -> tm -> tm . (* application *)

Inductive free (x : var) : tm -> Prop :=
| 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).

Definition beq_var (x y : var) : bool :=
match x, y with Var x', Var y' => beq_nat x' y' end.

Lemma beq_var_eq b x y :
b = beq_var x y -> if b then x=y else x<>y.

Proof. destruct x, y ; simpl ; intros A ; destruct b.
apply beq_nat_eq in A. congruence.
symmetry in A. apply beq_nat_false in A. congruence. Qed.

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

Inductive type : context -> tm -> ty -> Prop :=
| typeV g x T : g x = Some T -> type g (tmV x) T
| typeL g x S t T : type (update g x S) t T -> type g (tmL x S t) (Fun S T)
| typeA g t1 t2 S T : type g t1 (Fun S T) -> type g t2 S -> type g (tmA t1 t2) T.

Lemma type_free g t T x :
type g t T -> free x t -> exists S, g x = Some S.

Proof. intros A B. induction A ; inv B.
(* V *) now eauto.
(* L *) apply IHA in H3. destruct H3 as [S0 C].
unfold update in C. remember (beq_var x0 x) as b.
destruct b ; apply beq_var_eq in Heqb. congruence. now eauto.
(* A *) inv H0 ; auto. Qed.

Lemma type_empty t T x :
type empty t T -> free x t -> False.

Proof. intros A B. destruct (type_free A B) as [S C]. inv C. Qed.

Lemma type_invariance t g g' T :
(forall x, free x t -> g x = g' x) -> type g t T -> type g' t T.

Proof with now auto using free.
intros A B ; revert g' A ; induction B ; intros g' A.
(* V *) constructor. rewrite A in H...
(* L *) constructor. apply IHB. intros y C.
unfold update. remember (beq_var x y) as b.
destruct b ; apply beq_var_eq in Heqb...
(* A *) apply typeA with (S:=S)... Qed.

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

Proof. intros A ; revert T2 ; induction A ; intros T2 B ; inv B.
(* V *) congruence.
(* L *) now f_equal ; auto.
(* A *) apply IHA1 in H2 ; apply IHA2 in H4 ; congruence. Qed.

Fixpoint subst (t : tm) (x : var) (s : tm) : tm :=
  match t with
    | tmV y => if beq_var x y then s else t
    | tmL y T t' => if beq_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)
  end.

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.

Proof. revert g T ; induction t ; simpl ; intros g T A B ; inv A.
(* x *) unfold update in H1. remember (beq_var x v) as b.
destruct b ; apply beq_var_eq in Heqb.
inv H1. apply type_invariance with (g:= empty) ; auto.
   now intros y C ; exfalso ; eauto using type_empty.
now eauto using type.
(* L *) remember (beq_var x v) as b ; destruct b
; apply beq_var_eq in Heqb ; constructor.
subst v.
  apply type_invariance with (g := update (update g x S) x t) ; auto.
  intros y C. unfold update. remember (beq_var x y) as b.
  destruct b ; apply beq_var_eq in Heqb ; congruence.
apply IHt ; auto.
  apply type_invariance with (g := update (update g x S) v t) ; auto.
  intros y C. unfold update.
  remember (beq_var x y) as c ; remember (beq_var v y) as d.
  destruct c , d ; apply beq_var_eq in Heqc ; apply beq_var_eq in Heqd
  ; congruence.
(* A *) eauto using type. Qed.

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

Inductive step : tm -> tm -> Prop :=
| stepA x T t s : value s -> step (tmA (tmL x T t) s) (subst t x s)
| stepDAL 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').

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

Proof. intros A. revert t' ; induction A ; intros t' B ; inv B. Qed.

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

Proof. intros A B ; revert T A ; induction B ; intros T' A ; inv A.
(* A *) inv H3. now eauto using substitution.
(* ADL *) now eauto using type.
(* ADR *) eauto using type. Qed.

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

Proof. intros A ; remember empty as g ; induction A ; subst g.
(* V *) now inv H.
(* L *) now auto using value.
(* A *) right ; intuition ; inv H0 ; eauto using step.
inv H1 ; eauto using step. Qed.