Require Import List Vbase Varith Vlist extralib.
Require Import Classical ClassicalDescription IndefiniteDescription.
Require Import Permutation rslassn.

Set Implicit Arguments.

Transparent hplus.

Lemma hdef_alt h : h ≠ Hundef ↔ ∃ hf, h = Hdef hf.

Lemma AcombinableC P Q: Acombinable P Q → Acombinable Q P.

Lemma assn_mod_eqI1 (P Q: assn_mod): proj1_sig P = proj1_sig Q → P = Q.

Lemma assn_mod_eqI (P Q: assn_mod): Asim (sval P) (sval Q) → P = Q.

Lemma AsimD P Q : Asim P Q → mk_assn_mod P = mk_assn_mod Q.

Lemma hv_acq_defC b1 Q1 b2 Q2 :
  hv_acq_def b1 Q1 b2 Q2 → hv_acq_def b2 Q2 b1 Q1.

Lemma hvplusDEFC hv1 hv2: hvplusDEF hv1 hv2 → hvplusDEF hv2 hv1.

Lemma hvplusC hv1 hv2: hvplusDEF hv1 hv2 → hvplus hv1 hv2 = hvplus hv2 hv1.

Lemma hplusC h1 h2: hplus h1 h2 = hplus h2 h1.

Lemma hplus_emp_l h : hplus hemp h = h.

Lemma hplus_emp_r h : hplus h hemp = h.

Lemma hplus_eq_emp h1 h2 : hplus h1 h2 = hemp ↔ h1 = hemp ∧ h2 = hemp.

Lemma assn_norm_mod (Q : assn_mod) : assn_norm (sval Q) = sval Q.

Lemma hvplusDEF_hvplusA h1 h2 h3 :
  hvplusDEF h1 h2 →
  hvplusDEF (hvplus h1 h2) h3 →
  hvplusDEF h1 (hvplus h2 h3).

Lemma hvplusDEF_hvplus1 h1 h2 h3 :
  hvplusDEF h2 h3 →
  hvplusDEF h1 (hvplus h2 h3) →
  hvplusDEF h1 h2.

Lemma hvplusDEF_hvplus2 h1 h2 h3 :
  hvplusDEF h1 h2 →
  hvplusDEF (hvplus h1 h2) h3 →
  hvplusDEF h2 h3.

Lemma hvplusA h1 h2 h3 :
  hvplusDEF h1 h2 →
  hvplus (hvplus h1 h2) h3 = hvplus h1 (hvplus h2 h3).

Lemma hplusA h1 h2 h3 :
  hplus (hplus h1 h2) h3 = hplus h1 (hplus h2 h3).

Lemma hplusAC h1 h2 h3 :
  hplus h2 (hplus h1 h3) = hplus h1 (hplus h2 h3).

Lemma hplus_not_undef_l h h' : hplus h h' ≠ Hundef → h ≠ Hundef.

Lemma hplus_not_undef_r h h' : hplus h h' ≠ Hundef → h' ≠ Hundef.

Hint Resolve hplus_not_undef_l.
Hint Resolve hplus_not_undef_r.

Lemma hplus_def_inv h h' hx (P: hplus h h' = Hdef hx) :
  ∃ hy hz, h = Hdef hy ∧ h' = Hdef hz
    ∧ << DEFv: ∀ l, hvplusDEF (hy l) (hz l) >>
    ∧ << PLUSv: ∀ l, hx l = hvplus (hy l) (hz l) >>.

Lemma hplus_def_inv_l h h' hf : hplus h h' = Hdef hf → ∃ h3, h = Hdef h3.

Lemma hplus_def_inv_r h h' hf : hplus h h' = Hdef hf → ∃ h3, h' = Hdef h3.

Lemma hplus_alloc h1 h2 h l :
  hplus h1 h2 = Hdef h →
  h l ≠ HVnone →
  ∃ h', h1 = Hdef h' ∧ h' l ≠ HVnone ∨ h2 = Hdef h' ∧ h' l ≠ HVnone.

Lemma hplus_nalloc h1 h2 h loc :
  Hdef h = hplus h1 h2 →
  h loc = HVnone →
  ∃ h1f h2f, Hdef h1f = h1 ∧ h1f loc = HVnone ∧ Hdef h2f = h2 ∧ h2f loc = HVnone.

Lemma hplus_has_val_l :
  ∀ h h1 h2 l,
    hplus h1 h2 = Hdef h →
    (∀ h'', h1 = Hdef h'' → is_val (h'' l)) →
    is_val (h l).

