Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnlemmas fslmodel fslhmap.

Set Implicit Arguments.

Lemma triple_helper_start P e QQ :
  (∀ res acts_cmd lab sb fst lst
      (SEM : exp_sem e res acts_cmd lab sb fst lst) acts_ctx rf mo sc
      (CONS : weakConsistent (acts_cmd ++ acts_ctx) lab sb rf mo sc Model_hb_rf_acyclic)
      (UNIQ : NoDup (acts_cmd ++ acts_ctx))
      prev (FST : unique (sb^~ fst) prev)
      next (LST : unique (sb lst) next)
      n V (V_PREV : In prev V)
      (V_CTX : ∀ x : actid, In x V → In x acts_ctx)
      (HC : hist_closed sb rf V)
      hmap
      (VALID : hmap_valids_strong lab sb rf hmap V)
      (pDEF : hmap (hb_sb prev fst) ≠ Hundef) hp hFR
      (pEQ : hmap (hb_sb prev fst) = hp +!+ hFR)
      (pSAT : assn_sem P hp)
      (NIN : ¬ In fst V)
      (HC : hist_closed sb rf (fst :: V))
      (LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst),
   ∃ hmap´,
     agrees sb rf V hmap hmap´ ∧
     (hmap_valids_strong lab sb rf hmap´ (fst :: V)) ∧
     safe acts_cmd acts_ctx lab sb rf n (fst :: V) hmap´ lst
       (with_opt res
                 (fun res h ⇒ ∃ hFR´ hq, h ≠ Hundef ∧ h = hq +!+ hFR +!+ hFR´
                                          ∧ assn_sem (QQ res) hq))) →
  triple P e QQ.

Lemma Permutation_safe1 :
  ∀ l l´ (P : Permutation l l´) acts lab sb rf n V hmap lst Q,
    safe l acts lab sb rf n V hmap lst Q →
    safe l´ acts lab sb rf n V hmap lst Q.

Lemma map_upd_irr (A: eqType) B C (hmap : A → B) x y f (l : list C) :
  (∀ a, In a l → f a ≠ x) →
  map (mupd hmap x y) (map f l) = map hmap (map f l).

Lemma valid_ext :
  ∀ lab sb rf hmap e V
      (VAL : hmap_valid lab sb rf hmap e) (IN: In e V)
      (HC : hist_closed sb rf V) a (NIN: ¬ In a V) b h,
    hmap_valid lab sb rf (mupd hmap (hb_sb a b) h) e.
Lemma valid_ext_sink :
  ∀ lab sb rf hmap e V
      (VAL : hmap_valid lab sb rf hmap e) (IN: In e V)
      (HC : hist_closed sb rf V) a (NIN: ¬ In a V) h,
    hmap_valid lab sb rf (mupd hmap (hb_sink a) h) e.
Lemma hmap_irr_change_valid:
  ∀ lab sb rf hmap hmap´ e
    (VALID: hmap_valid lab sb rf hmap e)
    (IRR: ∀ edge, hb_fst edge = e ∨ hb_snd edge = Some e → hmap´ edge = hmap edge),
  hmap_valid lab sb rf hmap´ e.
Lemma safe_mod :
  ∀ acts_cmd acts_ctx lab sb rf n V hmap lst QQ
    (H : safe acts_cmd acts_ctx lab sb rf n V hmap lst QQ)
    acts_cmd´ (E1: ∀ x (NIN: ¬ In x V) (IN: In x acts_cmd´), In x acts_cmd)
    acts_ctx´ (E2: ∀ x (NIN: ¬ In x V) (IN: In x acts_ctx´), In x acts_ctx),
    safe acts_cmd´ acts_ctx´ lab sb rf n V hmap lst QQ.

