Tealeaves.Examples.STLC.TypeSoundness
From Tealeaves Require Export
Examples.STLC.Syntax.
Import Syntax.TermNotations.
#[local] Open Scope set_scope.
Implicit Types (x: atom) (τ: typ)
(t u: term) (n: nat) (v: LN) (Γ: ctx).
Ltac gather_atoms ::=
let A := gather_atoms_with (fun s: AtomSet.t ⇒ s) in
let B := gather_atoms_with (fun x: atom ⇒ {{ x }}) in
let C := gather_atoms_with (fun t: term ⇒ FV t) in
let D := gather_atoms_with (fun Γ: alist typ ⇒ domset Γ) in
constr:(A ∪ B ∪ C ∪ D).
Examples.STLC.Syntax.
Import Syntax.TermNotations.
#[local] Open Scope set_scope.
Implicit Types (x: atom) (τ: typ)
(t u: term) (n: nat) (v: LN) (Γ: ctx).
Ltac gather_atoms ::=
let A := gather_atoms_with (fun s: AtomSet.t ⇒ s) in
let B := gather_atoms_with (fun x: atom ⇒ {{ x }}) in
let C := gather_atoms_with (fun t: term ⇒ FV t) in
let D := gather_atoms_with (fun Γ: alist typ ⇒ domset Γ) in
constr:(A ∪ B ∪ C ∪ D).
Lemma inversion11: ∀ (τ: typ) (x: atom) (Γ: ctx),
Γ ⊢ tvar (Fr x): τ → (x, τ) ∈ Γ.
Proof.
inversion 1; auto.
Qed.
Lemma inversion12: ∀ (τ: typ) (n: nat) (Γ: ctx),
Γ ⊢ tvar (Bd n): τ → False.
Proof.
inversion 1; auto.
Qed.
(* This is somewhat weak because L should really be (dom Γ) *)
Lemma inversion21: ∀ (τ B: typ) (e: term) (Γ: ctx),
(Γ ⊢ λ τ e: B) →
∃ C, B = τ ⟹ C ∧ ∃ L, ∀ (x: atom),
x `notin` L → Γ ++ x ¬ τ ⊢ e '(x): C.
Proof.
introv J.
inversion J; subst.
∃ τ2. split; auto; ∃ L; auto.
Qed.
Γ ⊢ tvar (Fr x): τ → (x, τ) ∈ Γ.
Proof.
inversion 1; auto.
Qed.
Lemma inversion12: ∀ (τ: typ) (n: nat) (Γ: ctx),
Γ ⊢ tvar (Bd n): τ → False.
Proof.
inversion 1; auto.
Qed.
(* This is somewhat weak because L should really be (dom Γ) *)
Lemma inversion21: ∀ (τ B: typ) (e: term) (Γ: ctx),
(Γ ⊢ λ τ e: B) →
∃ C, B = τ ⟹ C ∧ ∃ L, ∀ (x: atom),
x `notin` L → Γ ++ x ¬ τ ⊢ e '(x): C.
Proof.
introv J.
inversion J; subst.
∃ τ2. split; auto; ∃ L; auto.
Qed.
Inversion principle for abs where we may assume the abstraction has arrow type
Lemma inversion22: ∀ (τ τ': typ) (e: term) (Γ: ctx),
Γ ⊢ λ τ e: τ ⟹ τ' →
∃ L, ∀ (x: atom),
x `notin` L →
Γ ++ x ¬ τ ⊢ e '(x: term): τ'.
Proof.
introv J. apply inversion21 in J.
destruct J as [C [H1 H2]].
assert (τ' = C) by (inversion H1; auto); subst.
assumption.
Qed.
Lemma inversion3: ∀ (τ: typ) (Γ: ctx) (t1 t2: term),
(Γ ⊢ ⟨t1⟩ (t2): τ) →
∃ τ', (Γ ⊢ t1: τ' ⟹ τ)
∧ (Γ ⊢ t2: τ').
Proof.
introv J; inversion J; subst; eauto.
Qed.
Γ ⊢ λ τ e: τ ⟹ τ' →
∃ L, ∀ (x: atom),
x `notin` L →
Γ ++ x ¬ τ ⊢ e '(x: term): τ'.
Proof.
introv J. apply inversion21 in J.
destruct J as [C [H1 H2]].
assert (τ' = C) by (inversion H1; auto); subst.
assumption.
Qed.
Lemma inversion3: ∀ (τ: typ) (Γ: ctx) (t1 t2: term),
(Γ ⊢ ⟨t1⟩ (t2): τ) →
∃ τ', (Γ ⊢ t1: τ' ⟹ τ)
∧ (Γ ⊢ t2: τ').
Proof.
introv J; inversion J; subst; eauto.
Qed.
Theorem j_ctx_wf: ∀ Γ (t: term) (τ: typ),
Γ ⊢ t: τ → uniq Γ.
Proof.
introv J; typing_induction.
- assumption.
- specialize_freshly IHbody.
now autorewrite with tea_rw_uniq in IHbody.
- assumption.
Qed.
Theorem j_wf: ∀ Γ (t: term) (τ: typ),
Γ ⊢ t: τ → FV t ⊆ domset Γ.
Proof.
introv J. typing_induction.
- simplify_LN.
apply in_in_domset in Hin.
fsetdec.
- specialize_freshly IHbody.
simplify_LN.
assert (step1: FV body ⊆ FV (body '(e: term)))
by apply (FV_open_lower (Binddt_TU := Binddt_STLC)).
assert (step2: ∀ x, x `in` FV body → x `in` (domset (Γ ++ e ¬ τ1)))
by fsetdec.
intros x xin.
assert (x ≠ e) by fsetdec.
specialize (step2 x xin).
rewrite domset_app in step2.
rewrite domset_one in step2.
fsetdec.
- simplify_LN.
fsetdec.
Qed.
Theorem lc_lam: ∀ (L: AtomSet.t) (t: term) (X: typ),
(∀ x: atom, ¬ x `in` L → LC (t '(x: term))) →
LC (λ X t).
Proof.
introv HLC.
simplify_LN.
specialize_freshly HLC.
change (fvar e) with (ret (Fr e)) in HLC.
rewrite <- lc_open_var in HLC.
assumption.
Qed.
Theorem j_lc: ∀ Γ t τ,
Γ ⊢ t: τ → LC t.
Proof.
introv J. typing_induction.
- simplify_LN. exact I.
- pick fresh y excluding L and apply lc_lam.
apply IHbody; auto.
- simplify_LN. split; assumption.
Qed.
Theorem weakening: ∀ Γ1 Γ2 Γ' (t: term) (τ: typ),
uniq Γ' →
disjoint Γ' (Γ1 ++ Γ2) →
(Γ1 ++ Γ2 ⊢ t: τ) →
(Γ1 ++ Γ' ++ Γ2 ⊢ t: τ).
Proof.
introv Huq Hdj J.
remember (Γ1 ++ Γ2) as Γrem.
generalize dependent Γ2.
typing_induction; intros Γ2 HeqΓ; subst.
- apply j_var.
{ autorewrite with tea_rw_uniq tea_rw_disj in ×.
rewrite disjoint_sym.
preprocess; intuition. }
simpl_list in ×.
intuition.
- pick fresh y and apply j_abs.
specialize_cof IHbody y.
simpl_alist in IHbody.
simpl_alist.
apply IHbody.
{ autorewrite with tea_rw_disj in ×.
split; try easy; try split; try easy.
fsetdec. }
{ reflexivity. }
- eauto using j_app.
Qed.
Corollary weakening_r: ∀ Γ1 (t: term) (τ: typ),
(Γ1 ⊢ t: τ) →
∀ Γ2, uniq Γ2 → disjoint Γ1 Γ2 → Γ1 ++ Γ2 ⊢ t: τ.
Proof.
intros.
rewrite <- (List.app_nil_r Γ1) in H.
rewrite <- (List.app_nil_r (Γ1 ++ Γ2)).
rewrite <- List.app_assoc.
apply weakening; auto.
List.simpl_list.
eauto with tea_alist.
Qed.
Theorem substitution: ∀ Γ1 Γ2 x t u τ1 τ2,
(Γ1 ++ x ¬ τ1 ++ Γ2 ⊢ t: τ2) →
(Γ1 ⊢ u: τ1) →
Γ1 ++ Γ2 ⊢ t '{x ~> u}: τ2.
Proof.
introv Jt Ju.
specialize (j_ctx_wf (Γ1 ++ x ¬ τ1 ++ Γ2)); intro Hwf.
assert (LC u) by (eauto using j_lc).
remember (Γ1 ++ x ¬ τ1 ++ Γ2) as Γrem.
generalize dependent Γ2.
typing_induction_on Jt; intros Γ2 HeqΓ.
- compare values x and x0.
+ simplify_subst.
simpl_local.
assert (τ = τ1) by eauto using binds_mid_eq; subst.
apply weakening_r.
{ compare values x0 and x0. }
{ autorewrite with tea_rw_uniq tea_rw_disj in ×.
intuition. }
{ autorewrite with tea_rw_uniq tea_rw_disj in ×.
intuition. }
+ simplify_LN. apply j_var.
{ autorewrite with tea_rw_uniq tea_rw_disj in ×.
intuition. }
{ eauto using binds_remove_mid. }
- simplify_subst.
apply j_abs with (L := L ∪ domset Γ ∪ {{x}}).
intros_cof IHbody.
change (fvar e) with (ret (Fr e)).
rewrite <- subst_open_var.
+ simpl_alist in ×.
eapply IHbody.
× eauto using j_ctx_wf.
× subst. now simpl_alist.
+ fsetdec.
+ auto.
- simplify_LN. eauto using j_app.
Qed.
Corollary substitution_r: ∀ Γ (x: atom) (t u: term) (A B: typ),
(Γ ++ x ¬ A ⊢ t: B) →
(Γ ⊢ u: A) →
(Γ ⊢ t '{x ~> u}: B).
Proof.
introv Jt Ju.
change_alist (Γ ++ x ¬ A ++ nil) in Jt.
change_alist (Γ ++ nil).
eapply substitution; eauto.
Qed.
Inductive value: term → Prop :=
| value_abs: ∀ X t, value (λ X t).
Inductive beta_step: term → term → Prop :=
| beta_app_l: ∀ (t1 t2 t1': term),
beta_step t1 t1' →
beta_step (⟨t1⟩ (t2)) (⟨t1'⟩(t2))
| beta_app_r: ∀ (t1 t2 t2': term),
beta_step t2 t2' →
beta_step (⟨t1⟩(t2)) (⟨t1⟩(t2'))
| beta_beta: ∀ τ t u,
beta_step (⟨λ τ t⟩(u)) (t '(u)).
Theorem subject_reduction_step: ∀ (t t': term) Γ A,
Γ ⊢ t: A → beta_step t t' → Γ ⊢ t': A.
Proof.
introv J Hstep.
generalize dependent t'.
typing_induction; intros t' Hstep.
- inversion Hstep.
- inversion Hstep.
- inversion Hstep.
+ subst. eauto using j_app.
+ subst. eauto using j_app.
+ subst.
apply inversion21 in J1.
destruct J1 as [C [hyp1 [L hyp2]]].
inversion hyp1; subst.
specialize_freshly hyp2.
rewrite (open_spec _ _ e).
{ eauto using substitution_r. }
{ fsetdec. }
Qed.
Theorem progress: ∀ (t: term) τ1,
nil ⊢ t: τ1 → value t ∨ (∃ t', beta_step t t').
Proof.
introv J. remember [] as ctx.
typing_induction; subst.
- inversion Hin.
- left. constructor.
- specialize (IHJ1 eq_refl).
specialize (IHJ2 eq_refl).
destruct IHJ1.
+ right. inversion H; subst.
∃ (t '(t2)). constructor.
+ right.
destruct H as [t1' Hstep'].
eauto using beta_app_l.
Qed.
Theorem soundness: ∀ (t: term) τ1,
nil ⊢ t: τ1 → value t ∨ (∃ t', beta_step t t').
Proof.
introv J. remember [] as ctx.
typing_induction; subst.
- inversion Hin.
- left. constructor.
- specialize (IHJ1 eq_refl).
specialize (IHJ2 eq_refl).
destruct IHJ1.
+ right. inversion H; subst.
∃ (t '(t2)). constructor.
+ right.
destruct H as [t1' Hstep'].
eauto using beta_app_l.
Qed.
Γ ⊢ t: τ → uniq Γ.
Proof.
introv J; typing_induction.
- assumption.
- specialize_freshly IHbody.
now autorewrite with tea_rw_uniq in IHbody.
- assumption.
Qed.
Theorem j_wf: ∀ Γ (t: term) (τ: typ),
Γ ⊢ t: τ → FV t ⊆ domset Γ.
Proof.
introv J. typing_induction.
- simplify_LN.
apply in_in_domset in Hin.
fsetdec.
- specialize_freshly IHbody.
simplify_LN.
assert (step1: FV body ⊆ FV (body '(e: term)))
by apply (FV_open_lower (Binddt_TU := Binddt_STLC)).
assert (step2: ∀ x, x `in` FV body → x `in` (domset (Γ ++ e ¬ τ1)))
by fsetdec.
intros x xin.
assert (x ≠ e) by fsetdec.
specialize (step2 x xin).
rewrite domset_app in step2.
rewrite domset_one in step2.
fsetdec.
- simplify_LN.
fsetdec.
Qed.
Theorem lc_lam: ∀ (L: AtomSet.t) (t: term) (X: typ),
(∀ x: atom, ¬ x `in` L → LC (t '(x: term))) →
LC (λ X t).
Proof.
introv HLC.
simplify_LN.
specialize_freshly HLC.
change (fvar e) with (ret (Fr e)) in HLC.
rewrite <- lc_open_var in HLC.
assumption.
Qed.
Theorem j_lc: ∀ Γ t τ,
Γ ⊢ t: τ → LC t.
Proof.
introv J. typing_induction.
- simplify_LN. exact I.
- pick fresh y excluding L and apply lc_lam.
apply IHbody; auto.
- simplify_LN. split; assumption.
Qed.
Theorem weakening: ∀ Γ1 Γ2 Γ' (t: term) (τ: typ),
uniq Γ' →
disjoint Γ' (Γ1 ++ Γ2) →
(Γ1 ++ Γ2 ⊢ t: τ) →
(Γ1 ++ Γ' ++ Γ2 ⊢ t: τ).
Proof.
introv Huq Hdj J.
remember (Γ1 ++ Γ2) as Γrem.
generalize dependent Γ2.
typing_induction; intros Γ2 HeqΓ; subst.
- apply j_var.
{ autorewrite with tea_rw_uniq tea_rw_disj in ×.
rewrite disjoint_sym.
preprocess; intuition. }
simpl_list in ×.
intuition.
- pick fresh y and apply j_abs.
specialize_cof IHbody y.
simpl_alist in IHbody.
simpl_alist.
apply IHbody.
{ autorewrite with tea_rw_disj in ×.
split; try easy; try split; try easy.
fsetdec. }
{ reflexivity. }
- eauto using j_app.
Qed.
Corollary weakening_r: ∀ Γ1 (t: term) (τ: typ),
(Γ1 ⊢ t: τ) →
∀ Γ2, uniq Γ2 → disjoint Γ1 Γ2 → Γ1 ++ Γ2 ⊢ t: τ.
Proof.
intros.
rewrite <- (List.app_nil_r Γ1) in H.
rewrite <- (List.app_nil_r (Γ1 ++ Γ2)).
rewrite <- List.app_assoc.
apply weakening; auto.
List.simpl_list.
eauto with tea_alist.
Qed.
Theorem substitution: ∀ Γ1 Γ2 x t u τ1 τ2,
(Γ1 ++ x ¬ τ1 ++ Γ2 ⊢ t: τ2) →
(Γ1 ⊢ u: τ1) →
Γ1 ++ Γ2 ⊢ t '{x ~> u}: τ2.
Proof.
introv Jt Ju.
specialize (j_ctx_wf (Γ1 ++ x ¬ τ1 ++ Γ2)); intro Hwf.
assert (LC u) by (eauto using j_lc).
remember (Γ1 ++ x ¬ τ1 ++ Γ2) as Γrem.
generalize dependent Γ2.
typing_induction_on Jt; intros Γ2 HeqΓ.
- compare values x and x0.
+ simplify_subst.
simpl_local.
assert (τ = τ1) by eauto using binds_mid_eq; subst.
apply weakening_r.
{ compare values x0 and x0. }
{ autorewrite with tea_rw_uniq tea_rw_disj in ×.
intuition. }
{ autorewrite with tea_rw_uniq tea_rw_disj in ×.
intuition. }
+ simplify_LN. apply j_var.
{ autorewrite with tea_rw_uniq tea_rw_disj in ×.
intuition. }
{ eauto using binds_remove_mid. }
- simplify_subst.
apply j_abs with (L := L ∪ domset Γ ∪ {{x}}).
intros_cof IHbody.
change (fvar e) with (ret (Fr e)).
rewrite <- subst_open_var.
+ simpl_alist in ×.
eapply IHbody.
× eauto using j_ctx_wf.
× subst. now simpl_alist.
+ fsetdec.
+ auto.
- simplify_LN. eauto using j_app.
Qed.
Corollary substitution_r: ∀ Γ (x: atom) (t u: term) (A B: typ),
(Γ ++ x ¬ A ⊢ t: B) →
(Γ ⊢ u: A) →
(Γ ⊢ t '{x ~> u}: B).
Proof.
introv Jt Ju.
change_alist (Γ ++ x ¬ A ++ nil) in Jt.
change_alist (Γ ++ nil).
eapply substitution; eauto.
Qed.
Inductive value: term → Prop :=
| value_abs: ∀ X t, value (λ X t).
Inductive beta_step: term → term → Prop :=
| beta_app_l: ∀ (t1 t2 t1': term),
beta_step t1 t1' →
beta_step (⟨t1⟩ (t2)) (⟨t1'⟩(t2))
| beta_app_r: ∀ (t1 t2 t2': term),
beta_step t2 t2' →
beta_step (⟨t1⟩(t2)) (⟨t1⟩(t2'))
| beta_beta: ∀ τ t u,
beta_step (⟨λ τ t⟩(u)) (t '(u)).
Theorem subject_reduction_step: ∀ (t t': term) Γ A,
Γ ⊢ t: A → beta_step t t' → Γ ⊢ t': A.
Proof.
introv J Hstep.
generalize dependent t'.
typing_induction; intros t' Hstep.
- inversion Hstep.
- inversion Hstep.
- inversion Hstep.
+ subst. eauto using j_app.
+ subst. eauto using j_app.
+ subst.
apply inversion21 in J1.
destruct J1 as [C [hyp1 [L hyp2]]].
inversion hyp1; subst.
specialize_freshly hyp2.
rewrite (open_spec _ _ e).
{ eauto using substitution_r. }
{ fsetdec. }
Qed.
Theorem progress: ∀ (t: term) τ1,
nil ⊢ t: τ1 → value t ∨ (∃ t', beta_step t t').
Proof.
introv J. remember [] as ctx.
typing_induction; subst.
- inversion Hin.
- left. constructor.
- specialize (IHJ1 eq_refl).
specialize (IHJ2 eq_refl).
destruct IHJ1.
+ right. inversion H; subst.
∃ (t '(t2)). constructor.
+ right.
destruct H as [t1' Hstep'].
eauto using beta_app_l.
Qed.
Theorem soundness: ∀ (t: term) τ1,
nil ⊢ t: τ1 → value t ∨ (∃ t', beta_step t t').
Proof.
introv J. remember [] as ctx.
typing_induction; subst.
- inversion Hin.
- left. constructor.
- specialize (IHJ1 eq_refl).
specialize (IHJ2 eq_refl).
destruct IHJ1.
+ right. inversion H; subst.
∃ (t '(t2)). constructor.
+ right.
destruct H as [t1' Hstep'].
eauto using beta_app_l.
Qed.