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

Set Implicit Arguments.

Lemma go_back_one_val :
  ∀ lab sb rf mo hmap edge
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (VALID : hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET : hmap edge = Hdef hf) l v
    (LA : has_value (hf l) v)
    (NW: ¬ is_writeLV (lab (hb_fst edge)) l v),
  ∃ edge´,
    edge_valid lab sb rf edge´ ∧
    hb_snd edge´ = Some (hb_fst edge) ∧
    ¬ is_writeL (lab (hb_fst edge)) l ∧
    ∃ hf´, hmap edge´ = Hdef hf´ ∧ has_value (hf´ l) v.
Lemma heap_loc_na_initialized2 :
  ∀ acts lab sb rf mo hmap V
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l v (LA: has_value (h l) v),
  ∃ cpre c hf,
    sb cpre c ∧
    is_writeLV (lab c) l v ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    is_val (hf l) ∧
    (c = hb_fst edge ∨ happens_before_union_rf sb rf c (hb_fst edge)) ∧
    (∀ d
      (HB1: d = hb_fst edge ∨ happens_before_union_rf sb rf d (hb_fst edge))
      (HB2: happens_before_union_rf sb rf c d),
      ¬ is_writeL (lab d) l).
Lemma is_write_weaken typ l v : is_writeLV typ l v → is_writeL typ l.

Lemma is_access_weaken typ l v : is_writeLV typ l v → is_access typ.

Hint Resolve is_write_weaken is_access_weaken.

Lemma two_access_cases :
  ∀ pre a b acts lab sb rf mo hmap V hf
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    (INa : In a V)
    (INb : In b V)
    (SB : sb pre a) (HD: hmap (hb_sb pre a) = Hdef hf) (IV: is_val (hf (loc (lab a))))
    (B : is_access (lab b)) (LOC : loc (lab a) = loc (lab b)),
  a = b ∨ happens_before_union_rf sb rf a b ∨ happens_before_union_rf sb rf b a.