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

Set Implicit Arguments.

Hint Unfold imm_happens_before.

Lemma hupds A h l (y : A) : hupd h l y l = y.

Lemma hist_closed_trans :
  ∀ sb rf V (HC: hist_closed sb rf V)
    a b (TR: clos_refl_trans _ sb a b) (IN: In b V), In a V.

Lemma hist_closedD :
  ∀ sb rf V (HC: hist_closed sb rf V)
    a b (TR: happens_before_union_rf sb rf a b) (IN: In b V), In a V.

Lemma happens_before_trans lab sb rf mo a b c :
  happens_before lab sb rf mo a b →
  happens_before lab sb rf mo b c →
  happens_before lab sb rf mo a c.

Lemma happens_before_union_rf_trans sb rf a b c :
  happens_before_union_rf sb rf a b →
  happens_before_union_rf sb rf b c →
  happens_before_union_rf sb rf a c.

Lemma happens_before_sb lab (sb : relation actid) rf mo a b :
  sb a b → happens_before lab sb rf mo a b.

Lemma happens_before_sw lab sb rf mo a b :
  synchronizes_with lab sb rf mo a b → happens_before lab sb rf mo a b.

Lemma happens_before_union_rf_sb (sb : relation actid) rf a b :
  sb a b → happens_before_union_rf sb rf a b.

Lemma happens_before_union_rf_rf (sb : relation actid) rf a b :
  rf b = Some a → happens_before_union_rf sb rf a b.

Lemma clos_trans_hbE :
  ∀ lab sb rf mo a b (HB: clos_trans actid (happens_before lab sb rf mo) a b),
    happens_before lab sb rf mo a b.

Lemma clos_trans_hbUrfE :
  ∀ sb rf a b (HB: clos_trans actid (happens_before_union_rf sb rf) a b),
    happens_before_union_rf sb rf a b.

Hint Immediate clos_trans_hbE : hb.
Hint Immediate clos_trans_hbUrfE : hb.

Hint Resolve
  happens_before_sb happens_before_sw happens_before_union_rf_sb happens_before_union_rf_rf
  happens_before_trans happens_before_union_rf_trans t_step hist_closedD : hb.

Lemma count_implies :
  ∀ (T: eqType) (f1 f2 : T → bool) (IMP : ∀ x, f1 x → f2 x) l,
  count f1 l ≤ count f2 l.

Lemma hasP´ :
  ∀ (T : eqType) (a : pred T) (l : list_predType T),
    reflect (∃ x : T, In x l ∧ a x) (has a l).

Lemma clos_refl_transE X rel a b :
    clos_refl_trans X rel a b ↔ a = b ∨ clos_trans X rel a b.

Lemma clos_refl_trans_hbE :
  ∀ lab sb rf mo a b,
    clos_refl_trans actid (happens_before lab sb rf mo) a b →
    happens_before lab sb rf mo a b ∨ a = b.

Lemma clos_refl_trans_hbUrfE :
  ∀ sb rf a b,
    clos_refl_trans actid (happens_before_union_rf sb rf) a b →
    happens_before_union_rf sb rf a b ∨ a = b.

Lemma helper_perm_filter_post :
  ∀ e T,
    ∃ posts_sb posts_rf,
      Permutation T (filter (fun x : hbcase ⇒ (hb_fst x != e) || (x == hb_sink e)) T ++
                     map (hb_sb e) posts_sb ++
                     map (hb_rf e) posts_rf).

Lemma helper_filter_decide_sink: ∀ a T (ND: NoDup T),
      Permutation (filter (fun x : hbcase ⇒ (hb_fst x != a) || (x == hb_sink a)) T)
        (if excluded_middle_informative (In (hb_sink a) T)
          then hb_sink a :: (filter (fun x : hbcase ⇒ hb_fst x != a) T)
          else (filter (fun x : hbcase ⇒ hb_fst x != a) T)).

Lemma has_rf_succs acts lab sb rf mo (a: actid) :
  ExecutionFinite acts lab sb →
  ConsistentRF_basic lab sb rf mo →
  ∃ (rfs: list actid),
    << NDrfs: NoDup rfs >> ∧
    << INrfs: ∀ x, In x rfs ↔ rf x = Some a >>.

