Blame
Require Export Coq.Program.Equality.
Require Export Definitions Infrastructure.
Require Export Metalib.Metatheory.
Require Export Safety.
Notation "A '≺' B" := (subtyp A B) (at level 40).
Notation "A '≺+' B" := (subtyp_pos A B) (at level 40).
Notation "A '≺-' B" := (subtyp_neg A B) (at level 40).
Notation "A '≺n' B" := (subtyp_n A B) (at level 40).
Inductive safe : trm → label → Prop :=
| safe_varb n p : safe (t_var_b n) p
| safe_var x p : safe (t_var_f x) p
| safe_constant c p : safe (t_const c) p
| safe_binop M N p : safe M p → safe N p → safe (t_binop M N) p
| safe_abs A N p : safe N p → safe (t_abs A N) p
| safe_app L M p : safe L p → safe M p → safe (t_app L M) p
| safe_null p : safe t_null p
| safe_lift M p : safe M p → safe (t_lift M) p
| safe_case L M N p : safe L p → safe M p → safe N p → safe (t_case L M N) p
| safe_cast_pos A B p M : A ≺+ B → safe M p → safe (M ⦂ A ⇒ B @@ p) p
| safe_cast_neg A B p M : A ≺- B → safe M p → safe (M ⦂ A ⇒ B @@ (neglabel_fun p)) p
| safe_cast_diff A B p q M : safe M p → p ≠ q → p ≠ (neglabel_fun q) → safe (M ⦂ A ⇒ B @@ q) p
| safe_blame_diff p q : p ≠ q → safe (t_blame q) p.
Hint Constructors safe : core.
Lemma subst_pres_safe M N p n :
safe N p →
safe M p →
safe (open_trm_wrt_trm_rec n M N) p.
Proof.
intros Hsa Hsv.
generalize dependent n.
induction N; intros; default_simp.
inversion Hsa; subst; eauto.
Qed.
Notation "~~ p" := (neglabel_fun p) (at level 40).
Lemma neglabel_fun_completeness l l' :
neglabel l l' →
l' = ~~ l.
Proof.
intros Hn.
inversion Hn; auto.
Qed.
Lemma neglabel_fun_involutive p :
~~ (~~ p) = p.
Proof.
destruct p; auto.
Qed.
Lemma neglabel_not_id p : p ≠ ~~ p.
Proof.
destruct p; simpl; discriminate.
Qed.
Hint Resolve neglabel_not_id : core.
Lemma safe_preservation : ∀ G M A N p,
G ⊢ N : A →
step N M →
safe N p →
safe M p.
Proof.
intros G M A N p Htyp Hstep Hsafe.
generalize dependent A.
dependent induction Hstep; intros; inversion Htyp; subst; inversion Hsafe; subst; eauto.
- eapply subst_pres_safe; eauto.
inversion Hsafe; subst; auto.
inversion H4; subst; auto.
- pose proof (neglabel_fun_completeness _ _ H3). subst.
inversion Htyp; subst; eauto.
inversion Hsafe; subst; eauto.
inversion H6; subst; eauto.
× inversion H17; subst; eauto.
× inversion H17; subst; eauto.
rewrite (neglabel_fun_involutive p). eauto.
× eapply safe_cast_diff; eauto.
eapply safe_app; eauto.
eapply safe_cast_diff; eauto.
rewrite (neglabel_fun_involutive p0). eauto.
- inversion H9; subst; eauto.
inversion H6; eauto.
- inversion H9; subst; eauto.
inversion H6; eauto.
- inversion H6; eauto.
- inversion H4.
- inversion H6.
- inversion H9; subst; eauto.
inversion H6; eauto.
- inversion H6; eauto.
- inversion H6; eauto.
- inversion H6; eauto.
- inversion H6; subst; eauto.
eapply subst_pres_safe; eauto.
Qed.
Ltac invert_safe_blame :=
match goal with
| [ H : safe (⇑ ?q) ?p |- ?p ≠ ?q ] ⇒
inversion H; subst; eauto end.
Lemma subst_is_blame : ∀ L M p,
open_trm_wrt_trm L M = ⇑ p →
L = ⇑ p ∨ M = ⇑ p.
Proof.
intros.
unfold open_trm_wrt_trm in H.
unfold open_trm_wrt_trm_rec in H.
induction L; default_simp.
Qed.
Lemma safe_progress : ∀ N A p q,
nil ⊢ N : A →
safe N p →
step N (⇑ q) →
p ≠ q.
Proof.
intros N A p q Htyp Hsafe Hstep.
pose proof (safe_preservation _ _ _ _ _ Htyp Hstep Hsafe).
inversion H. assumption.
Qed.
Inductive multi_step : trm → trm → Prop :=
| multi_step_refl: ∀ N,
multi_step N N
| star_step: ∀ L M N,
step L M →
multi_step M N →
multi_step L N.
Theorem safety N A p q :
nil ⊢ N : A →
safe N p →
multi_step N (t_blame q) →
p ≠ q.
Proof.
intros.
dependent induction H1; eauto.
- inversion H0. subst. assumption.
- eapply IHmulti_step; eauto.
× pose proof (preservation _ _ _ _ H H2); eauto.
× pose proof (safe_preservation _ _ _ _ _ H H2 H0). auto.
Qed.
Lemma tangram_fwd : ∀ A B,
A ≺ B →
A ≺+ B ∧ A ≺- B.
Proof.
intros.
induction H; subst; split;
try destruct IHsubtyp; try destruct IHsubtyp1; try destruct IHsubtyp2;
eauto.
Qed.
Scheme sub_pos_mut := Induction for subtyp_pos Sort Prop
with sub_neg_mut := Induction for subtyp_neg Sort Prop.
Combined Scheme sub_mutind from sub_pos_mut, sub_neg_mut.
Lemma tangram_rev_helper :
(∀ A B, A ≺+ B → A ≺- B → A ≺ B) ∧
(∀ A B, A ≺- B → A ≺+ B → A ≺ B).
Proof.
apply sub_mutind; intros; eauto.
- inversion H0; subst; eauto.
- inversion H0; subst; eauto.
- inversion H1; subst; eauto.
- inversion H0; subst; eauto.
- inversion H0; subst; eauto.
- inversion H0; subst; eauto.
- inversion H1; subst; eauto.
Qed.
Lemma tangram_rev : ∀ A B,
A ≺+ B → A ≺- B → A ≺ B.
Proof.
pose proof tangram_rev_helper.
destruct H.
assumption.
Qed.
Lemma tangram_naive_fwd : ∀ A B,
A ≺n B →
A ≺+ B ∧ B ≺- A.
Proof.
intros.
induction H; subst; split;
try destruct IHsubtyp_n; try destruct IHsubtyp_n1; try destruct IHsubtyp_n2; eauto.
Qed.
Lemma tangram_naive_rev_helper :
(∀ A B, A ≺+ B → B ≺- A → A ≺n B) ∧
(∀ B A, B ≺- A → A ≺+ B → A ≺n B).
Proof.
apply sub_mutind; intros; eauto.
- inversion H0; subst; eauto.
- inversion H0; subst; eauto.
- inversion H1; subst; eauto.
- inversion H0; subst; eauto.
- inversion H0; subst; eauto.
- inversion H0; subst; eauto.
- inversion H1; subst; eauto.
Qed.
Lemma tangram_naive_rev : ∀ A B,
A ≺+ B → B ≺- A → A ≺n B.
Proof.
pose proof tangram_naive_rev_helper.
destruct H.
assumption.
Qed.
Hint Resolve tangram_fwd : tangram.
Hint Resolve tangram_rev : tangram.
Hint Resolve tangram_naive_fwd : tangram.
Hint Resolve tangram_naive_rev : tangram.
Lemma tangram : ∀ A B,
(A ≺ B ↔ A ≺+ B ∧ A ≺- B) ∧
(A ≺n B ↔ A ≺+ B ∧ B ≺- A).
Proof.
intros.
split; split; try destruct 1; eauto with tangram.
Qed.
Require Export Definitions Infrastructure.
Require Export Metalib.Metatheory.
Require Export Safety.
Notation "A '≺' B" := (subtyp A B) (at level 40).
Notation "A '≺+' B" := (subtyp_pos A B) (at level 40).
Notation "A '≺-' B" := (subtyp_neg A B) (at level 40).
Notation "A '≺n' B" := (subtyp_n A B) (at level 40).
Inductive safe : trm → label → Prop :=
| safe_varb n p : safe (t_var_b n) p
| safe_var x p : safe (t_var_f x) p
| safe_constant c p : safe (t_const c) p
| safe_binop M N p : safe M p → safe N p → safe (t_binop M N) p
| safe_abs A N p : safe N p → safe (t_abs A N) p
| safe_app L M p : safe L p → safe M p → safe (t_app L M) p
| safe_null p : safe t_null p
| safe_lift M p : safe M p → safe (t_lift M) p
| safe_case L M N p : safe L p → safe M p → safe N p → safe (t_case L M N) p
| safe_cast_pos A B p M : A ≺+ B → safe M p → safe (M ⦂ A ⇒ B @@ p) p
| safe_cast_neg A B p M : A ≺- B → safe M p → safe (M ⦂ A ⇒ B @@ (neglabel_fun p)) p
| safe_cast_diff A B p q M : safe M p → p ≠ q → p ≠ (neglabel_fun q) → safe (M ⦂ A ⇒ B @@ q) p
| safe_blame_diff p q : p ≠ q → safe (t_blame q) p.
Hint Constructors safe : core.
Lemma subst_pres_safe M N p n :
safe N p →
safe M p →
safe (open_trm_wrt_trm_rec n M N) p.
Proof.
intros Hsa Hsv.
generalize dependent n.
induction N; intros; default_simp.
inversion Hsa; subst; eauto.
Qed.
Notation "~~ p" := (neglabel_fun p) (at level 40).
Lemma neglabel_fun_completeness l l' :
neglabel l l' →
l' = ~~ l.
Proof.
intros Hn.
inversion Hn; auto.
Qed.
Lemma neglabel_fun_involutive p :
~~ (~~ p) = p.
Proof.
destruct p; auto.
Qed.
Lemma neglabel_not_id p : p ≠ ~~ p.
Proof.
destruct p; simpl; discriminate.
Qed.
Hint Resolve neglabel_not_id : core.
Lemma safe_preservation : ∀ G M A N p,
G ⊢ N : A →
step N M →
safe N p →
safe M p.
Proof.
intros G M A N p Htyp Hstep Hsafe.
generalize dependent A.
dependent induction Hstep; intros; inversion Htyp; subst; inversion Hsafe; subst; eauto.
- eapply subst_pres_safe; eauto.
inversion Hsafe; subst; auto.
inversion H4; subst; auto.
- pose proof (neglabel_fun_completeness _ _ H3). subst.
inversion Htyp; subst; eauto.
inversion Hsafe; subst; eauto.
inversion H6; subst; eauto.
× inversion H17; subst; eauto.
× inversion H17; subst; eauto.
rewrite (neglabel_fun_involutive p). eauto.
× eapply safe_cast_diff; eauto.
eapply safe_app; eauto.
eapply safe_cast_diff; eauto.
rewrite (neglabel_fun_involutive p0). eauto.
- inversion H9; subst; eauto.
inversion H6; eauto.
- inversion H9; subst; eauto.
inversion H6; eauto.
- inversion H6; eauto.
- inversion H4.
- inversion H6.
- inversion H9; subst; eauto.
inversion H6; eauto.
- inversion H6; eauto.
- inversion H6; eauto.
- inversion H6; eauto.
- inversion H6; subst; eauto.
eapply subst_pres_safe; eauto.
Qed.
Ltac invert_safe_blame :=
match goal with
| [ H : safe (⇑ ?q) ?p |- ?p ≠ ?q ] ⇒
inversion H; subst; eauto end.
Lemma subst_is_blame : ∀ L M p,
open_trm_wrt_trm L M = ⇑ p →
L = ⇑ p ∨ M = ⇑ p.
Proof.
intros.
unfold open_trm_wrt_trm in H.
unfold open_trm_wrt_trm_rec in H.
induction L; default_simp.
Qed.
Lemma safe_progress : ∀ N A p q,
nil ⊢ N : A →
safe N p →
step N (⇑ q) →
p ≠ q.
Proof.
intros N A p q Htyp Hsafe Hstep.
pose proof (safe_preservation _ _ _ _ _ Htyp Hstep Hsafe).
inversion H. assumption.
Qed.
Inductive multi_step : trm → trm → Prop :=
| multi_step_refl: ∀ N,
multi_step N N
| star_step: ∀ L M N,
step L M →
multi_step M N →
multi_step L N.
Theorem safety N A p q :
nil ⊢ N : A →
safe N p →
multi_step N (t_blame q) →
p ≠ q.
Proof.
intros.
dependent induction H1; eauto.
- inversion H0. subst. assumption.
- eapply IHmulti_step; eauto.
× pose proof (preservation _ _ _ _ H H2); eauto.
× pose proof (safe_preservation _ _ _ _ _ H H2 H0). auto.
Qed.
Lemma tangram_fwd : ∀ A B,
A ≺ B →
A ≺+ B ∧ A ≺- B.
Proof.
intros.
induction H; subst; split;
try destruct IHsubtyp; try destruct IHsubtyp1; try destruct IHsubtyp2;
eauto.
Qed.
Scheme sub_pos_mut := Induction for subtyp_pos Sort Prop
with sub_neg_mut := Induction for subtyp_neg Sort Prop.
Combined Scheme sub_mutind from sub_pos_mut, sub_neg_mut.
Lemma tangram_rev_helper :
(∀ A B, A ≺+ B → A ≺- B → A ≺ B) ∧
(∀ A B, A ≺- B → A ≺+ B → A ≺ B).
Proof.
apply sub_mutind; intros; eauto.
- inversion H0; subst; eauto.
- inversion H0; subst; eauto.
- inversion H1; subst; eauto.
- inversion H0; subst; eauto.
- inversion H0; subst; eauto.
- inversion H0; subst; eauto.
- inversion H1; subst; eauto.
Qed.
Lemma tangram_rev : ∀ A B,
A ≺+ B → A ≺- B → A ≺ B.
Proof.
pose proof tangram_rev_helper.
destruct H.
assumption.
Qed.
Lemma tangram_naive_fwd : ∀ A B,
A ≺n B →
A ≺+ B ∧ B ≺- A.
Proof.
intros.
induction H; subst; split;
try destruct IHsubtyp_n; try destruct IHsubtyp_n1; try destruct IHsubtyp_n2; eauto.
Qed.
Lemma tangram_naive_rev_helper :
(∀ A B, A ≺+ B → B ≺- A → A ≺n B) ∧
(∀ B A, B ≺- A → A ≺+ B → A ≺n B).
Proof.
apply sub_mutind; intros; eauto.
- inversion H0; subst; eauto.
- inversion H0; subst; eauto.
- inversion H1; subst; eauto.
- inversion H0; subst; eauto.
- inversion H0; subst; eauto.
- inversion H0; subst; eauto.
- inversion H1; subst; eauto.
Qed.
Lemma tangram_naive_rev : ∀ A B,
A ≺+ B → B ≺- A → A ≺n B.
Proof.
pose proof tangram_naive_rev_helper.
destruct H.
assumption.
Qed.
Hint Resolve tangram_fwd : tangram.
Hint Resolve tangram_rev : tangram.
Hint Resolve tangram_naive_fwd : tangram.
Hint Resolve tangram_naive_rev : tangram.
Lemma tangram : ∀ A B,
(A ≺ B ↔ A ≺+ B ∧ A ≺- B) ∧
(A ≺n B ↔ A ≺+ B ∧ B ≺- A).
Proof.
intros.
split; split; try destruct 1; eauto with tangram.
Qed.