Safety

Require Export Coq.Program.Equality.
Require Export Definitions Infrastructure.
Require Export Metalib.Metatheory.

Ltac gather_atoms ::=
  let A := gather_atoms_with (fun x : varsx) in
  let B := gather_atoms_with (fun x : var{{ x }}) in
  let C := gather_atoms_with (fun x : ctxdom x) in
  let D1 := gather_atoms_with (fun xfv_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.