Require Import Vbase List Classical ClassicalDescription.
Require Import permission GpsSepAlg.
Require Import fslassn fslassnsem fslmodel.
Require Import fslassnlemmas fslassnlemmas2.

Set Implicit Arguments.

Definition normalize_lbl lbl :=
  match lbl with
    | Some HLCnormal | Some HLCtriangledot | Some HLCnabladot | Some HLCdiamonddot ⇒ Some HLCnormal
    | Some HLCtriangle | Some HLCnabla | Some HLCdiamond ⇒ None
    | None ⇒ None
  end.

Definition denormalize_lbl lbl :=
  match lbl with
    | Some HLCnormal ⇒ None
    | Some HLCtriangle | Some HLCtriangledot ⇒ Some HLCtriangle
    | Some HLCnabla | Some HLCnabladot ⇒ Some HLCnabla
    | Some HLCdiamond | Some HLCdiamonddot ⇒ Some HLCdiamond
    | None ⇒ None
  end.

Lemma label_split lbl: lbl = ohlplus (normalize_lbl lbl) (denormalize_lbl lbl).
Proof.
  by destruct lbl; ins; desf.
Qed.

Lemma normalize_lbl_dist lbl1 lbl2 :
  normalize_lbl (ohlplus lbl1 lbl2) = ohlplus (normalize_lbl lbl1) (normalize_lbl lbl2).
Proof.
  by destruct lbl1, lbl2; ins; desf.
Qed.

Program Definition normalize_hv PS PSg (hv : HeapVal PS PSg) : HeapVal PS PSg:=
  match hv with
    | HVnone ⇒ HVnone
    | HVuval lbl ⇒
        match excluded_middle_informative (lbl = HLnormal) return HeapVal PS PSg with
             | left _ ⇒ HVuval lbl
             | right _ ⇒ HVnone
           end
    | HVval v Perm pNormal pTriangle pNabla _
        ⇒ match excluded_middle_informative (pNormal ≠ Pzero Perm) return HeapVal PS PSg with
             | left _ ⇒ HVval v Perm pNormal (Pzero Perm) (Pzero Perm) _
             | right _ ⇒ HVnone
           end
    | HVra PP QQ isrmw permlbl initlbl
        ⇒ HVra PP QQ isrmw (normalize_lbl permlbl) (normalize_lbl initlbl)
  end.
Next Obligation.
  unfold permissionsOK in *; split; red; intro; pplus_zero_simpl; desf.
  by rewrite !permission_plus_undef_l in PSUMdef.
Qed.

