Library Ftypesystem
Require Import Omega.
Require Import List.
Require Import list.
Require Import Flanguage.
Require Export typesystem.
Inductive jterm M : type_env → coer_env → term_env → term → type → Prop :=
| JVar : ∀ H Z G k x t,
(1 ≤ M → jterm_env M H Z G) →
nth x G Top = t →
jterm M H Z G (Var_x k x) t
| JLam : ∀ H Z G k a t s,
(M ≠ 1 → jtype M H Z t) →
jterm M H Z (t :: G) a s →
jterm M H Z G (Lam k a) (Arr t s)
| JApp : ∀ H Z G k 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 k a b) s
| JPair : ∀ H Z G k a b t s,
jterm M H Z G a t →
jterm M H Z G b s →
jterm M H Z G (Pair k a b) (Prod t s)
| JFst : ∀ H Z G k a t s,
jterm M H Z G a (Prod t s) →
jterm M H Z G (Fst k a) t
| JSnd : ∀ H Z G k a t s,
jterm M H Z G a (Prod t s) →
jterm M H Z G (Snd k 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
.
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.
Require Import List.
Require Import list.
Require Import Flanguage.
Require Export typesystem.
Inductive jterm M : type_env → coer_env → term_env → term → type → Prop :=
| JVar : ∀ H Z G k x t,
(1 ≤ M → jterm_env M H Z G) →
nth x G Top = t →
jterm M H Z G (Var_x k x) t
| JLam : ∀ H Z G k a t s,
(M ≠ 1 → jtype M H Z t) →
jterm M H Z (t :: G) a s →
jterm M H Z G (Lam k a) (Arr t s)
| JApp : ∀ H Z G k 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 k a b) s
| JPair : ∀ H Z G k a b t s,
jterm M H Z G a t →
jterm M H Z G b s →
jterm M H Z G (Pair k a b) (Prod t s)
| JFst : ∀ H Z G k a t s,
jterm M H Z G a (Prod t s) →
jterm M H Z G (Fst k a) t
| JSnd : ∀ H Z G k a t s,
jterm M H Z G a (Prod t s) →
jterm M H Z G (Snd k 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
.
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.