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

Local Open Scope string_scope.

Set Implicit Arguments.

Lemma rely_step :
  ∀ b acts (NIN: ¬ In b acts) amap sb rf mo sc L
    (PC : prefix_closed sb rf acts)
    (V : ∀ a (IN: In a acts), valid_node (b::acts) acts amap rf L a)
    (CC: compat amap sb rf L)
    (CO: conform (b::acts) amap mo L acts)
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (INrf: in_rf (b::acts) L b = res_emp)
    (INesc: in_esc (b::acts) L b = res_emp)
    (INsb: in_sb (b :: acts) L b ≠ Rundef)
    (INsbOK: ∀ a, ¬ sb a b → L (Tsb a b) = res_emp)
    (OUT : outgoing (b::acts) L b = res_emp)
    (ND : NoDup (b ::acts))
    (LR : label_restr (b::acts) amap sb rf L),
  ∃ L',
    ≪ V : ∀ a (IN: In a acts), valid_node (b::acts) (b::acts) amap rf L' a ≫ ∧
    ≪ CC: compat amap sb rf L' ≫ ∧
    ≪ CO: conform (b::acts) amap mo L' acts ≫ ∧
    ≪ RELY: rely (in_sb (b::acts) L' b) (amap b)
                  (in_sb (b::acts) L' b ⊕ in_rf (b::acts) L' b) ≫ ∧
    ≪ INesc: in_esc (b::acts) L' b = res_emp ≫ ∧
    ≪ OUT : outgoing (b::acts) L' b = res_emp ≫ ∧
    ≪ Esb : ∀ a b, L' (Tsb a b) = L (Tsb a b) ≫ ∧
    ≪ EsbS : ∀ a, L' (TsbS a) = L (TsbS a) ≫ ∧
    ≪ LR : label_restr (b::acts) amap sb rf L' ≫.

Lemma rely_compat_post :
  ∀ b acts amap sb rf
    (LAST: ∀ x, ¬ happens_before amap sb rf b x) L
    (LR : label_restr (b::acts) amap sb rf L)
    (CC: compat amap sb rf L)
    (ND : NoDup (b::acts))
    (OUT : outgoing (b::acts) L b = res_emp),
  compat amap sb rf
    (upd L (TescS b)
         (L (TescS b) ⊕ in_sb (b::acts) L b ⊕ in_rf (b::acts) L b)).

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 :
  Consistent acts amap sb rf mo sc →
  label_restr acts amap sb rf L →
  ∃ 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' = elem_gres_emp.

Lemma orR r r' : r || r' ↔ r ∨ r'.

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)
    (GM: ghost_move r P) L
    (V : ∀ a (IN: In a acts), valid_node (b::acts) (b::acts) amap rf L a)
    (CC: compat amap sb rf (upd L (TescS b) (L (TescS b) ⊕ r)))
    (CO: conform (b::acts) amap mo L acts) I
    (VG: valid_ghost (incoming (b::acts) L b)
                     (r ⊕ out_esc (b::acts) L b ⊕ L (TcondS b)) I)
    (VI : ∀ σ r (GIN: In (σ, r) I),
            ∃ P P', interp_escr σ = (P, P') ∧ P' r)
    (RS: res_lt (res_strip (incoming (b::acts) L b)) r)
    (VES: res_lt (rsum (map snd (filter (escr_ffun L (b::acts)) I))) (L (TescS b)))
    (EO: ∀ c, L (Tesc b c) = res_emp)
    (LR : label_restr (b::acts) amap sb rf L),
  ∃ L' I r,
    ≪ IN': P r ≫ ∧
    ≪ V : ∀ a (IN: In a acts), valid_node (b::acts) (b::acts) amap rf L' a ≫ ∧
    ≪ CC: compat amap sb rf (upd L' (TescS b) (L' (TescS b) ⊕ r)) ≫ ∧
    ≪ CO: conform (b::acts) amap mo L' acts ≫ ∧
    ≪ VG: valid_ghost (incoming (b::acts) L' b)
                       (r ⊕ out_esc (b::acts) L' b ⊕ L' (TcondS b)) I ≫ ∧
    ≪ RS: res_lt (res_strip (incoming (b::acts) L' b)) r ≫ ∧
    ≪ VI : ∀ σ r (GIN: In (σ, r) I),
            ∃ P P', interp_escr σ = (P, P') ∧ P' r ≫ ∧
    ≪ VES: res_lt (rsum (map snd (filter (escr_ffun L' (b::acts)) I))) (L' (TescS b)) ≫ ∧
    ≪ 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) ≫ ∧
    ≪ LR : label_restr (b::acts) amap sb rf L' ≫.