Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsFraction GpsSepAlg GpsModel.

Set Implicit Arguments.

Lemma get_state_lt2 τ (S S': slist τ) (L: slist_lt S S') s (IN: In s (SL_list S)) :
  prot_trans τ s (get_state S').

Lemma slist_lt_trans A (x y z: slist A) :
  slist_lt x y →
  slist_lt y z →
  slist_lt x z.

Lemma slist_ltD τ (S S': slist τ) :
  slist_lt S S' ↔ prot_trans τ (get_state S) (get_state S').

Lemma get_state_eq_incl_helper τ (S S': slist τ) :
  (∀ x, In x (SL_list S) → In x (SL_list S')) →
  slist_lt S' S →
  get_state S = get_state S'.

Lemma get_state_eq_prove :
  ∀ τ s (S : slist τ)
    (IN : In s (SL_list S))
    (LAST : ∀ s0, In s0 (SL_list S) → prot_trans τ s0 s),
  get_state S = s.

Lemma res_get_plus r l τ S r' :
  res_get r l = p_at τ S →
  (res_plus r r') ≠ Rundef →
  ∃ S',
    res_get (res_plus r r') l = p_at τ S' ∧
    ∀ s (SIN: In s (SL_list S)), In s (SL_list S').

Lemma res_get_plus2 r l τ S r' S' :
  res_get r l = p_at τ S →
  res_get r' l = p_at τ S' →
  (res_plus r r') ≠ Rundef →
  ∃ S'',
    res_get (res_plus r r') l = p_at τ S'' ∧
    ∀ s, In s (SL_list S'') ↔ In s (SL_list S) ∨ In s (SL_list S').

Lemma res_plus_strip_def r r' :
  res_plus r r' ≠ Rundef →
  res_plus r (res_strip r') ≠ Rundef.

Lemma res_plus_strip2_def r r' :
  res_plus r r' ≠ Rundef →
  res_plus (res_strip r) (res_strip r') ≠ Rundef.

Lemma res_plus_escr_def r e :
  r ≠ Rundef →
  res_plus r (Rdef (fun _ ⇒ p_bot) gres_emp e) ≠ Rundef.

Hint Resolve res_plus_strip_def res_plus_escr_def : rpd.

Lemma res_plus_left_def a b c :
  res_plus a (res_plus b c) ≠ Rundef →
  res_plus a b ≠ Rundef.

Lemma res_plus_right_def a b c :
  res_plus a (res_plus b c) ≠ Rundef →
  res_plus a c ≠ Rundef.

Hint Immediate res_plus_left_def res_plus_right_def.

Lemma res_get_upds r l pi : r ≠ Rundef → res_get (res_upd r l pi) l = pi.

Lemma res_plus_upd_at r l τ S :
 (res_get r l = p_bot ∨
 ∃ S',
   res_get r l = p_at τ S' ∧
   (∀ s, In s (SL_list S') → In s (SL_list S))) →
 res_upd r l (p_at τ S) =
 res_plus r
     (Rdef (fun x ⇒ if x == l then p_at τ S else p_bot) gres_emp
           (fun _ ⇒ false)).

Lemma res_plus_upd_upd r r' l pi pi' pi'' :
  res_plus r r' ≠ Rundef →
  prot_plus pi pi' = Some pi'' →
  res_plus (res_upd r l pi) (res_upd r' l pi') =
     (res_upd (res_plus r r') l pi'').

Lemma res_get_strip_at r l τ S :
  res_get r l = p_at τ S →
  res_get (res_strip r) l = p_at τ S.

Lemma res_get_plus_uninit2 r1 r2 l :
  res_get r1 l = p_uninit →
  res_plus r1 r2 ≠ Rundef →
  res_get r2 l = p_bot.

Lemma res_get_plus_bot_l r1 r2 l :
  res_get r1 l = p_bot →
  res_plus r1 r2 ≠ Rundef →
  res_get (res_plus r1 r2) l = res_get r2 l.

Lemma res_get_plus_bot_r r1 r2 l :
  res_get r2 l = p_bot →
  res_plus r1 r2 ≠ Rundef →
  res_get (res_plus r1 r2) l = res_get r1 l.

Lemma res_get_plus_na_l r1 r2 l :
  res_get r1 l = p_uninit ∨ (∃ n, res_get r1 l = p_na pe_full n) →
  res_plus r1 r2 ≠ Rundef →
  res_get (res_plus r1 r2) l = res_get r1 l.

Lemma res_upd_expand_bot r l pi :
  res_get r l = p_bot →
  res_upd r l pi = res_plus r (res_upd res_emp l pi).

Lemma res_plus_upd_l r r' l pi :
  res_plus r r' ≠ Rundef →
  res_get r' l = p_bot →
  res_plus (res_upd r l pi) r' =
  res_upd (res_plus r r') l pi.

Lemma prot_plus_get_helper r r' l pi pi' :
  res_get (res_plus r r') l = pi' →
  prot_plus pi' pi = Some pi →
  pi' ≠ p_bot →
  prot_plus (res_get r l) pi = Some pi.

Lemma prot_plus_at_bounded τ S S' :
  (∀ s, In s (SL_list S) → In s (SL_list S')) →
  prot_plus (p_at τ S) (p_at τ S') = Some (p_at τ S').

Lemma res_plus_upd_l2 r r' l pi :
  res_plus r r' ≠ Rundef →
  prot_plus (res_get r' l) pi = Some pi →
  res_plus (res_upd r l pi) r' =
  res_upd (res_plus r r') l pi.

Lemma res_strip_emp : res_strip res_emp = res_emp.

Lemma res_strip_upd r l pi :
  res_strip (res_upd r l pi) = res_upd (res_strip r) l (prot_strip pi).

Lemma res_upd_strip_irr r l pi :
  prot_strip (res_get r l) = pi →
  res_upd (res_strip r) l pi = res_strip r.

Lemma res_plus_strip_l r : res_plus (res_strip r) r = r.

Lemma res_plus_pcancel :
  ∀ r a b,
    res_plus r a = res_plus r b →
    res_plus r a ≠ Rundef →
    res_plus (res_strip r) a = res_plus (res_strip r) b.

Definition rknow r := r = res_strip r.

Lemma res_plus_ubound r r' :
    r ≠ Rundef →
    r = res_plus r r' →
    rknow r'.

Lemma gknow_plusE g g' gg :
  gres_plus g g' = Some gg →
  gg = gres_strip gg →
  g = gres_strip g ∧ g' = gres_strip g'.

Lemma rknow_plusE r r' :
  res_plus r r' ≠ Rundef →
  (rknow (res_plus r r') ↔ rknow r ∧ rknow r').

Lemma res_plus_eq_empD r r' : res_plus r r' = res_emp → r = res_emp ∧ r' = res_emp.

Lemma rsum_eq_empD l : rsum l = res_emp → ∀ r, In r l → r = res_emp.

Lemma res_plus_get1 r r' l :
  res_plus r r' ≠ Rundef →
  prot_plus (res_get r l) (res_get r' l) ≠ None.

Lemma res_plus_get2 r r' l :
  prot_plus (res_get r l) (res_get r' l) = None →
  res_plus r r' = Rundef.

Lemma res_escr_upd r l pi σ :
  res_escr (res_upd r l pi) σ ↔ res_escr r σ.

Lemma res_escr_mupd r l n pi σ :
  res_escr (res_mupd r l n pi) σ ↔ res_escr r σ.

Lemma res_escr_plusE r r' σ :
  res_escr (res_plus r r') σ → res_escr r σ ∨ res_escr r' σ.

Lemma res_escr_plusI r r' σ :
  res_plus r r' ≠ Rundef →
  res_escr r σ ∨ res_escr r' σ → res_escr (res_plus r r') σ.

Lemma res_escr_plus r r' (D: res_plus r r' ≠ Rundef) σ :
  res_escr (res_plus r r') σ ↔ res_escr r σ ∨ res_escr r' σ.

Lemma res_escr_strip :
  ∀ r σ, res_escr (res_strip r) σ ↔ res_escr r σ.

Lemma res_get_sum:
  ∀ r loc τ (S : slist τ) l,
  res_get r loc = p_at τ S →
  rsum l ≠ Rundef →
  In r l →
  ∃ S' : slist τ,
    res_get (rsum l) loc = p_at τ S' ∧
    (∀ s : prot_state τ, In s (SL_list S) → In s (SL_list S')).

Lemma res_get_of_strip_eq r r' l τ S :
  res_strip r = res_strip r' →
  res_get r' l = p_at τ S →
  res_get r l = p_at τ S.

Lemma res_plus_eq_empI r r' :
  r = res_emp → r' = res_emp → res_plus r r' = res_emp.

Lemma rsum_map_map_eq_empI A B f (g: A → B) l :
  (∀ x, In x l → f (g x) = res_emp) →
  rsum (map f (map g l)) = res_emp.

Lemma res_gget_def r mm gone :
  res_gget r mm = None →
  r ≠ Rundef →
  res_plus r (Rdef (fun _ ⇒ p_bot) (gres_one mm gone) (fun _ ⇒ false)) ≠ Rundef.

Lemma res_gget_def2 r p g e mm gone :
  r = Rdef p g e →
  res_gget r mm = None →
  ∃ g', gres_plus g (gres_one mm gone) = Some g' ∧
  res_plus r (Rdef (fun _ ⇒ p_bot) (gres_one mm gone) (fun _ ⇒ false)) = Rdef p g' e.

Lemma res_gget_plus r1 r2 mm :
  res_gget (res_plus r1 r2) mm = None ↔
  res_plus r1 r2 = Rundef ∨
  res_gget r1 mm = None ∧
  res_gget r2 mm = None.

Lemma res_gget_rsum rl mm :
  res_gget (rsum rl) mm = None ↔
  rsum rl = Rundef ∨ ∀ r, In r rl → res_gget r mm = None.

Lemma res_lt_strengthen r r' :
  (r' ≠ Rundef → res_lt r r') → res_lt r r'.

Lemma res_lt_strip_frame r r' f :
  res_lt (res_strip r) (res_strip r') →
  res_plus r f ≠ Rundef →
  res_lt (res_strip (res_plus r f)) (res_strip (res_plus r' f)).

Lemma res_lt_frame_l r r' f : res_lt r r' → res_lt (res_plus f r) (res_plus f r').

Lemma res_lt_frame_r r r' f : res_lt r r' → res_lt (res_plus r f) (res_plus r' f).

Lemma res_lt_plus_l r r' f : res_lt r r' → res_lt r (res_plus f r').

Lemma res_lt_plus_r r r' f : res_lt r r' → res_lt r (res_plus r' f).

Lemma res_lt_plus :
  ∀ r r' (L: res_lt r r') s s' (L' : res_lt s s'),
    res_lt (res_plus r s) (res_plus r' s').

Lemma res_lt_strip_l r r' :
  res_lt (res_strip r) r' ↔ res_lt (res_strip r) (res_strip r').

Lemma res_lt_frame_rev r a b:
  res_lt (res_plus r a) (res_plus r b) →
  res_lt (res_strip r) b →
  res_plus r b ≠ Rundef →
  res_lt a b.

Lemma res_add_strip_stengthen r r' :
  (∃ rem, r = res_plus r' rem) →
  (∃ rem, r = res_plus r' rem ∧ res_lt (res_strip r') rem).