Library Ltypesystem

Require Import Omega.
Require Import List.

Require Import list.
Require Import Llanguage.
Require Export typesystem.

Inductive jterm M : type_env → coer_env → term_env → term → type → Prop :=
| JVar : ∀ H Z G x t,
           (1 ≤ M → jterm_env M H Z G) →
           nth x G Top = t →
           jterm M H Z G (Var_x x) t
| JLam : ∀ H Z G a t s,
           (M ≠ 1 → jtype M H Z t) →
           jterm M H Z (t :: G) a s →
           jterm M H Z G (Lam a) (Arr t s)
| JApp : ∀ H Z G a b t s,
           jterm M H Z G a (Arr t s) →
           jterm M H Z G b t →
           jterm M H Z G (App a b) s
| JPair : ∀ H Z G a b t s,
            jterm M H Z G a t →
            jterm M H Z G b s →
            jterm M H Z G (Pair a b) (Prod t s)
| JFst : ∀ H Z G a t s,
           jterm M H Z G a (Prod t s) →
           jterm M H Z G (Fst a) t
| JSnd : ∀ H Z G a t s,
           jterm M H Z G a (Prod t s) →
           jterm M H Z G (Snd a) s
| JCoer : ∀ dH H dZ Z G a t s,
            (1 ≤ M → jterm_env M H Z G) →
            jcoer M H Z nil nil dH dZ t s →
            jterm M (dH + H) (dZ ++ dmap (lift dH 0) Z) (map (lift dH 0) G) a t →
            jterm M H Z G a s
.

Ltac jterm_induction H :=
  induction H; intros;
  [ apply JVar
  | apply JLam
  | eapply JApp
  | apply JPair
  | eapply JFst
  | eapply JSnd
  | eapply JCoer ].

Lemma jterm_extract_jterm_env : ∀ {M H Z G a t}, 1 ≤ M →
  jterm M H Z G a t → jterm_env M H Z G.
Proof.
intros M H Z G a t M1M HZGat; induction HZGat; auto.
destruct IHHZGat. inversion H2; auto.
Qed.

Lemma jterm_extract_jtype : ∀ {M H Z G a t}, 1 ≤ M →
  jterm M H Z G a t → jtype M H Z t.
Proof.
intros M H Z G a t M1M HZGat.
induction HZGat;
repeat (match goal with
  | H1 : 1 ≤ M → _ |- _ ⇒ pose proof (H1 M1M); clear H1
  | |- jtype _ _ _ ?t ⇒ (is_var t; fail 1) || constructor
  | H1 : jtype _ _ _ ?t |- _ ⇒ (is_var t; fail 1) || inversion H1; clear H1
end; auto).
  destruct H2; subst; apply Forall_nth; auto; apply JTTop.
  pose proof (jterm_extract_jterm_env M1M HZGat) as [? ?].
  inversion H2; auto.
  apply (jcoer_extract_right_type M1M H1).
Qed.