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.