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

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

Inductive tm : Type :=
| tmR : nat -> tm (* reference *)
| tmL : ty -> tm -> tm (* lambda *)
| tmA : tm -> tm -> tm . (* application *)

Definition context := list ty.

Inductive typeC : context -> nat -> ty -> Prop :=
| typeCO g T : typeC (T::g) 0 T
| typeCS g n T T' : typeC g n T -> typeC (T'::g) (S n) T.

Inductive type : context -> tm -> ty -> Prop :=
| typeR g x T :
  typeC g x T ->
  type g (tmR x) T
| typeL g T t T' :
  type (T::g) t T' ->
  type g (tmL T t) (Fun T T')
| typeA g t1 t2 T1 T :
  type g t1 (Fun T1 T) ->
  type g t2 T1 ->
  type g (tmA t1 t2) T.

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.
(* R *) now induction H ; inv H2 ; auto.
(* L *) now f_equal ; auto.
(* A *) apply IHA1 in H2 ; apply IHA2 in H4 ; congruence. Qed.

Fixpoint shift (d k : nat) (t : tm) : tm :=
match t with
| tmR x => tmR (if le_gt_dec d x then x + k else x)
| tmL T t' => tmL T (shift (S d) k t')
| tmA t1 t2 => tmA (shift d k t1) (shift d k t2)
end.

Fixpoint subst (d : nat) (t s : tm) : tm :=
match t with
| tmR x => match lt_eq_lt_dec d x with
             | inleft (left _) => tmR (pred x) (* x>d, free but not least *)
             | inleft (right _) => shift 0 d s (* x=d, free and least *)
             | inright _ => tmR x (* x<d, bound *)
           end
| tmL T t' => tmL T (subst (S d) t' s)
| tmA t1 t2 => tmA (subst d t1 s) (subst d t2 s)
end.

Lemma shifting g g1 g2 t T :
type (g1 ++ g) t T ->
type (g1 ++ g2 ++ g) (shift (length g1) (length g2) t) T.

Proof. revert g1 T ; induction t ; intros g1 T A ; simpl ; inv A.
(* R *) constructor. destruct (le_gt_dec (length g1) n) ;
revert dependent n ; induction g1 ; simpl ; intros n A B.
(* 1 *) assert (R : n + length g2 = length g2 + n) by omega. rewrite R. clear B R.
induction g2 ; simpl. assumption. constructor ; assumption.
(* 2 *) destruct n. now inv B. inv A ; simpl ; constructor. intuition ; omega.
(* 3 *) now inv B.
(* 4 *) destruct n ; inv A ; constructor. intuition ; omega.
(* L *) constructor. exact (IHt (t::g1) _ H3).
(* A *) econstructor ; eauto. Qed.

Lemma substitution g g' T' T s t :
type (g ++ T'::g') t T ->
type g' s T' ->
type (g ++ g') (subst (length g) t s) T.

Proof. revert g T ; induction t ; intros g T A B ; inv A ; simpl.
(* R *) destruct (lt_eq_lt_dec (length g) n). destruct s0.
(* 1 *) clear B s. constructor. destruct n. now inv l. simpl.
revert dependent n. induction g ; simpl ; intros n A B ; inv A. assumption.
destruct n. now inv B. constructor. intuition ; omega.
(* 2 *) subst n.
assert (T'=T) by (induction g ; simpl in H1 ; inv H1 ; auto). subst T'.
apply shifting with (g1:=nil) ; assumption.
(* 3 *) clear B s. constructor.
revert dependent n. induction g ; simpl ; intros n A B. now inv B.
destruct n ; inv A ; constructor. intuition ; omega.
(* L *) constructor. exact (IHt (t::g) _ H3 B).
(* A *) econstructor ; eauto. Qed.

Inductive step : tm -> tm -> Prop :=
| stepB T t s :
  step (tmA (tmL T t) s) (subst 0 t s)
| stepDL T t t' :
  step t t' ->
  step (tmL T t) (tmL T t')
| stepA1 t1 t1' t2 :
  step t1 t1' ->
  step (tmA t1 t2) (tmA t1' t2)
| stepA2 t1 t2 t2' :
  step t2 t2' ->
  step (tmA t1 t2) (tmA t1 t2').

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

Proof. intros A B ; revert g T A.
induction B ; intros g T' A ; inv A ; eauto using type.
inv H2. eapply substitution with (g:=nil) ; eauto. Qed.

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

Lemma progress t T :
type nil t T -> abstraction t \/ exists t', step t t'.

Proof. revert T ; induction t ; intros T A ; inv A.
(* R *) now inv H1.
(* L *) now left ; constructor.
(* A *) right. destruct (IHt1 _ H2) ; inv H ; eauto using step. Qed.

Inductive free : nat -> tm -> Prop :=
| freeR x : free x (tmR x)
| freeL x T t : free (S x) t -> free x (tmL T t)
| freeA x t1 t2 : free x t1 \/ free x t2 -> free x (tmA t1 t2).

Lemma type_free g t T x :
type g t T -> free x t -> x < length g.

Proof. intros A ; revert x ; induction A ; intros n B ; inv B.
(* R *) revert dependent x. induction g ; intros x A. now inv A.
destruct x ; inv A ; simpl ; intuition ; omega.
(* L *) apply IHA in H1. simpl in H1. omega.
(* A *) intuition ; auto. Qed.