Lemma safe_final1 :
  ∀ acts_cmd acts_ctx lab sb rf lst
      (LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
      V Q n hmap
      (HC: hist_closed sb rf (lst :: V))
      (VALID: hmap_valids_strong lab sb rf hmap (lst :: V))
      (POST: ∀ next (SB: sb lst next), Q (hmap (hb_sb lst next)) : Prop),
    safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap lst Q.

Lemma safe_final_plain :
  ∀ acts_cmd acts_ctx lab sb rf n V lst hmap Q next h
    (LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
    (HC: hist_closed sb rf V)
    (HC´: hist_closed sb rf (lst :: V))
    (VALID: hmap_valids_strong lab sb rf hmap V)
    (LST: unique (fun x ⇒ sb lst x) next)
    (POST: Q h : Prop)
    (VALID´: hmap_valid lab sb rf (mupd hmap (hb_sb lst next) h) lst)
    (NIN: ¬ In lst V),
    ∃ hmap´,
      agrees sb rf V hmap hmap´ ∧
      hmap_valids_strong lab sb rf hmap´ (lst :: V) ∧
      safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap´ lst Q.

Lemma safe_final_plain2 :
  ∀ acts_cmd acts_ctx lab sb rf n V lst hmap Q next h
    (LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
    (HC: hist_closed sb rf V)
    (HC´: hist_closed sb rf (lst :: V))
    (VALID: hmap_valids_strong lab sb rf hmap V)
    (LST: unique (fun x ⇒ sb lst x) next)
    (POST: Q h : Prop)
    (VALID´: hmap_valid lab sb rf (mupd hmap (hb_sb lst next) h) lst)
    (NIN: ¬ In lst V),
    ∃ hmap´,
      agrees sb rf V hmap hmap´ ∧
      hmap_valids_strong lab sb rf hmap´ (lst :: V) ∧
      safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap´ lst Q.

Lemma safe_final3 :
  ∀ acts_cmd acts_ctx lab sb rf n V lst hmap Q next h
    (LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
    (HC: hist_closed sb rf V)
    (HC´: hist_closed sb rf (lst :: V))
    (VALID: hmap_valids_strong lab sb rf hmap V)
    (LST: unique (fun x ⇒ sb lst x) next)
    (POST: Q h : Prop)
    (VALID´: hmap_valid lab sb rf (mupd hmap (hb_sb lst next) h) lst)
    (NIN: ¬ In lst V),
    ∃ hmap´,
      agrees sb rf V hmap hmap´ ∧
      hmap_valids_strong lab sb rf hmap´ (lst :: V) ∧
      safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap´ lst Q.

Lemma safe_final3s :
  ∀ acts_cmd acts_ctx lab sb rf n V lst hmap Q next h hs
    (LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
    (HC: hist_closed sb rf V)
    (HC´: hist_closed sb rf (lst :: V))
    (VALID: hmap_valids_strong lab sb rf hmap V)
    (LST: unique (fun x ⇒ sb lst x) next)
    (POST: Q h : Prop)
    (VALID´: hmap_valid lab sb rf (mupd (mupd hmap (hb_sb lst next) h) (hb_sink lst) hs) lst)
    (NIN: ¬ In lst V),
    ∃ hmap´,
      agrees sb rf V hmap hmap´ ∧
      hmap_valids_strong lab sb rf hmap´ (lst :: V) ∧
      safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap´ lst Q.

Lemma safe_final4a :
  ∀ acts_cmd acts_ctx lab sb rf n V lst hmap Q wri next hr hsinkw h hs
    (LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
    (HC: hist_closed sb rf V)
    (HC´: hist_closed sb rf (lst :: V))
    (VALID: hmap_valids_strong lab sb rf hmap V)
    (LST: unique (fun x ⇒ sb lst x) next)
    (RF: rf lst = Some wri)
    (POST: Q h : Prop)
    (VALID´: hmap_valid lab sb rf (mupd
                                       (mupd
                                            (mupd
                                                 (mupd
                                                      hmap
                                                  (hb_rf wri lst) hr)
                                            (hb_sink wri) hsinkw)
                                       (hb_sb lst next) h)
                                  (hb_sink lst) hs)
                              lst)
    (VALID´´: hmap_valid lab sb rf (mupd (mupd hmap (hb_rf wri lst) hr) (hb_sink wri) hsinkw) wri)
    (NIN: ¬ In lst V),
    ∃ hmap´,
      agrees sb rf V hmap hmap´ ∧
      hmap_valids_strong lab sb rf hmap´ (lst :: V) ∧
      safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap´ lst Q.