Set Implicit Arguments.
Require Import Decidable Metatheory
STLC_Dec_Definitions
STLC_Dec_Infrastructure
STLC_Dec_Soundness.
Lemma eq_typ_dec : forall (T T' : typ),
sumbool (T = T') (T <> T').
Proof.
unfold decidable. decide equality. use eq_var_dec.
Qed.
Lemma binds_typ_dec : forall x (T : typ) E,
decidable (binds x T E).
Proof.
intros. apply binds_dec. apply eq_typ_dec.
Qed.
Lemma typing_rename : forall x y E t T U,
x \notin (fv t \u dom E) ->
y \notin (fv t \u dom E) ->
(E & x ~ U) |= (t ^ x) ~: T ->
(E & y ~ U) |= (t ^ y) ~: T.
Proof.
introv Frx Fry Typ.
asserts* K (ok (E & x ~ U)). inversions K.
destruct (x == y). subst*.
rewrite~ (@subst_intro x).
apply_empty* typing_subst.
poses P (@typing_weaken (x ~ U) E (y ~ U)).
simpls. apply* P; env_fix.
apply* ok_push.
apply* typing_var.
Qed.
Lemma typing_dec' : forall t E T, term t -> ok E ->
decidable (E |= t ~: T).
Proof.
introv Wf Ok. gen T E.
induction Wf; intros.
destruct (@binds_typ_dec x T E).
left. apply* typing_var.
right. intros K. inversions* K.
destruct T. right. intros K. inversions K.
pick_fresh x.
forward~ (H0 x) as H1. clear H0.
forward~ (H1 T2 (E & x ~ T1)) as [Typ1 | NTyp1 ]. clear H1.
left. apply_fresh* typing_abs as y. apply* (@typing_rename x).
right. intros Typ1. inversions Typ1. apply NTyp1.
pick_fresh y. forward~ (H4 y) as K.
apply* (@typing_rename y).
forward~ (IHWf1 (typ_arrow T T0) E) as [Typ1 | NTyp1]. clear IHWf1.
forward~ (IHWf2 T E) as [Typ2 | NTyp2]. clear IHWf2.
left. apply* typing_app.
right. intros K. inversions* K.
right. intros K. inversions* K.
Qed.