Safety
Require Export Coq.Program.Equality.
Require Export Definitions Infrastructure.
Require Export Metalib.Metatheory.
Ltac gather_atoms ::=
let A := gather_atoms_with (fun x : vars ⇒ x) in
let B := gather_atoms_with (fun x : var ⇒ {{ x }}) in
let C := gather_atoms_with (fun x : ctx ⇒ dom x) in
let D1 := gather_atoms_with (fun x ⇒ fv_trm x) in
constr:(A \u B \u C \u D1).
Notation "G '⊢' N ':' A" := (typing G N A) (at level 40, N at level 59).
Notation "⇑ p" := (t_blame p) (at level 40).
Notation "'λ(' A ')' N" := (t_abs A N) (at level 40).
Notation "N '⦂' A '=>' B '@@' p" := (t_cast N A p B) (at level 40).
Notation "'{{{' D '→' E '}}}'" := (dtyp_arrow D E) (at level 40).
Lemma compat_sym : ∀ A B,
compat A B →
compat B A.
Proof.
induction 1; eauto.
Qed.
Hint Resolve compat_sym : core.
Lemma typing_weakening : ∀ (F E G : ctx) (N : trm) (A : typ),
(F ++ G) ⊢ N : A →
uniq (F ++ E ++ G) →
(F ++ E ++ G) ⊢ N : A.
Proof.
intros until 1. dependent induction H; intros; eauto.
pick fresh x and apply typing_abs.
rewrite_env ((x ¬ A ++ F) ++ E ++ G).
apply_first_hyp; simpl_env; auto.
pick fresh x and apply typing_case; eauto.
rewrite_env ((x ¬ (typ_def D) ++ F) ++ E ++ G).
apply_first_hyp; simpl_env; auto.
Qed.
Lemma typing_to_lc_trm : ∀ G N A,
G ⊢ N : A → lc_trm N.
Proof.
intros G N A H. induction H; eauto.
Qed.
Hint Resolve typing_to_lc_trm : core.
Lemma substitution_gen F x B G N M A :
(F ++ x ¬ B ++ G) ⊢ N : A →
G ⊢ M : B →
(F ++ G) ⊢ subst_trm M x N : A.
Proof with eauto.
intros until 1. dependent induction H; intros; simpl subst_trm...
-
destruct (eq_dec x0 x); try subst x0.
+ analyze_binds_uniq H0.
apply typing_weakening with (F := nil)...
+ analyze_binds_uniq H0...
-
pick fresh z and apply typing_abs.
rewrite_env ((z ¬ A ++ F) ++ G).
rewrite subst_trm_open_trm_wrt_trm_var...
apply H0 with (B1 := B)...
-
pick fresh z and apply typing_case; eauto.
rewrite_env ((z ¬ (typ_def D) ++ F) ++ G).
rewrite subst_trm_open_trm_wrt_trm_var...
apply H2 with (B0 := B)...
Qed.
Lemma substitution G x B N M A :
([(x, B)] ++ G) ⊢ N : A →
G ⊢ M : B →
G ⊢ subst_trm M x N : A.
Proof.
intros Ht Hu.
rewrite_env (nil ++ G).
eapply substitution_gen.
simpl_env. eauto. auto.
Qed.
Ltac invert_typing :=
match goal with
| [ H : _ ⊢ _ : _ |- _ ] ⇒
inversion H; subst end.
Ltac solve_pres_ctx :=
invert_typing;
match goal with
| [ IH : ∀ _ : typ, _ ⊢ ?u : _ → _,
Ht : _ ⊢ ?u : _ |- _ ] ⇒
specialize (IH _ Ht) as Heq; inversion Heq;
subst; eauto
end.
Lemma typing_uniq G N A :
G ⊢ N : A → uniq G.
Proof.
induction 1; eauto;
pick_fresh x; eapply uniq_app_2; eauto.
Qed.
Hint Resolve typing_uniq : core.
Lemma preservation : ∀ G N M A,
G ⊢ N : A →
step N M →
G ⊢ M : A.
Proof with eauto.
intros G N M A H J.
generalize dependent A.
induction J; intros; eauto; try solve [solve_pres_ctx].
-
inversion H3...
-
inversion H2. subst. inversion H6. subst.
pick_fresh z. assert (z `notin` L) as Hz by auto.
specialize (H5 z Hz).
pose proof (substitution _ _ _ _ _ _ H5 H8) as Ht.
rewrite (subst_trm_intro z); auto.
-
invert_typing.
inversion H8; subst.
inversion H15; subst.
inversion H11; inversion H13; subst; eauto.
-
invert_typing. eauto.
-
invert_typing.
invert_typing.
constructor.
constructor.
assumption.
inversion H9; subst; eauto.
inversion H4; subst; eauto.
inversion H3; subst; eauto.
-
invert_typing.
invert_typing.
constructor; auto.
inversion H9; subst; eauto.
-
invert_typing.
apply typing_lift.
apply typing_cast; try assumption.
inversion H9; subst; assumption.
-
invert_typing.
assumption.
-
invert_typing. assumption.
-
invert_typing.
inversion H8; subst.
pick_fresh z. assert (z `notin` L) as Hz by auto.
specialize (H11 z Hz).
pose proof (substitution _ _ _ _ _ _ H11 H7) as Ht.
rewrite (subst_trm_intro z); auto.
Qed.
Lemma canonical_forms_arrow V A B :
nil ⊢ V : typ_def ({{{A → B}}}) →
Is_true (is_val_of_trm V) →
(∃ N, V = (λ(A)N)) ∨
(∃ W A' B' A'' B'' p,
Is_true (is_val_of_trm W) ∧
V = W ⦂ typ_def ({{{A' → B'}}}) ⇒ typ_def ({{{A'' → B''}}}) @@ p).
Proof.
intros.
apply Is_true_eq_true in H0.
dependent induction H; try discriminate.
- left. ∃ N. reflexivity.
- right.
inversion H1.
apply andb_true_iff in H3. destruct H3.
apply andb_true_iff in H2. destruct H2.
inversion H0; subst.
× inversion H; subst; try discriminate.
× repeat eexists.
eauto with bool.
Qed.
Fixpoint neglabel_fun (l: label) : label :=
match l with
| (label_name l') ⇒ (label_not_label l')
| (label_not_label l') ⇒ label_name l'
end.
Lemma neglabel_fun_soundness l :
neglabel l (neglabel_fun l).
Proof.
destruct l.
- simpl.
auto.
- simpl.
auto.
Qed.
Lemma neglabel_fun_completenss l l' :
neglabel l l' →
l' = neglabel_fun l.
Proof.
intros Hn.
inversion Hn; auto.
Qed.
Lemma progress N A :
nil ⊢ N : A →
(Is_true (is_val_of_trm N)) ∨
(∃ M, step N M) ∨
(∃ p, N = t_blame p).
Proof.
intros.
dependent induction H; simpl; auto.
-
specialize (IHtyping1 (JMeq_refl nil)) as [s_val | [[L step_s] | [p s_blame]]]; subst; right; left; eauto.
specialize (IHtyping2 (JMeq_refl nil)) as [t_val | [[L' step_t] | [p t_blame]]]; subst.
× ∃ (t_const 0). eauto.
× eauto.
× eauto.
-
specialize (IHtyping1 (JMeq_refl nil)) as [s_val | [[L' step_s] | [p s_blame]]]; subst; eauto; try (right; left; eauto).
specialize (IHtyping2 (JMeq_refl nil)) as [t_val | [[L' step_t] | [p t_blame]]]; subst; eauto; try (right; left; eauto).
pose proof (canonical_forms_arrow _ _ _ H s_val) as [[s0 Elam] | [v1 [V1 [V2 [T1 [T2 [p [Eval Ecast]]]]]]]].
× subst. eauto.
× subst. eexists. eapply step_wrap; eauto.
+ inversion H. eauto.
+ eapply neglabel_fun_soundness.
-
specialize (IHtyping (JMeq_refl nil)) as [s_val | [[L step_s] | [p s_blame]]]; subst; eauto.
-
right. left.
specialize (IHtyping1 (JMeq_refl nil)) as [s_val | [[M' step_s] | [p s_blame]]]; subst; eauto.
× apply Is_true_eq_true in s_val.
inversion H; subst; try discriminate.
+ eexists. eauto.
+ inversion s_val. eexists. eapply step_case_lift; eauto with bool.
+ inversion s_val. apply andb_true_iff in H6. destruct H6. discriminate.
× eexists. eauto.
× eexists. eauto.
-
specialize (IHtyping (JMeq_refl nil)) as [s_val | [[L step_s] | [p2 s_blame]]]; subst; eauto.
apply Is_true_eq_true in s_val.
destruct M; try discriminate.
×
inversion H; subst.
inversion H0; subst; eauto with bool.
×
inversion H; subst.
inversion H0; subst.
inversion H1; subst.
+ right. left. eauto with bool.
+ left. eauto with bool.
×
inversion H; subst.
right. destruct B; eauto.
×
inversion H; subst.
right.
destruct B; eauto with bool.
×
inversion s_val.
apply andb_true_iff in H2. destruct H2.
apply andb_true_iff in H1. destruct H1.
destruct B0; try discriminate.
destruct D; try discriminate.
inversion H; subst.
inversion H0; subst.
+ right. eauto with bool.
+ left. inversion H11; subst; eauto with bool.
-
right. right. eauto.
Qed.
Require Export Definitions Infrastructure.
Require Export Metalib.Metatheory.
Ltac gather_atoms ::=
let A := gather_atoms_with (fun x : vars ⇒ x) in
let B := gather_atoms_with (fun x : var ⇒ {{ x }}) in
let C := gather_atoms_with (fun x : ctx ⇒ dom x) in
let D1 := gather_atoms_with (fun x ⇒ fv_trm x) in
constr:(A \u B \u C \u D1).
Notation "G '⊢' N ':' A" := (typing G N A) (at level 40, N at level 59).
Notation "⇑ p" := (t_blame p) (at level 40).
Notation "'λ(' A ')' N" := (t_abs A N) (at level 40).
Notation "N '⦂' A '=>' B '@@' p" := (t_cast N A p B) (at level 40).
Notation "'{{{' D '→' E '}}}'" := (dtyp_arrow D E) (at level 40).
Lemma compat_sym : ∀ A B,
compat A B →
compat B A.
Proof.
induction 1; eauto.
Qed.
Hint Resolve compat_sym : core.
Lemma typing_weakening : ∀ (F E G : ctx) (N : trm) (A : typ),
(F ++ G) ⊢ N : A →
uniq (F ++ E ++ G) →
(F ++ E ++ G) ⊢ N : A.
Proof.
intros until 1. dependent induction H; intros; eauto.
pick fresh x and apply typing_abs.
rewrite_env ((x ¬ A ++ F) ++ E ++ G).
apply_first_hyp; simpl_env; auto.
pick fresh x and apply typing_case; eauto.
rewrite_env ((x ¬ (typ_def D) ++ F) ++ E ++ G).
apply_first_hyp; simpl_env; auto.
Qed.
Lemma typing_to_lc_trm : ∀ G N A,
G ⊢ N : A → lc_trm N.
Proof.
intros G N A H. induction H; eauto.
Qed.
Hint Resolve typing_to_lc_trm : core.
Lemma substitution_gen F x B G N M A :
(F ++ x ¬ B ++ G) ⊢ N : A →
G ⊢ M : B →
(F ++ G) ⊢ subst_trm M x N : A.
Proof with eauto.
intros until 1. dependent induction H; intros; simpl subst_trm...
-
destruct (eq_dec x0 x); try subst x0.
+ analyze_binds_uniq H0.
apply typing_weakening with (F := nil)...
+ analyze_binds_uniq H0...
-
pick fresh z and apply typing_abs.
rewrite_env ((z ¬ A ++ F) ++ G).
rewrite subst_trm_open_trm_wrt_trm_var...
apply H0 with (B1 := B)...
-
pick fresh z and apply typing_case; eauto.
rewrite_env ((z ¬ (typ_def D) ++ F) ++ G).
rewrite subst_trm_open_trm_wrt_trm_var...
apply H2 with (B0 := B)...
Qed.
Lemma substitution G x B N M A :
([(x, B)] ++ G) ⊢ N : A →
G ⊢ M : B →
G ⊢ subst_trm M x N : A.
Proof.
intros Ht Hu.
rewrite_env (nil ++ G).
eapply substitution_gen.
simpl_env. eauto. auto.
Qed.
Ltac invert_typing :=
match goal with
| [ H : _ ⊢ _ : _ |- _ ] ⇒
inversion H; subst end.
Ltac solve_pres_ctx :=
invert_typing;
match goal with
| [ IH : ∀ _ : typ, _ ⊢ ?u : _ → _,
Ht : _ ⊢ ?u : _ |- _ ] ⇒
specialize (IH _ Ht) as Heq; inversion Heq;
subst; eauto
end.
Lemma typing_uniq G N A :
G ⊢ N : A → uniq G.
Proof.
induction 1; eauto;
pick_fresh x; eapply uniq_app_2; eauto.
Qed.
Hint Resolve typing_uniq : core.
Lemma preservation : ∀ G N M A,
G ⊢ N : A →
step N M →
G ⊢ M : A.
Proof with eauto.
intros G N M A H J.
generalize dependent A.
induction J; intros; eauto; try solve [solve_pres_ctx].
-
inversion H3...
-
inversion H2. subst. inversion H6. subst.
pick_fresh z. assert (z `notin` L) as Hz by auto.
specialize (H5 z Hz).
pose proof (substitution _ _ _ _ _ _ H5 H8) as Ht.
rewrite (subst_trm_intro z); auto.
-
invert_typing.
inversion H8; subst.
inversion H15; subst.
inversion H11; inversion H13; subst; eauto.
-
invert_typing. eauto.
-
invert_typing.
invert_typing.
constructor.
constructor.
assumption.
inversion H9; subst; eauto.
inversion H4; subst; eauto.
inversion H3; subst; eauto.
-
invert_typing.
invert_typing.
constructor; auto.
inversion H9; subst; eauto.
-
invert_typing.
apply typing_lift.
apply typing_cast; try assumption.
inversion H9; subst; assumption.
-
invert_typing.
assumption.
-
invert_typing. assumption.
-
invert_typing.
inversion H8; subst.
pick_fresh z. assert (z `notin` L) as Hz by auto.
specialize (H11 z Hz).
pose proof (substitution _ _ _ _ _ _ H11 H7) as Ht.
rewrite (subst_trm_intro z); auto.
Qed.
Lemma canonical_forms_arrow V A B :
nil ⊢ V : typ_def ({{{A → B}}}) →
Is_true (is_val_of_trm V) →
(∃ N, V = (λ(A)N)) ∨
(∃ W A' B' A'' B'' p,
Is_true (is_val_of_trm W) ∧
V = W ⦂ typ_def ({{{A' → B'}}}) ⇒ typ_def ({{{A'' → B''}}}) @@ p).
Proof.
intros.
apply Is_true_eq_true in H0.
dependent induction H; try discriminate.
- left. ∃ N. reflexivity.
- right.
inversion H1.
apply andb_true_iff in H3. destruct H3.
apply andb_true_iff in H2. destruct H2.
inversion H0; subst.
× inversion H; subst; try discriminate.
× repeat eexists.
eauto with bool.
Qed.
Fixpoint neglabel_fun (l: label) : label :=
match l with
| (label_name l') ⇒ (label_not_label l')
| (label_not_label l') ⇒ label_name l'
end.
Lemma neglabel_fun_soundness l :
neglabel l (neglabel_fun l).
Proof.
destruct l.
- simpl.
auto.
- simpl.
auto.
Qed.
Lemma neglabel_fun_completenss l l' :
neglabel l l' →
l' = neglabel_fun l.
Proof.
intros Hn.
inversion Hn; auto.
Qed.
Lemma progress N A :
nil ⊢ N : A →
(Is_true (is_val_of_trm N)) ∨
(∃ M, step N M) ∨
(∃ p, N = t_blame p).
Proof.
intros.
dependent induction H; simpl; auto.
-
specialize (IHtyping1 (JMeq_refl nil)) as [s_val | [[L step_s] | [p s_blame]]]; subst; right; left; eauto.
specialize (IHtyping2 (JMeq_refl nil)) as [t_val | [[L' step_t] | [p t_blame]]]; subst.
× ∃ (t_const 0). eauto.
× eauto.
× eauto.
-
specialize (IHtyping1 (JMeq_refl nil)) as [s_val | [[L' step_s] | [p s_blame]]]; subst; eauto; try (right; left; eauto).
specialize (IHtyping2 (JMeq_refl nil)) as [t_val | [[L' step_t] | [p t_blame]]]; subst; eauto; try (right; left; eauto).
pose proof (canonical_forms_arrow _ _ _ H s_val) as [[s0 Elam] | [v1 [V1 [V2 [T1 [T2 [p [Eval Ecast]]]]]]]].
× subst. eauto.
× subst. eexists. eapply step_wrap; eauto.
+ inversion H. eauto.
+ eapply neglabel_fun_soundness.
-
specialize (IHtyping (JMeq_refl nil)) as [s_val | [[L step_s] | [p s_blame]]]; subst; eauto.
-
right. left.
specialize (IHtyping1 (JMeq_refl nil)) as [s_val | [[M' step_s] | [p s_blame]]]; subst; eauto.
× apply Is_true_eq_true in s_val.
inversion H; subst; try discriminate.
+ eexists. eauto.
+ inversion s_val. eexists. eapply step_case_lift; eauto with bool.
+ inversion s_val. apply andb_true_iff in H6. destruct H6. discriminate.
× eexists. eauto.
× eexists. eauto.
-
specialize (IHtyping (JMeq_refl nil)) as [s_val | [[L step_s] | [p2 s_blame]]]; subst; eauto.
apply Is_true_eq_true in s_val.
destruct M; try discriminate.
×
inversion H; subst.
inversion H0; subst; eauto with bool.
×
inversion H; subst.
inversion H0; subst.
inversion H1; subst.
+ right. left. eauto with bool.
+ left. eauto with bool.
×
inversion H; subst.
right. destruct B; eauto.
×
inversion H; subst.
right.
destruct B; eauto with bool.
×
inversion s_val.
apply andb_true_iff in H2. destruct H2.
apply andb_true_iff in H1. destruct H1.
destruct B0; try discriminate.
destruct D; try discriminate.
inversion H; subst.
inversion H0; subst.
+ right. eauto with bool.
+ left. inversion H11; subst; eauto with bool.
-
right. right. eauto.
Qed.