Lemma has_rf_pres acts lab sb rf mo a :
  ExecutionFinite acts lab sb →
  ConsistentRF_basic lab sb rf mo →
  ∃ rfs,
    << NDrfs: NoDup rfs >> ∧
    << INrfs: ∀ x, In x rfs ↔ rf a = Some x >>.

Definition wf_ltof A (f : A → nat) :
  well_founded (fun x y ⇒ f x < f y).

Lemma In_implies_perm A (x : A) l (IN: In x l) :
  ∃ l´, Permutation l (x :: l´).

Lemma Permutation_count A l l´ (P : Permutation (A:=A) l l´) f :
  count f l = count f l´.

Lemma count_eq_0: ∀ A f (lst: list A), count f lst = 0 ↔ ∀ x (IN: In x lst), ¬ f x.

Lemma Permutation_hmap_valids :
  ∀ l l´ (P : Permutation l l´) lab sb rf hmap,
    hmap_valids lab sb rf hmap l →
    hmap_valids lab sb rf hmap l´.

Lemma Permutation_hmap_valids_strong :
  ∀ l l´ (P : Permutation l l´) lab sb rf hmap,
    hmap_valids_strong lab sb rf hmap l →
    hmap_valids_strong lab sb rf hmap l´.

Lemma Permutation_hist_closed :
  ∀ l l´ (P : Permutation l l´) sb rf,
    hist_closed sb rf l →
    hist_closed sb rf l´.

Lemma Consistent_perm :
  ∀ acts lab sb rf mo sc mt (CONS : Consistent acts lab sb rf mo sc mt)
         acts´ (EQ: perm_eq acts acts´),
    Consistent acts´ lab sb rf mo sc mt.

Lemma weakConsistent_perm :
  ∀ acts lab sb rf mo sc mt (CONS : weakConsistent acts lab sb rf mo sc mt)
         acts´ (EQ: perm_eq acts acts´),
    weakConsistent acts´ lab sb rf mo sc mt.

Lemma weakConsistent_Permutation :
  ∀ acts lab sb rf mo sc mt (CONS : weakConsistent acts lab sb rf mo sc mt)
         acts´ (EQ: Permutation acts acts´),
    weakConsistent acts´ lab sb rf mo sc mt.

Lemma Permutation_flatten A l l´ (P : Permutation l l´) :
  Permutation (A:=A) (flatten l) (flatten l´).

Lemma AcyclicStrong_implies_IrreflexiveHBuRF:
  ∀ lab sb rf mo, AcyclicStrong lab sb rf mo → IrreflexiveHBuRF sb rf.

Hint Resolve AcyclicStrong_implies_IrreflexiveHBuRF.

Definition is_pred A (rel : A → A → Prop) B a :=
  has (fun b ⇒ mydec (clos_refl_trans A rel a b)) B.

Definition depth_metric A (rel: A → A → Prop) V a :=
  count (is_pred rel a) V.

Lemma clos_transK T (rel: relation T) x y :
  clos_trans _ (clos_trans _ rel) x y →
  clos_trans _ rel x y.

Lemma clos_refl_transD T rel a b :
  clos_refl_trans T rel a b → a = b ∨ clos_trans T rel a b.

Lemma depth_lt (rel : relation actid) V A B
  (HB : ∀ a, In a A → ¬ In a B →
        ∃ b, In b B ∧ rel a b)
  b (IN : In b B) (NIN: ¬ In b A)
  (NHB: ∀ a, In a A → ¬ clos_trans _ rel b a)
  (SUB: ∀ b, In b B → In b V) :
  depth_metric rel V A < depth_metric rel V B.

