Set Implicit Arguments.

Inductive tm : Type :=
| tmV : nat -> tm (* variable *)
| tmL : tm -> tm -> tm (* lambda *)
| tmA : tm -> tm -> tm (* application *)
| tmF : tm -> tm -> tm (* forall *)
| tmU : nat -> tm. (* universe *)

Inductive free : nat -> tm -> Prop :=
| freeV x : free x (tmV x)
| freeL x s t : free x s \/ free (S x) t -> free x (tmL s t)
| freeA x s t : free x s \/ free x t -> free x (tmA s t)
| freeF x s t : free x s \/ free (S x) t -> free x (tmF s t).

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

Fixpoint raise (d : nat) (t : tm) : tm :=
  match t with
    | tmV y => tmV (if blt y d then y else S y)
    | tmL u v => tmL (raise d u) (raise (S d) v)
    | tmA u v => tmA (raise d u) (raise d v)
    | tmF u v => tmF (raise d u) (raise (S d) v)
    | tmU n => tmU n
  end.

Fixpoint subst (d : nat) (s t : tm) : tm :=
  match s with
    | tmV y => if blt y d then tmV y
               else if blt d y then tmV (pred y)
                    else t
    | tmL u v => tmL (subst d u t) (subst (S d) v (raise 0 t))
    | tmA u v => tmA (subst d u t) (subst d v t)
    | tmF u v => tmF (subst d u t) (subst (S d) v (raise 0 t))
    | tmU n => tmU n
  end.

Inductive step : tm -> tm -> Prop :=
| stepB s t u : step (tmA (tmL s t) u) (subst 0 t u)
| stepLL s s' t : step s s' -> step (tmL s t) (tmL s' t)
| stepLR s t t' : step t t' -> step (tmL s t) (tmL s t')
| stepAL s s' t : step s s' -> step (tmA s t) (tmA s' t)
| stepAR s t t' : step t t' -> step (tmA s t) (tmA s t')
| stepFL s s' t : step s s' -> step (tmF s t) (tmF s' t)
| stepFR s t t' : step t t' -> step (tmF s t) (tmF s t').

Inductive red : tm -> tm -> Prop :=
| redR t : red t t
| redS s t u : step s t -> red t u -> red s u.

Inductive convertible : tm -> tm -> Prop :=
| convR t : convertible t t
| convS s t u : step s t -> convertible t u -> convertible s u
| convS' s t u : step t s -> convertible t u -> convertible s u.

Inductive terminates : tm -> Prop :=
terI s : (forall t, step s t -> terminates t) -> terminates s.

Inductive subtype : tm -> tm -> Prop :=
| subtypeU m n : blt m n = true -> subtype (tmU m) (tmU n)
| subtypeF s t t' : subtype t t' -> subtype (tmF s t) (tmF s t').

Definition context := list tm.

Inductive typeC : context -> nat -> tm -> Prop :=
| typeCO g t : typeC (cons t g) 0 (raise 0 t)
| typeCS g x t s : typeC g x t -> typeC (cons s g) (S x) (raise 0 t).

Inductive type : context -> tm -> tm -> Prop :=
| typeCE :
  type nil (tmU 0) (tmU 1)
| typeCV g t n:
  type g t (tmU n) ->
  type (cons t g) (tmU 0) (tmU 1)
| typeV g x t :
  typeC g x t ->
  type g (tmU 0) (tmU 1) ->
  type g (tmV x) t
| typeL g s t u :
  type (cons s g) t u ->
  type g (tmL s t) (tmF s u)
| typeA g s t u v :
  type g s (tmF u v) ->
  type g t u ->
  type g (tmA s t) (subst 0 v t)
| typeF g s t n :
  type g s (tmU n) ->
  type (cons s g) t (tmU n) ->
  type g (tmF s t) (tmU n)
| typeU g n :
  type g (tmU 0) (tmU 1) ->
  type g (tmU n) (tmU (S n))
| typeCon g s t t' n :
  convertible t t' ->
  type g s t ->
  type g t' (tmU n) ->
  type g s t'
| typeSub g s t t' :
  subtype t t' ->
  type g s t ->
  type g s t'.

Lemma confluence s t1 t2 :
red s t1 -> red s t2 -> exists u, red t1 u /\ red t2 u.
Admitted.

Lemma type_free g s t x :
type g s t -> free x s -> exists u, typeC g x u.
Admitted.

Lemma propagation g s t :
type g s t -> exists n, type g t (tmU n).
Admitted.

Lemma preservation g s t s' :
type g s t -> step s s' -> type g s' t.
Admitted.

Lemma termination g s t :
type g s t -> terminates s.
Admitted.

Inductive decidable (X : Prop) : Type :=
| decP : X -> decidable X
| decN : ~ X -> decidable X.

Lemma decidable_convertible g s t s' t' :
type g s t -> type g s' t' -> decidable (convertible s s').
Admitted.

Lemma decidable_type g s t :
decidable (type g s t).
Admitted.

Compute
subst 0
(tmL (tmU 0) (tmL (tmF (tmV 0) (tmV 0)) (tmA (tmV 0) (tmV 2))))
(tmF (tmV 7) (tmV 1)).

(* Examples *)

(*** f : U2 -> U0 |- f : U2 -> U2 ***)
Goal type (cons (tmF (tmU 2) (tmU 0)) nil) (tmV 0) (tmF (tmU 2) (tmU 2)).
Proof with now eauto using type, typeC, subtype.
apply typeSub with (t := (tmF (tmU 2) (tmU 0))).
trivial...
apply typeV. apply typeCO.
apply typeCV with (n := 3).
apply typeF.
trivial...
apply typeSub with (t := (tmU 1))...
Qed.

(*** X:U0,f:X -> X,x:X |- f x : X ***)
Goal type (cons (tmV 1) (cons (tmF (tmV 0) (tmV 1)) (cons (tmU 0) nil))) (tmA (tmV 1) (tmV 0)) (tmV 2).
assert (G1:type (tmU 0 :: nil)%list (tmU 0) (tmU 1)).
apply typeCV with (n := 1).
apply typeCE.
assert (G2:type (tmF (tmV 0) (tmV 1) :: tmU 0 :: nil)%list (tmU 0) (tmU 1)).
apply typeCV with (n := 0).
apply typeF.
apply typeV. apply typeCO.
assumption.
apply typeV. apply typeCS with (t := (tmU 0)). apply typeCO.
apply typeCV with (n := 0).
apply typeV. apply typeCO.
assumption.
assert (G3:type (tmV 1 :: tmF (tmV 0) (tmV 1) :: tmU 0 :: nil)%list (tmU 0) (tmU 1)).
apply typeCV with (n := 0).
apply typeV. apply typeCS with (t := (tmU 0)). apply typeCO.
assumption.
apply typeA with (u := (tmV 2)) (v := (tmV 3)).
apply typeV.
apply typeCS with (t := (tmF (tmV 1) (tmV 2))).
apply typeCO.
assumption.
apply typeV. apply typeCO.
assumption.
Qed.