Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsSepAlg GpsModel GpsModelLemmas.
Require Import GpsGlobal GpsVisible GpsGlobalHelper.

Local Open Scope string_scope.

Set Implicit Arguments.

Lemma incoming_upd_ext_esc :
  ∀ acts (ND: NoDup acts) a (IN: In a acts) L b rr,
    incoming acts (upd L (Tesc a b) (rr ⊕ L (Tesc a b))) b =
    rr ⊕ incoming acts L b.

Lemma label_restr_fin acts amap sb rf mo sc L E :
  Consistent acts amap sb rf mo sc →
  label_restr acts amap sb rf L E →
  ∃ tel, ∀ te (NIN: ¬ In te tel), L te = res_emp.

Lemma res_gget_max_list l :
  ∃ n, ∀ n' (LT: n < n') r , In r l → res_gget r n' = None.

Lemma outgoing_upd_sbS b acts L E r a :
  outgoing acts (upd L (TsbS b) (L (TsbS b) ⊕ r)) E a =
  if a == b then r ⊕ outgoing acts L E a else outgoing acts L E a.

Lemma RP_extC (P : RProp) r (H : P r) r' (D: r' ⊕ r ≠ Rundef) : P (r' ⊕ r).

Lemma hb_irr :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) a
    (HB: happens_before amap sb rf a a),
    False.

Lemma compat_inc_sink :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND : NoDup acts) L
    (CC : compat amap sb rf L) E
    (LR : label_restr acts amap sb rf L E) a b,
  a = b ∨
  happens_before amap sb rf a b ∨
  happens_before amap sb rf b a ∨
  L (TsbS b) ⊕ incoming acts L a ≠ Rundef.

Lemma replace_edge_ext :
  ∀ A (a : A) f pi l
    (ND: NoDup l)
    (IN : In a l),
  rsum (map (upd f a (f a ⊕ pi)) l) = pi ⊕ rsum (map f l).