Lemma hplus_has_val_r :
  ∀ h h1 h2 l,
    hplus h1 h2 = Hdef h →
    (∀ h'', h2 = Hdef h'' → is_val (h'' l)) →
    is_val (h l).

Lemma hplus_is_val :
  ∀ h h1 h2 l,
    hplus h1 h2 = Hdef h →
    is_val (h l) →
    ∃ hf1 hf2,
      h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧ (is_val (hf1 l) ∨ is_val (hf2 l)).

Lemma hplus_val_lD:
  ∀ h h1 h2 l v,
    Hdef h = hplus h1 h2 →
    (∀ h'', Hdef h'' = h1 → h'' l = HVval v) →
    h l = HVval v.

Lemma hplus_val_rD:
  ∀ h h1 h2 l v,
    Hdef h = hplus h1 h2 →
    (∀ h'', Hdef h'' = h2 → h'' l = HVval v) →
    h l = HVval v.

Lemma hplus_valD:
  ∀ h h1 h2 l v,
    hplus h1 h2 = Hdef h →
    h l = HVval v →
    ∃ hf1 hf2, h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧ (hf1 l = HVval v ∨ hf2 l = HVval v).

Lemma hplus_eq_ra_initD:
  ∀ h h1 h2 l PP QQ isrmw,
    hplus h1 h2 = Hdef h →
    h l = HVra PP QQ isrmw true →
    ∃ hf PP' QQ' isrmw',
      (h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP' QQ' isrmw' true.

Definition hvplus_ra2_ret hv (QQ' : val → assn_mod) :=
  match hv with
    | HVra PP QQ isrmw init ⇒
      ∀ v, ∃ QR, Asim (sval (QQ v)) (Astar (sval (QQ' v)) QR)
    | _ ⇒ False
  end.

Lemma hvplus_ra2 hv hv' PP' QQ' isrmw' init' :
  hv = HVra PP' QQ' isrmw' init' →
  hvplusDEF hv hv' →
  hvplus_ra2_ret (hvplus hv hv') QQ'.

Lemma hsum_nil : hsum nil = hemp.

Lemma hsum_cons a l : hsum (a :: l) = hplus a (hsum l).

Lemma hsum_one h : hsum (h :: nil) = h.

Lemma hsum_two h h' : hsum (h :: h' :: nil) = hplus h h'.

Lemma hsum_perm l l' : Permutation l l' → hsum l = hsum l'.

Lemma hsum_app l l' : hsum (l ++ l') = hplus (hsum l) (hsum l').

Lemma hsum_alloc l h loc :
  hsum l = Hdef h →
  h loc ≠ HVnone →
  ∃ h', In (Hdef h') l ∧ h' loc ≠ HVnone.

Lemma hsum_nalloc hs hf h loc :
  Hdef hf = hsum hs →
  hf loc = HVnone →
  In h hs →
  ∃ hf, Hdef hf = h ∧ hf loc = HVnone.

Lemma hsum_has_val :
  ∀ h hs h'' l,
    hsum hs = Hdef h →
    In (Hdef h'') hs →
    is_val (h'' l) →
    is_val (h l).

Lemma hsum_is_val :
  ∀ hs h l,
    hsum hs = Hdef h →
    is_val (h l) →
    ∃ hf, In (Hdef hf) hs ∧ is_val (hf l).

Lemma hsum_valD :
  ∀ h hs h'' l v,
    hsum hs = Hdef h →
    In (Hdef h'') hs →
    h'' l = HVval v →
    h l = HVval v.

Lemma hsum_eq_val :
  ∀ hs h l v,
    hsum hs = Hdef h →
    h l = HVval v →
    ∃ hf, In (Hdef hf) hs ∧ hf l = HVval v.

Lemma hsum_eq_ra_initD:
  ∀ h' hs l PP QQ isrmw,
    hsum hs = Hdef h' →
    h' l = HVra PP QQ isrmw true →
    ∃ h'' PP' QQ' isrmw',
      In (Hdef h'') hs ∧
      h'' l = HVra PP' QQ' isrmw' true.

Lemma hdef_upd_alloc hf l v' h h' :
  is_val (hf l) →
  hplus (Hdef hf) h = Hdef h' →
  ∃ h'', hplus (Hdef (hupd hf l (HVval v'))) h = Hdef h''.

Lemma hdef_upd_alloc2 hf l v' h h' :
  is_val (hf l) →
  hplus (Hdef hf) h = Hdef h' →
  ∃ h'',
    hplus (Hdef (hupd hf l (HVval v'))) h = Hdef h''
    ∧ (∀ l' (NEQ: l' ≠ l), h'' l' = h' l').

Lemma hplus_unfold h1 h2 :
  hplus (Hdef h1) (Hdef h2) =
  (if excluded_middle_informative (∀ v : val, hvplusDEF (h1 v) (h2 v))
    then Hdef (fun v : val ⇒ hvplus (h1 v) (h2 v))
    else Hundef).

Lemma hplus_init_def hf l h h' :
  hplus (Hdef hf) h = Hdef h' →
  hplus (Hdef (initialize hf l)) h ≠ Hundef.

Lemma hplus_init_def2 hf l h h' :
  hplus (Hdef hf) h = Hdef h' →
  hf l ≠ HVnone →
  hplus (Hdef (initialize hf l)) h = Hdef (initialize h' l).

Lemma initialize_eq_raD hf l l' PP QQ isrmw init :
  initialize hf l l' = HVra PP QQ isrmw init →
  ∃ init', hf l' = HVra PP QQ isrmw init'.

Lemma assn_sem_def P h : assn_sem P h → h ≠ Hundef.

Lemma sim_assn_sem :
  ∀ p p' (S: Asim p p') h, assn_sem p h ↔ assn_sem p' h.

Lemma assn_sem_satD Q h : assn_sem Q h → ∃ hf, h = Hdef hf.

Lemma precise_emp : precise Aemp.

Lemma precise_star P Q : precise P → precise Q → precise (Astar P Q).

Hint Resolve precise_emp precise_star.

Lemma assn_sem_disj P Q h :
  assn_sem (Adisj P Q) h ↔ assn_sem P h ∨ assn_sem Q h.

Lemma assn_sem_exists PP h :
  assn_sem (Aexists PP) h ↔ ∃ x, assn_sem (PP x) h.

Lemma hplus_ram_lD:
  ∀ h h1 h2 l PP QQ init,
    hplus (Hdef h1) h2 = Hdef h →
    h1 l = HVra PP QQ true init →
    ∃ PP' init',
      h l = HVra PP' QQ true init' ∧
      (∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h) ∧
      ∃ hf, h2 = Hdef hf ∧
        (hf l = HVnone ∧ init = init'
         ∨ ∃ PP'' QQ'' isrmw'' init'',
              hf l = HVra PP'' QQ'' isrmw'' init'' ∧
              init' = (init || init'') ∧
              (∀ v, sval (QQ'' v) = Aemp ∨ QQ'' v = QQ v)).

Lemma hplus_ram_rD:
  ∀ h h1 h2 l PP QQ init,
    hplus h1 (Hdef h2) = Hdef h →
    h2 l = HVra PP QQ true init →
    ∃ PP' init',
      h l = HVra PP' QQ true init' ∧
      (∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h) ∧
      ∃ hf, h1 = Hdef hf ∧
        (hf l = HVnone ∧ init = init'
         ∨ ∃ PP'' QQ'' isrmw'' init'',
              hf l = HVra PP'' QQ'' isrmw'' init'' ∧
              init' = (init || init'') ∧
              (∀ v, sval (QQ'' v) = Aemp ∨ QQ'' v = QQ v)).

Lemma hplus_ra_lD:
  ∀ h h1 h2 l PP QQ init,
    hplus (Hdef h1) h2 = Hdef h →
    h1 l = HVra PP QQ false init →
    ∃ PP' QQ' isrmw' init',
      h l = HVra PP' QQ' isrmw' init' ∧
      (∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h) ∧
      ∃ hf, h2 = Hdef hf ∧
        (hf l = HVnone ∧ (∀ v, QQ' v = QQ v) ∧ init = init' ∧ isrmw' = false
         ∨ ∃ PP'' QQ'' init'',
           hf l = HVra PP'' QQ'' isrmw' init'' ∧
           init' = (init || init'') ∧
           (∀ v, Asim (sval (QQ' v)) (Astar (sval (QQ v)) (sval (QQ'' v))))).

Lemma hplus_ra_rD:
  ∀ h h1 h2 l PP QQ init,
    hplus h1 (Hdef h2) = Hdef h →
    h2 l = HVra PP QQ false init →
    ∃ PP' QQ' isrmw' init',
      h l = HVra PP' QQ' isrmw' init' ∧
      (∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h) ∧
      ∃ hf, h1 = Hdef hf ∧
        (hf l = HVnone ∧ (∀ v, QQ' v = QQ v) ∧ init = init' ∧ isrmw' = false
         ∨ ∃ PP'' QQ'' init'',
           hf l = HVra PP'' QQ'' isrmw' init'' ∧
           init' = (init || init'') ∧
           (∀ v, Asim (sval (QQ' v)) (Astar (sval (QQ v)) (sval (QQ'' v))))).

Lemma hsum_raD:
  ∀ h hs h'' l PP QQ isrmw init,
    hsum hs = Hdef h →
    In (Hdef h'') hs →
    h'' l = HVra PP QQ isrmw init →
    ∃ PP' QQ' isrmw' init',
      h l = HVra PP' QQ' isrmw' init' ∧ (init → init') ∧ (isrmw → isrmw')
      ∧ (∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h).

Lemma hplus_raD:
  ∀ h h1 h2 l PP QQ isrmw init,
    hplus h1 h2 = Hdef h →
    h l = HVra PP QQ isrmw init →
    ∃ hf1 hf2,
      h1 = Hdef hf1 ∧ h2 = Hdef hf2
      ∧ << N: hf1 l ≠ HVnone ∨ hf2 l ≠ HVnone >>
      ∧ << L: hf1 l = HVnone ∨ ∃ PP' QQ' isrmw' init',
               hf1 l = HVra PP' QQ' isrmw' init' ∧
               (∀ v h, assn_sem (sval (PP' v)) h → assn_sem (sval (PP v)) h) >>
      ∧ << R: hf2 l = HVnone ∨ ∃ PP' QQ' isrmw' init',
               hf2 l = HVra PP' QQ' isrmw' init' ∧
               (∀ v h, assn_sem (sval (PP' v)) h → assn_sem (sval (PP v)) h) >>.

Lemma hplus_raD':
  ∀ h h1 h2 l PP QQ isrmw init,
    hplus h1 h2 = Hdef h →
    h l = HVra PP QQ isrmw init →
    ∃ hf1 hf2, h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧
     ( (hf1 l = HVnone ∧ ∃ PP' QQ', hf2 l = HVra PP' QQ' isrmw init ∧ PP' = PP ∧ QQ' = QQ)
      ∨ (hf2 l = HVnone ∧ ∃ PP' QQ', hf1 l = HVra PP' QQ' isrmw init ∧ PP' = PP ∧ QQ' = QQ)
      ∨ (∃ PP1 QQ1 isrmw1 init1 PP2 QQ2 isrmw2 init2,
            hf1 l = HVra PP1 QQ1 isrmw1 init1 ∧
            hf2 l = HVra PP2 QQ2 isrmw2 init2 ∧
            init = init1 || init2 ∧
            isrmw = isrmw1 || isrmw2 ∧
            (∀ v, Acombinable (sval (PP1 v)) (sval (PP2 v))) ∧
            (∀ v h, assn_sem (sval (PP v)) h ↔
                         assn_sem (sval (PP1 v)) h ∨ assn_sem (sval (PP2 v)) h))).

Lemma hplus_eq_raD:
  ∀ h h1 h2 l PP QQ isrmw init v,
    hplus h1 h2 = Hdef h →
    h l = HVra PP QQ isrmw init →
    ∃ hf PP' QQ' isrmw' init',
      (h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP' QQ' isrmw' init' ∧
      (∀ h, assn_sem (sval (PP v)) h ↔ assn_sem (sval (PP' v)) h).

Lemma hsum_eq_raD:
  ∀ h' hs l PP QQ isrmw init v,
    hsum hs = Hdef h' →
    h' l = HVra PP QQ isrmw init →
    ∃ h'' PP' QQ' isrmw' init',
      In (Hdef h'') hs ∧
      h'' l = HVra PP' QQ' isrmw' init' ∧
      (∀ h, assn_sem (sval (PP v)) h ↔ assn_sem (sval (PP' v)) h).

Lemma hplus_init1 E PP QQ isrmw init :
  hplus (hsingl E (HVra PP QQ isrmw init))
        (hsingl E (HVra Wemp Remp false true)) =
  hsingl E (HVra PP QQ isrmw true).

Lemma hdef_initializeE hf E PP QQ isrmw init :
  hf E = HVra PP QQ isrmw init →
  Hdef (initialize hf E) = hplus (Hdef hf) (hsingl E (HVra Wemp Remp false true)).

Opaque hplus.

Lemma foldr_star_perm :
  ∀ l l' (P: Permutation l l') init h,
    assn_sem (foldr Astar l init) h →
    assn_sem (foldr Astar l' init) h.

Lemma foldr_star_perm2 :
  ∀ l l' (P: Permutation l l') init,
    Asim (foldr Astar l init) (foldr Astar l' init).

Lemma assn_sem_foldr_true_ext A (f: A → assn) l h h' :
  assn_sem (foldr Astar (List.map f l) Atrue) h →
  hplus h h' ≠ Hundef →
  assn_sem (foldr Astar (List.map f l) Atrue) (hplus h h').