Program Definition denormalize_hv PS PSg (hv : HeapVal PS PSg) : HeapVal PS PSg:=
  match hv with
    | HVnone ⇒ HVnone
    | HVuval lbl ⇒
        match excluded_middle_informative (lbl = HLnormal) return HeapVal PS PSg with
             | left _ ⇒ HVnone
             | right _ ⇒ HVuval lbl
           end
    | HVval v Perm pNormal pTriangle pNabla _
        ⇒ match excluded_middle_informative (pTriangle ## pNabla ≠ Pzero Perm) return HeapVal PS PSg with
             | left _ ⇒ HVval v Perm (Pzero Perm) pTriangle pNabla _
             | right _ ⇒ HVnone
           end
    | HVra PP QQ isrmw permlbl initlbl
        ⇒ if isrmw
           then HVra PP QQ isrmw (denormalize_lbl permlbl) (denormalize_lbl initlbl)
           else HVra PP Remp isrmw (denormalize_lbl permlbl) (denormalize_lbl initlbl)
  end.
Next Obligation.
  unfold permissionsOK in *; split; red; intro; pplus_eq_zero; pplus_zero_simpl; desf.
  by rewrite H0, permission_plus_undef_r in PSUMdef.
Qed.

Definition normal_part PS PSg (h : heap PS PSg) :=
  match h with
    | Hundef ⇒ Hundef
    | Hdef hf hfg ⇒ Hdef (fun x ⇒ normalize_hv (hf x)) hfg
  end.

Definition triangled_part PS PSg (h : heap PS PSg) :=
  match h with
    | Hundef ⇒ Hundef
    | Hdef hf hfg ⇒ Hdef (fun x ⇒ denormalize_hv (hf x)) gres_emp
  end.

Lemma heap_split PS PSg (h : heap PS PSg): h = normal_part h +!+ triangled_part h.
Proof.
  destruct h; ins.
  rewrite hplus_unfold; ins; desf; desf.
  × f_equal.
      2: by rewrite gres_plus_total_emp_r.
    exten; ins.
    destruct (hf x); clear; ins; desf; ins; desf.
    + by eapply HVval_equal; eq_rect_simpl; pplus_zero_simpl.
    + by exfalso; eq_rect_simpl; pplus_zero_simpl.
    + by apply NNPP in n0; pplus_eq_zero; eapply HVval_equal; eq_rect_simpl.
    + by apply NNPP in n; pplus_eq_zero; eapply HVval_equal; eq_rect_simpl.
    + eby exfalso; apply NNPP in n; apply NNPP in n0; pplus_eq_zero; desf; eapply all_permissions_zero.
    + by f_equal; try (by rewrite <- label_split); exten; ins; desf.
    + f_equal; try (by rewrite <- label_split); exten; ins; desf.
      apply assn_mod_eqI1; ins.
      by rewrite assn_norm_emp, assn_norm_star_emp_r, assn_norm_mod.
  × destruct n; unnw; split; ins.
    by destruct (hf v); ins; desf; ins; desf; eq_rect_simpl; split; ins; vauto; pplus_zero_simpl.
    by rewrite gres_plus_emp_r.

  Grab Existential Variables. all: done.
Qed.

Lemma normal_part_hplus_dist PS PSg (h1 h2 : heap PS PSg):
  h1 +!+ h2 ≠ Hundef → normal_part (h1 +!+ h2) = normal_part h1 +!+ normal_part h2.
Proof.
  destruct h1, h2; ins.
  rewrite !hplus_unfold; ins; desf; ins; desf.
  × f_equal; exten; ins.
    generalize (HEAPcompat0 x); clear.
    destruct (hf x), (hf0 x); ins; desf; ins; desf; try (by f_equal; rewrite <- normalize_lbl_dist).
    + by eapply HVval_equal; eq_rect_simpl; pplus_zero_simpl.
    + destruct n2; red; eq_rect_simpl; rewrite !permission_plusA; pplus_zero_simpl; split; try done.
      intro U; rewrite U in ×.
      red in p; desf.
      by rewrite permission_plus_undef_l in PSUMdef.
    + eby exfalso; eq_rect_simpl; apply NNPP in n1; rewrite n1 in *; pplus_zero_simpl; eapply all_permissions_zero.
    + by apply NNPP in n1; pplus_eq_zero.
    + by apply NNPP in n0; desf; eapply HVval_equal; eq_rect_simpl; pplus_zero_simpl.
    + by apply NNPP in n1; pplus_eq_zero.
    + by apply NNPP in n; desf; eapply HVval_equal; eq_rect_simpl; pplus_zero_simpl.
    + by apply NNPP in n1; pplus_eq_zero.
    + by exfalso; apply NNPP in n; apply NNPP in n0; desf; pplus_zero_simpl.
  × destruct n; unnw; split; ins.
    generalize (HEAPcompat v); clear.
    destruct (hf v), (hf0 v); ins; desf; ins; desf; split; try done; eq_rect_simpl.
    red; rewrite !permission_plusA; pplus_zero_simpl; split.
      2: by intro; pplus_eq_zero.
    intro U; rewrite U in ×.
    red in H0; desf.
    by rewrite permission_plus_undef_l in PSUMdef.
  × rewrite hplus_unfold in H; ins; desf.

  Grab Existential Variables. all: done.
Qed.

Lemma normal_part_is_normal PS PSg (h : heap PS PSg):
  h ≠ Hundef → HlabeledExact (normal_part h) HLnormal.
Proof.
  destruct h; ins.
  eexists _ , _; split; try edone.
  red; ins.
  destruct (hf l); ins; desf; destruct permlbl, init; ins; desf.
Qed.

Opaque Aexists Aconj Adisj.

Inductive modality_free_positive PS PSg : (assn PS PSg) → Prop :=
  | MFPtrue: modality_free_positive Atrue
  | MFPemp: modality_free_positive Aemp
  | MFPpt: ∀ Perm psIN p OK E E', modality_free_positive (Apt Perm psIN p OK E E')
  | MFPptu: ∀ E, modality_free_positive (Aptu E)
  | MFPrainit: ∀ E, modality_free_positive (Arainit E)
  | MFPrel: ∀ E Q, modality_free_positive (Arel E Q)
  | MFPacq: ∀ E Q, modality_free_positive (Aacq E Q)
  | MFPrmwacq: ∀ E Q, modality_free_positive (Armwacq E Q)
  | MFPghost: ∀ PCM pcmIN E g, modality_free_positive (Aghost PCM pcmIN E g)
  | MPFconj: ∀ P Q, modality_free_positive P → modality_free_positive Q
                           → modality_free_positive (Aconj P Q)
  | MFPdisj: ∀ P Q, modality_free_positive P → modality_free_positive Q
                           → modality_free_positive (Adisj P Q)
  | MFPstar: ∀ P Q, modality_free_positive P → modality_free_positive Q
                           → modality_free_positive (Astar P Q)
  | MFPforall: ∀ PP, (∀ x, modality_free_positive (PP x))
                          → modality_free_positive (Aforall PP)
  | MFPexists: ∀ PP, (∀ x, modality_free_positive (PP x))
                          → modality_free_positive (Aexists PP).

Lemma MFPassn_cares_only_about_normal_part PS PSg (F: assn PS PSg) (MFP: modality_free_positive F) h :
  assn_sem F h → assn_sem F (normal_part h).
Proof.
  revert h; induction MFP;
  try (by ins; desf; ins; f_equal; exten; ins; unfold hupd; desf; ins; desf).
  × ins; desf; ins.
    by split; destruct h.
  × ins; desf; ins.
    f_equal; exten; ins.
    unfold hupd; desf; ins; desf.
    by eapply HVval_equal; eq_rect_simpl.
  × ins; rewrite assn_sem_conj in *; desf; eauto using IHMFP1, IHMFP2.
  × ins; rewrite assn_sem_disj in *; desf; eauto using IHMFP1, IHMFP2.
  × ins; desf.
    ∃ (normal_part h1), (normal_part h2); repeat split; eauto using IHMFP1, IHMFP2.
    by destruct (h1 +!+ h2).
    by rewrite normal_part_hplus_dist.
  × by ins; apply H0.
  × ins; rewrite assn_sem_exists in *; desf.
    eexists; eauto using H.

  Grab Existential Variables. done.
Qed.

Theorem MFPassn_normalizable PS PSg (F: assn PS PSg):
  modality_free_positive F → normalizable F.
Proof.
  red; ins.
  ∃ (normal_part h), (triangled_part h); repeat split.
  by apply MFPassn_cares_only_about_normal_part.
  eby eapply normal_part_is_normal, assn_sem_def.
  by apply heap_split.
Qed.