Lemma sat_exch_ext :
  ∀ IE σ r (M : sat_exch IE σ r)
         r' (D : r ⊕ r' ≠ Rundef),
  sat_exch IE σ (r ⊕ r').

Lemma exch_conform_ext1 IE acts amap sb rf L te r L' EE σ
  (ECO : exch_conform IE acts amap sb rf (upd L te r) L' EE σ)
  (NEQ: ∀ a, te ≠ TescS σ a) r'
  (IMP : res_escr (r ⊕ r') σ → res_escr r σ) :
  exch_conform IE acts amap sb rf (upd L te (r ⊕ r')) L' EE σ.

Lemma in_esc_upd_in :
  ∀ acts L a b r1 r,
    In a acts →
    NoDup acts →
    L (Tesc a b) = r1 →
    in_esc acts (upd L (Tesc a b) (r ⊕ r1)) b =
    in_esc acts L b ⊕ r.

Lemma hb_mhb amap sb rf a b :
  happens_before amap sb rf a b →
  may_happens_before amap sb rf a b.

Lemma ghost_allocE r mm :
  ghost_alloc r mm ↔ r = Rundef ∨ res_gget r mm ≠ None.

Lemma ghost_alloc_conform_helper2 :
  ∀ acts L EE (ND: NoDup EE) r r' a
         (GAC: ghost_alloc_conform acts (upd L (TsbS a) (L (TsbS a) ⊕ r)) EE)
         (IMP: ∀ gl (GA: ghost_alloc r' gl)
                 a' (NEQ: a ≠ a') (GA': ghost_alloc (outgoing acts L EE a') gl),
                 False)
         (DEF: outgoing acts (upd L (TsbS a) (L (TsbS a) ⊕ r ⊕ r')) EE a ≠ Rundef),
    ghost_alloc_conform acts (upd L (TsbS a) (L (TsbS a) ⊕ r ⊕ r')) EE.

Lemma outgoing_ee :
  ∀ acts amap sb rf L EE
    (LR : label_restr acts amap sb rf L EE) σ a,
    outgoing acts L
         (if excluded_middle_informative (In σ EE)
          then EE
          else σ :: EE) a =
    outgoing acts L EE a.

Lemma valid_ghost_gget :
  ∀ r r' (VG : valid_ghost r r') r0
         (BAR: ∀ m gr, res_gget r0 m = Some gr →
                            res_gget r m = None →
                            res_gget r' m = None) r''
         (IDEF : r ⊕ r0 ⊕ r'' ≠ Rundef)
         (ODEF : r' ⊕ r0 ≠ Rundef)
         (OUD : r' ⊕ r0 ⊕ r'' = Rundef),
   ∃ gl : nat,
     res_gget r'' gl ≠ None ∧
     res_gget (r ⊕ r0) gl = None ∧
     res_gget (r' ⊕ r0) gl ≠ None.

Lemma exch_conform_upd1_acc IE acts amap sb rf L L' EE σ te2 r
  (ECO : exch_conform IE acts amap sb rf (upd L te2 r) L' EE σ) te1 r1
  (N1: ∀ a, te1 = TescS σ a → sat_exch IE σ r1) r2
  (N2: ∀ a, te2 = TescS σ a → sat_exch IE σ r2)
  (SRC: te_src te1 = te_src te2)
  (T1: te_tgt te1 = None)
  (T2: te_tgt te2 = None)
  (NEQ: te1 ≠ te2)
  (DEF: r1 ⊕ r2 ≠ Rundef)
  (EQ: r1 ⊕ r2 = L te1 ⊕ r) :
  exch_conform IE acts amap sb rf (upd (upd L te1 r1) te2 r2) L' EE σ.

Lemma visible_ghost_one :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) L E
    (LR: label_restr acts amap sb rf L E)
    (CC: compat amap sb rf L) N
    (PC: prefix_closed sb rf N) te
    (IN : In (te_src te) N) gl
    (G : res_gget (L te) gl ≠ None)
    (ND: NoDup acts) (NDE: NoDup E),
  ∃ a,
    ≪ HB : may_happens_before amap sb rf a (te_src te) ≫ ∧
    ≪ INC : res_gget (incoming acts L a) gl = None ≫ ∧
    ≪ OUT : res_gget (outgoing acts L E a) gl ≠ None ≫ ∧
    ≪ INA : In a acts ≫.

Lemma visible_ghost2 :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) L E
    (GAC: ghost_alloc_conform acts L E)
    (CC: compat amap sb rf L) te a gl
    (G : res_gget (L te) gl ≠ None)
    (INC : res_gget (incoming acts L a) gl = None)
    (OUT : res_gget (outgoing acts L E a) gl ≠ None)
    (LR: label_restr acts amap sb rf L E)
    (ND: NoDup acts) (NDE: NoDup E) (INA: In a acts),
  may_happens_before amap sb rf a (te_src te).

Lemma sat_exch_emp IE σ : ¬ sat_exch IE σ res_emp.

Lemma ghost_elim_sat_exch IE P1 P2 Q r r' σ :
   interp_exch IE σ = (P1, P2) →
   ghost_elim P1 P2 Q r r' → sat_exch IE σ r'.

Lemma three_sat_exch IE r1 r2 r3 σ :
  sat_exch IE σ r1 →
  sat_exch IE σ r2 →
  sat_exch IE σ r3 →
  r1 ⊕ r2 ⊕ r3 = Rundef.

Lemma ghost_step :
  ∀ b acts (NIN: ¬ In b acts) amap sb rf mo sc r P
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (ND: NoDup (b :: acts))
    (PC : prefix_closed sb rf acts)
    (PI: pres_in sb rf b acts) IE
    (GM: ghost_move IE r P) L EE
    (V : ∀ a (IN: In a acts), valid_node IE (b::acts) (b::acts) amap rf L EE a)
    (CC: compat amap sb rf (upd L (TsbS b) (L (TsbS b) ⊕ r)))
    (CO: conform (b::acts) amap mo L acts)
    (ECO: ∀ σ,
           exch_conform IE (b::acts) amap sb rf
                         (upd L (TsbS b) (L (TsbS b) ⊕ r))
                         (upd L (TsbS b) (L (TsbS b) ⊕ r)) EE σ)
    (GAC: ghost_alloc_conform (b::acts)
                (upd L (TsbS b) (L (TsbS b) ⊕ r)) EE)
    (VG: valid_ghost (incoming (b::acts) L b)
                     (r ⊕ out_esc (b::acts) L EE b))
    (RS: res_lt (res_strip (incoming (b::acts) L b)) r)
    (EO: ∀ c, L (Tesc b c) = res_emp)
    (LR : label_restr (b::acts) amap sb rf L EE)
    (Osb : out_sb (b :: acts) L b = res_emp)
    (Orf : out_rf (b :: acts) L b = res_emp)
    (ND' : NoDup EE),
  ∃ L' EE' r,
    ≪ IN': P r ≫ ∧
    ≪ V : ∀ a (IN: In a acts), valid_node IE (b::acts) (b::acts) amap rf L' EE' a ≫ ∧
    ≪ CC: compat amap sb rf (upd L' (TsbS b) (L' (TsbS b) ⊕ r)) ≫ ∧
    ≪ CO: conform (b::acts) amap mo L' acts ≫ ∧
    ≪ ECO: ∀ σ,
              exch_conform IE (b::acts) amap sb rf
                           (upd L' (TsbS b) (L' (TsbS b) ⊕ r))
                           (upd L' (TsbS b) (L' (TsbS b) ⊕ r)) EE' σ ≫ ∧
    ≪ GAC: ghost_alloc_conform (b::acts)
                (upd L' (TsbS b) (L' (TsbS b) ⊕ r)) EE' ≫ ∧
    ≪ VG: valid_ghost (incoming (b::acts) L' b)
                       (r ⊕ out_esc (b::acts) L' EE' b) ≫ ∧
    ≪ RS: res_lt (res_strip (incoming (b::acts) L' b)) r ≫ ∧
    ≪ EO: ∀ c, L' (Tesc b c) = res_emp ≫ ∧
    ≪ Esb: ∀ a b, L' (Tsb a b) = L (Tsb a b) ≫ ∧
    ≪ Erf: ∀ a b, L' (Trf a b) = L (Trf a b) ≫ ∧
    ≪ EsbS: ∀ a, L' (TsbS a) = L (TsbS a) ≫ ∧
    ≪ ErfS: ∀ a, L' (TrfS a) = L (TrfS a) ≫ ∧
    ≪ NDE : NoDup EE' ≫ ∧
    ≪ EEE : ∀ σ, In σ EE → In σ EE' ≫ ∧
    ≪ LR : label_restr (b::acts) amap sb rf L' EE' ≫.