Lemma edge_depth_ind lab sb rf V
  (ACYCLIC: IrreflexiveHBuRF sb rf)
  (HC: hist_closed sb rf V) (P : hbcase → Prop) :
  (∀ edge
    (IH: ∀ edge´ (EV : edge_valid lab sb rf edge´)
            (LT: happens_before_union_rf sb rf (hb_fst edge´) (hb_fst edge)),
      P edge´)
    (EV : edge_valid lab sb rf edge)
    (IN : In (hb_fst edge) V),
    P edge) →
  ∀ edge (EV : edge_valid lab sb rf edge), In (hb_fst edge) V → P edge.

Fixpoint find_max A (curr : A) f l :=
  match l with
    | nil ⇒ curr
    | x :: xs ⇒
      if f curr ≤ f x then find_max x f xs else find_max curr f xs
  end.

Lemma find_max_range :
  ∀ A (curr: A) f l,
    In (find_max curr f l) (curr :: l).

Lemma find_max_greatest :
  ∀ A (x curr: A) f l (IN: In x (curr :: l)),
    f x ≤ f (find_max curr f l).

Lemma get_deepest :
  ∀ sb rf (ACYCLIC: IrreflexiveHBuRF sb rf)
         V (HC: hist_closed sb rf V)
         T (NNIL: T ≠ nil)
         (INCL: ∀ edge (IN: In edge T), In (hb_fst edge) V),
  ∃ edge,
    << IN: In edge T >> ∧
    << INe: In (hb_fst edge) V >> ∧
    << DEEP: ∀ edge´ (IN´: In edge´ T)
                 (HB´: happens_before_union_rf sb rf (hb_fst edge) (hb_fst edge´)),
               False >>.

Fixpoint find_min A (curr : A) f l :=
  match l with
    | nil ⇒ curr
    | x :: xs ⇒
      if f x ≤ f curr then find_min x f xs else find_min curr f xs
  end.

Lemma find_min_range :
  ∀ A (curr: A) f l,
    In (find_min curr f l) (curr :: l).

Lemma find_min_greatest :
  ∀ A (x curr: A) f l (IN: In x (curr :: l)),
    f (find_min curr f l) ≤ f x.

Lemma get_shallow :
  ∀ lab sb rf mo (ACYCLIC: AcyclicStrong lab sb rf mo)
         V (HC: hist_closed sb rf V)
         T (HC´: hist_closed sb rf (V ++ T)) (NNIL: T ≠ nil),
  ∃ e,
    << IN: In e T >> ∧
    << HC: hist_closed sb rf (e :: V) >>.

Lemma no_normals_on_rf :
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    a b (RF: rf b = Some a) hmap (VALID: hmap_valid lab sb rf hmap a)
    hfr (MAP: hmap (hb_rf a b) = Hdef hfr) l (ALL: hfr l ≠ HVnone) (NORMAL: HVlabeled (hfr l) HLnormal),
  False.
Lemma triangles_never_on_rf:
∀ edge lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (EV: edge_valid lab sb rf edge) hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge))
    hf (MAP: hmap edge = Hdef hf) l (ALL: hf l ≠ HVnone) (LAB: HVlabeled (hf l) HLtriangle),
  is_sb edge ∨ is_sink edge.

Lemma valid_accessD :
  ∀ lab sb rf hmap a
         (VALID : hmap_valid lab sb rf hmap a)
         (Aa : is_access (lab a)),
  ∃ pre hf,
    sb pre a ∧ hmap (hb_sb pre a) = Hdef hf
    ∧ hf (loc (lab a)) ≠ HVnone ∧ HVlabeled (hf (loc (lab a))) HLnormal.

Lemma valid_na_accessD :
  ∀ lab sb rf hmap a
         (VALID : hmap_valid lab sb rf hmap a)
         (NA : is_na (lab a)) pre
         (SB : sb pre a) hf
         (HM : hmap (hb_sb pre a) = Hdef hf),
  is_val (hf (loc (lab a))).

Lemma valid_readD :
  ∀ lab sb rf hmap a
         (VALID : hmap_valid lab sb rf hmap a)
         (Ra : is_read (lab a)),
  ∃ pre hf,
    sb pre a ∧ hmap (hb_sb pre a) = Hdef hf
    ∧ HVlabeledR (hf (loc (lab a))) HLnormal.