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

Set Implicit Arguments.
Local Open Scope string_scope.

Section GPS_Logic.

Variable IE : interp_env.

Inductive assn :=
  | Pure (P : Prop)
  | Base (P : RProp)
  | Conj (P P' : assn)
  | Disj (P P' : assn)
  | Impl (P P' : assn)
  | Forall A (PP: A → assn)
  | Exists A (PP: A → assn)
  | Star (P P' : assn)
  | Box (P : assn)
  | Uninit (l : nat)
  | Pt (k : fraction) (l v : nat)
  | At (l : nat) (tau : protTy) (s: prot_state tau)
  | Gres (gres : ghost_resource)
  | Escr (escr : escrowTy).

Program Definition Rat l tau s :=
  {| RP_car := fun r ⇒ ∃ S, res_get r l = p_at tau S ∧ In s (SL_list S) |}.
Next Obligation. red; ins; desf. Qed.
Next Obligation.
  ins; desf; exploit res_get_plus; eauto; ins; desf; eauto.
Qed.

Fixpoint assn_sem (P : assn) { struct P } :=
  match P with
    | Pure P ⇒ Rpure P
    | Base P ⇒ P
    | Conj P P' ⇒ Rconj (assn_sem P) (assn_sem P')
    | Disj P P' ⇒ Rdisj (assn_sem P) (assn_sem P')
    | Impl P P' ⇒ Rimpl (assn_sem P) (assn_sem P')
    | Forall PP ⇒ Rforall (fun x ⇒ assn_sem (PP x))
    | Exists PP ⇒ Rexists (fun x ⇒ assn_sem (PP x))
    | Star P P' ⇒ Rstar (assn_sem P) (assn_sem P')
    | Box P ⇒ Rbox (assn_sem P)
    | Uninit l ⇒ Runinit l
    | Pt k l v ⇒ Rpt k l v
    | At l s tau ⇒ Rat l s tau
    | Gres g ⇒ Rgres g
    | Escr sigma ⇒ Rescr sigma
  end.

Definition gimp (P Q : RProp) :=
  ∀ r (SAT: P r), ghost_move IE r Q.

Definition triple P (e : exp) QQ :=
  ∃ P',
    gimp P P' ∧
    ∀ r' (SAT': P' r') n,
      safe IE n e (fun n ⇒ QQ n) r'.

Definition implies (P Q : RProp) := ∀ r (SAT: P r), Q r.

Definition riff (P Q : RProp) := ∀ r, P r ↔ Q r.

Lemma riff_refl P : riff P P.
Proof. done. Qed.

Lemma riff_sym P Q : riff P Q → riff Q P.
Proof. unfold riff; firstorder. Qed.

Lemma riff_trans P Q R : riff P Q → riff Q R → riff P R.
Proof. unfold riff; firstorder. Qed.

Require Import Setoid.

Global Add Parametric Relation : _ riff
  reflexivity proved by riff_refl
  symmetry proved by riff_sym
  transitivity proved by riff_trans
 as riff_rel.

Global Add Parametric Morphism: implies with signature riff ==> riff ==> iff as implies_mor.
Proof. unfold riff; repeat (eexists; ins; desf); instantiate; firstorder. Qed.

Global Add Parametric Morphism: RP_car with signature riff ==> eq ==> iff as RP_car_mor.
Proof. unfold riff; repeat (eexists; ins; desf); instantiate; firstorder. Qed.

Global Add Parametric Morphism: Rstar with signature riff ==> riff ==> riff as Rstar_mor.
Proof. unfold riff; repeat (eexists; ins; desf); instantiate; firstorder. Qed.

Global Add Parametric Morphism: Rconj with signature riff ==> riff ==> riff as Rconj_mor.
Proof. unfold riff; repeat (eexists; ins; desf); instantiate; firstorder. Qed.

Global Add Parametric Morphism: Rdisj with signature riff ==> riff ==> riff as Rdisj_mor.
Proof. unfold riff; repeat (eexists; ins; desf); instantiate; firstorder. Qed.

Global Add Parametric Morphism: Rimpl with signature riff ==> riff ==> riff as Rimpl_mor.
Proof. by split; ins; desf; split; ins; eapply H0, H2, H. Qed.

Global Add Parametric Morphism: Rbox with signature riff ==> riff as Rbox_mor.
Proof. unfold riff; repeat (eexists; ins; desf); instantiate; firstorder. Qed.

Global Add Parametric Morphism A : (@Rforall A)
  with signature (eq ==> riff) ==> riff as Rforall_mor.
Proof. unfold riff; split; ins; desf; split; ins; eapply H; ins. Qed.

Global Add Parametric Morphism A : (@Rexists A)
  with signature (eq ==> riff) ==> riff as Rexists_mor.
Proof. eby unfold riff; split; ins; desf; split; ins; eexists; eapply H; ins. Qed.

Global Add Parametric Morphism: ghost_move
  with signature (eq ==> eq ==> riff ==> iff) as gm_mor.
Proof.
  by unfold riff; split; ins; eapply GM_weaken_post; eauto; ins; eapply H.
Qed.

Global Add Parametric Morphism: gimp
  with signature (riff ==> riff ==> iff) as gimp_mor.
Proof.
  by unfold gimp, riff; split; ins; apply H in SAT;
     eapply GM_weaken_post; eauto; ins; eapply H0.
Qed.

Global Add Parametric Morphism: safe
  with signature (eq ==> eq ==> eq ==> (eq ==> riff) ==> eq ==> iff) as safe_mor.
Proof.
  split; revert y1 y3; induction y0; ins; desf; unnw; repeat split; ins; desf; eauto.
  by rewrite <- (H val); ins; eauto.
  by exploit FORK; eauto; ins; desf; eauto 8.
  by exploit STEP; eauto; intro M; desf; eexists; split; eauto;
     ins; exploit M0; eauto; ins; desf; eauto.
  by rewrite (H val); ins; eauto.
  by exploit FORK; eauto; ins; desf; eauto 8.
  by exploit STEP; eauto; intro M; desf; eexists; split; eauto;
     ins; exploit M0; eauto; ins; desf; eauto.
Qed.

Global Add Parametric Morphism: triple
  with signature (riff ==> eq ==> (eq ==> riff) ==> iff) as triple_mor.
Proof.
  unfold triple; split; ins; desf; eexists P'; split; ins; try rewrite H in *; ins.
  by replace [eta y1] with y1; ins; rewrite <- H0; eauto.
  by replace [eta x0] with x0; ins; rewrite H0; eauto.
Qed.

Lemma Rstar_true P : riff (Rstar P Rtrue) P.
Proof.
  destruct P; split; ins; desf; eauto.
  split; try red; ins; desf.
  by eexists r, res_emp; rewrite res_plus_emp_r.
Qed.

Lemma RstarA P Q R : riff (Rstar (Rstar P Q) R) (Rstar P (Rstar Q R)).
Proof.
  split; ins; desf; split; eauto.
    rewrite res_plusA in *; repeat eexists; eauto.
    by intro X; rewrite X in *; destruct r0; ins.
  rewrite <- res_plusA in *; repeat eexists; eauto.
  by intro X; rewrite X in ×.
Qed.

Lemma RstarC P Q : riff (Rstar P Q) (Rstar Q P).
Proof.
  split; ins; desf; split; rewrite res_plusC in *;
  repeat eexists; eauto.
Qed.

Lemma RstarAC P Q R : riff (Rstar P (Rstar Q R)) (Rstar Q (Rstar P R)).
Proof. by rewrite <- !RstarA, (RstarC P). Qed.

Lemma Rstar_singl a b :
  res_plus a b ≠ Rundef →
  riff (Rstar (Rsingl a) (Rsingl b)) (Rsingl (res_plus a b)).
Proof.
   split; ins; desf; split; ins.
  ∃ (res_plus r'0 r').
  rewrite !res_plusA; f_equal; rewrite <- !res_plusA; f_equal; apply res_plusC.
  rewrite res_plusA in ×.
  eexists a, (res_plus b r'); repeat split; try red; ins; desf; eauto using res_plus_emp_r.
  rewrite H1 in *; destruct a; ins.
Qed.

Lemma star_disj P Q R :
  riff (Rstar P (Rdisj Q R)) (Rdisj (Rstar P Q) (Rstar P R)).
Proof.
  split; ins; desf; eauto 8.
Qed.

Lemma star_exists A P (QQ : A → RProp) :
  riff (Rstar P (Rexists QQ)) (Rexists (fun x ⇒ Rstar P (QQ x))).
Proof.
  split; ins; desf; split; ins; repeat (eexists; eauto).
  intro; desf; ins; rewrite res_plus_undef in *; ins.
Qed.

Lemma guar_def r_pre r' alpha r rx :
  guar IE r_pre r' alpha r rx →
  r ≠ Rundef ∧ rx ≠ Rundef.
Proof.
  destruct alpha; ins; desf; desf; destruct r'; ins;
  unfold atomic_guar in *; desf; destruct r, rx; ins.
Qed.

Lemma res_get_plus_naE r r' (D: res_plus r r' ≠ Rundef) k l v :
  res_get (res_plus r r') l = p_na k v →
  ∃ k', res_get r l = p_na k' v ∨ res_get r' l = p_na k' v.
Proof.
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; vauto;
  rewrite H in *; desf; eauto.
Qed.

Lemma res_get_plus_naI r r' (D: res_plus r r' ≠ Rundef) k l v :
  res_get r l = p_na k v ∨ res_get r' l = p_na k v →
  ∃ k', res_get (res_plus r r') l = p_na k' v.
Proof.
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; desf; eauto.
  rewrite H in *; desf; eauto.
Qed.

Lemma res_get_plus_na_fullI r r' (D: res_plus r r' ≠ Rundef) l v :
  res_get r l = p_na pe_full v ∨ res_get r' l = p_na pe_full v →
  res_get (res_plus r r') l = p_na pe_full v.
Proof.
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; desf; eauto.
  rewrite H in *; desf; eauto.
  by destruct k.
Qed.


Lemma Rstar_at l tau s P r :
  Rstar (Rat l tau s) P r ↔
  P r ∧ ∃ S, res_get r l = p_at tau S ∧ In s (SL_list S).
Proof.
  split; ins; desf; split; ins.
    by rewrite res_plusC in *; eauto using RP_ext.
    by exploit res_get_plus; eauto; ins; desf; eauto.
    by intro; desf.
  eexists (res_strip r),r; rewrite res_plus_strip_l; repeat eexists; eauto.
  by destruct r; ins; rewrite H0.
Qed.

Lemma RP_strip_ext (P : RProp) r r' :
  P (res_strip r) →
  res_plus r r' ≠ Rundef →
  P (res_strip (res_plus r r')).
Proof.
  ins; rewrite res_strip_plus; ins.
  eapply RP_ext; eauto using res_plus_strip2_def.
Qed.

Lemma RP_ext_upd (P : RProp) r l pi :
  P r →
  prot_plus (res_get r l) pi = Some pi →
  P (res_upd r l pi).
Proof.
  ins; cut (res_upd r l pi = res_plus r (res_upd res_emp l pi)).
    by intro X; rewrite X; eapply RP_ext; eauto; rewrite <- X; destruct r, P.
  rewrite prot_plusC, res_plusC in *; destruct r; ins; desf;
  rewrite ?gres_plusI in *; desf; f_equal.

  extensionality l'; eapply lift_plus_some_inv with (l:=l') in Heq.
  destruct (eqnP l' l); ins; desf; ins; desf; destruct pi; ins; desf.

  exfalso; eapply lift_plus_none_inv in Heq; desc.
  destruct (eqnP l0 l); ins; desf; ins; desf; destruct pi; ins; desf.
Qed.

Lemma implies_true : ∀ P, implies P Rtrue.
Proof. red; ins; desf; intro; destruct P; ins; desf. Qed.

Lemma implies_false : ∀ P, implies Rfalse P.
Proof. red; ins; desf. Qed.

Theorem Rbox1 P : implies (Rbox P) P.
Proof.
  red; ins; rewrite <- res_plus_strip_idemp, res_plusC; apply RP_ext; ins.
  rewrite res_plusC, res_plus_strip_idemp; intro; destruct P; ins; desf.
Qed.

Theorem Rbox2 P : implies (Rbox P) (Rbox (Rbox P)).
Proof.
  by red; ins; rewrite res_strip_idemp.
Qed.

Theorem Rstar_box P Q r :
  Rstar P (Rbox Q) r ↔ P r ∧ Q (res_strip r).
Proof.
  split; ins; desf; split; ins; eauto using RP_ext.
  rewrite res_plusC in ×.
  rewrite res_strip_plus; ins; apply RP_ext; eauto.
  rewrite <- res_strip_plus; ins.
   destruct (res_plus r2 r1); ins.
  destruct Q; intro; desf.
  eexists r, (res_strip r); repeat split; eauto using eq_sym, res_plus_strip_idemp.
  by rewrite res_strip_idemp.
Qed.

Corollary Rbox_dupl P :
  riff (Rbox P) (Rstar (Rbox P) (Rbox P)).
Proof. by split; rewrite Rstar_box; ins; desf. Qed.

Theorem implies_box_pure P :
  implies (Rpure P) (Rbox (Rpure P)).
Proof.
  red; ins; desf; destruct r; ins.
Qed.

Corollary Rbox_pure P : riff (Rbox (Rpure P)) (Rpure P).
Proof. by split; [apply Rbox1|apply implies_box_pure]. Qed.

Corollary Rstar_pure P Q r :
  Rstar P (Rpure Q) r ↔ P r ∧ Q.
Proof.
  rewrite <- Rbox_pure, Rstar_box; repeat split; ins; desf.
  destruct P, r; ins.
Qed.

Theorem implies_box_at l tau s :
  implies (Rat l tau s) (Rbox (Rat l tau s)).
Proof.
  red; ins; desf; repeat eexists; eauto.
  by destruct r; ins; rewrite SAT.
Qed.

Corollary Rbox_at l tau s :
  riff (Rbox (Rat l tau s)) (Rat l tau s).
Proof. by split; [apply Rbox1|apply implies_box_at]. Qed.

Corollary Rat_dupl l tau s :
  riff (Rat l tau s) (Rstar (Rat l tau s) (Rat l tau s)).
Proof. rewrite <- Rbox_at; apply Rbox_dupl. Qed.

Theorem implies_box_escr sigma :
  implies (Rescr sigma) (Rbox (Rescr sigma)).
Proof.
  red; ins; desf; destruct r; ins.
Qed.

Corollary Rbox_escr sigma : riff (Rbox (Rescr sigma)) (Rescr sigma).
Proof. by split; [apply Rbox1|apply implies_box_escr]. Qed.

Corollary Rescr_dupl sigma :
  riff (Rescr sigma) (Rstar (Rescr sigma) (Rescr sigma)).
Proof. rewrite <- Rbox_escr; apply Rbox_dupl. Qed.

Lemma Rstar_mono P P' Q Q' :
  implies P P' →
  implies Q Q' →
  implies (Rstar P Q) (Rstar P' Q').
Proof.
  unfold implies, Rstar; ins; desf; repeat eexists; eauto.
Qed.

Lemma RexistsI A (QQ: A → RProp) x :
  implies (QQ x) (Rexists QQ).
Proof.
  split; vauto; intro; destruct (QQ x); desf.
Qed.

Lemma RexistsE A (PP: A → RProp) Q :
  (∀ x, implies (PP x) Q) →
  implies (Rexists PP) Q.
Proof.
  unfold implies, Rexists; ins; desf; eauto.
Qed.

Lemma Rstar_forget_r P P' Q :
  implies P Q →
  implies (Rstar P P') Q.
Proof.
  unfold implies, Rstar; ins; desf; eauto using RP_ext.
Qed.

Lemma Rstar_forget_l P P' Q :
  implies P' Q →
  implies (Rstar P P') Q.
Proof.
  rewrite RstarC; apply Rstar_forget_r.
Qed.

Theorem Rstar_gres1 g g' r :
  Rstar (Rgres g) (Rgres g') r ↔
  ∃ g'', gres_plus g g' = Some g'' ∧ (Rgres g'') r.
Proof.
  destruct (gres_plus g g') as [g''|] eqn: X.

  unfold Rgres; rewrite Rstar_singl; ins;
  rewrite lift_plus_emp_l in *; desf; repeat split; ins; desf; try done;
  rewrite lift_plus_emp_l in *; desf; [eexists; split; split; try done|];
  eexists (Rdef p gres escr); simpl;
  rewrite lift_plus_emp_l in *; desf; done.

  split; intros; desf.
  exfalso; hnf in H; desf.
  hnf in H0, H1; desf; clear H0 H1.
  rewrite !res_plusA, res_plusAC, res_plusC, <- res_plusA in H.
  ins; desf.
Qed.

Theorem Rstar_at0 l tau s tau' s' :
  implies (Rstar (Rat l tau s) (Rat l tau' s'))
          (Rpure (tau = tau')).
Proof.
  red; ins; desf; split; try done.
  destruct r1, r2; ins; desf.
  inv_lplus l; unfold prot_plus, mk_slist in *; desf; clear H0; desf.
Qed.

Theorem Rstar_at1 l tau s s' :
  implies (Rstar (Rat l tau s) (Rat l tau s'))
          (Rpure (prot_trans tau s s' ∨ prot_trans tau s' s)).
Proof.
  red; ins; desf; split; try done.
  destruct r1, r2; ins; desf.
  inv_lplus l; unfold prot_plus, mk_slist in *; desf; clear H0; desf.
  repeat rewrite <- eq_rect_eq in ×.
  eapply a0; eauto using in_or_app.
Qed.

Theorem star_pt_pt k k' l v v' :
  fraction_plus k k' = None →
  riff (Rstar (Rpt k l v) (Rpt k' l v')) Rfalse.
Proof.
  split; ins; desf.
  destruct r1, r2; ins; desf.
  inv_lplus l; rewrite H1, H2 in *; ins; desf; desf.
  eapply fraction_le_none1 in H; eauto;
  eapply fraction_le_none2 in H; eauto; desf.
Qed.

Lemma GM_singl r : r ≠ Rundef → ghost_move IE r (Rsingl r).
Proof. ins; apply GM_base; split; eauto using res_plus_emp_r. Qed.

Lemma GM_frame r1 r2 (Q F : RProp) :
  ghost_move IE r1 Q →
  F r2 →
  res_plus r1 r2 ≠ Rundef →
  ghost_move IE (res_plus r1 r2) (Rstar Q F).
Proof.
  intros until 1; revert r2; induction H; ins; desf.
  econstructor 1; ins; desf; eauto 7.

  econstructor 2; eauto; ins; desf; eauto.

  econstructor 3; eauto; unfold NW; ins; desf.
  rewrite res_plusA, (res_plusC r2), <- res_plusA in *; desf.
  repeat eexists; eauto; eapply PEQ; eauto.
  by intro X; rewrite X in ×.

  ins; desf.
  destruct (gres_plus g' gres) as [g1|] eqn: M.
    2: by apply GDEF in M; desf.
  econstructor 4 with (g':=g1); repeat eexists; ins; eauto; ins; desf.
    case_eq (gres_plus g0 gF) as Y; ins.
    destruct (gres_plusA Heq0 Y) as (gg & ? & ?).
    by destruct (gres_plusA2 M H1); desf; eapply GDEF in H4; desf.
  clear GDEF; unfold gres_plus in *; repeat des_eqrefl; desf; ins.
  clear H0 Heq; inv_lplus gl.
  specialize (GDOM gl); destruct (g gl), (g' gl); ins; desf; try congruence.
  exploit GDOM; congruence.

  rewrite res_plusA, (res_plusC r2), <- res_plusA in ×.
  econstructor 5; try edone; repeat (eexists; try edone); eauto. unfold NW; ins; desf.
    destruct (res_plus r1 r0); ins; clear.
    by rewrite lift_plusC, lift_plus_emp_l, gres_plusC, gres_plusI;
       ins; auto using prot_plusC.
  by rewrite res_plusC, res_plusAC, res_plusA.

  rewrite res_plusA, (res_plusC r2), <- res_plusA in ×.
  econstructor 5; try edone; repeat (eexists; try edone); eauto. unfold NW; ins; desf.
    destruct (res_plus r1 r0); ins; clear.
    by rewrite lift_plusC, lift_plus_emp_l, gres_plusC, gres_plusI;
       ins; auto using prot_plusC.
  by rewrite res_plusC, res_plusAC, res_plusA.

  rewrite res_plusA in ×.
  econstructor 6; eauto; ins; desf.
    by rewrite <- res_plusA in *; apply res_escr_plus; eauto.
  destruct GEL; [left|right]; ins; desf; split; ins;
  rewrite !res_plusA, res_plusAC, res_plusC in H1 |- *;
  exploit (IN' (res_plus r0 (res_plus r' r3))); eauto;
  split; repeat eexists; eauto using res_plusA;
  rewrite <- !res_plusA in *; kundef.
Qed.

Lemma RgresI g r :
  r ≠ Rundef →
  res_lt (Rdef (fun _ ⇒ p_bot) g (fun _ ⇒ false)) r →
  Rgres g r.
Proof. unfold res_lt; intros; desf; split; eauto. Qed.

Theorem gimp_implies P Q :
  implies P Q →
  gimp P Q.
Proof. unfold implies, gimp; eauto using ghost_move. Qed.

Corollary gimp_refl P : gimp P P.
Proof. by apply gimp_implies. Qed.

Theorem gimp_trans :
  ∀ P Q R,
    gimp P Q →
    gimp Q R →
    gimp P R.
Proof. repeat red; ins; eapply GM_trans; eauto. Qed.

Theorem gimp_frame P Q F :
  gimp P Q →
  gimp (Rstar P F) (Rstar Q F).
Proof.
  unfold gimp; ins; desf; eapply GM_frame; eauto.
Qed.

Corollary gimp_frame_l P Q F :
  gimp P Q →
  gimp (Rstar F P) (Rstar F Q).
Proof.
  unfold gimp; ins; desf.
  eapply GM_weaken_post.
    rewrite res_plusC; eapply GM_frame; eauto.
    by rewrite res_plusC.
  by intros; apply RstarC.
Qed.

Corollary gimp_star P Q P' Q' :
  gimp P Q →
  gimp P' Q' →
  gimp (Rstar P P') (Rstar Q Q').
Proof.
  ins; eapply gimp_trans; eauto using gimp_frame, gimp_frame_l, Permutation, Permutation_app_comm.
Qed.

Theorem gimp_eintro sigma P Q :
  interp_exch IE sigma = (P, Q) →
  gimp P (Rescr sigma).
Proof.
  red; ins; eapply GM_eintro with (r1 := res_emp); try edone; instantiate;
  rewrite ?res_plus_emp_l; repeat eexists; eauto using res_plus_emp_r; try red; ins; vauto.
  by destruct P.
Qed.

Theorem gimp_eintro2 sigma P Q :
  interp_exch IE sigma = (P, Q) →
  gimp Q (Rescr sigma).
Proof.
  red; ins; eapply GM_eintro with (r1 := res_emp); try edone; instantiate;
  rewrite ?res_plus_emp_l; repeat eexists; eauto using res_plus_emp_r; try red; ins; vauto.
  by destruct Q.
Qed.

Theorem gimp_eelim sigma P Q :
  interp_exch IE sigma = (P, Q) →
  gimp (Rstar P (Rescr sigma)) Q.
Proof.
  red; ins; desf; eapply GM_eelim; eauto using in_eq.
    by eapply res_escr_plus; ins; eauto.
  left; ins; desf; rewrite res_plusC in *; eapply RP_ext; eauto.
Qed.

Theorem gimp_eelim2 sigma P Q :
  interp_exch IE sigma = (P, Q) →
  gimp (Rstar Q (Rescr sigma)) P.
Proof.
  red; ins; desf; eapply GM_eelim; eauto using in_eq.
    by eapply res_escr_plus; ins; eauto.
  right; ins; desf; rewrite res_plusC in *; eapply RP_ext; eauto.
Qed.

Theorem gimp_or P1 P2 Q :
  gimp P1 Q →
  gimp P2 Q →
  gimp (Rdisj P1 P2) Q.
Proof.
  unfold gimp; ins; desf; eauto.
Qed.

Theorem gimp_exists A PP Q :
  (∀ x : A, gimp (PP x) Q) →
  gimp (Rexists PP) Q.
Proof.
  unfold gimp; ins; desf; eauto.
Qed.

Theorem gimp_gintro g :
  gimp Rtrue (Rexists (fun gamma ⇒ Rgres (gres_one gamma g))).
Proof.
  red; ins; apply GM_extend with (gone:=g).
  split; [|∃ l]; try done.
  apply RgresI; ins; desf; eapply res_lt_plus_l.
  by ∃ (Rdef pmap g0 escr); ins; rewrite lift_plus_emp_l, H.
Qed.

Theorem gimp_gupd gamma g g' :
  (∀ gF, salg_plus (projT1 g) g' gF = None →
              salg_plus (projT1 g) (projT2 g) gF = None) →
  gimp (Rgres (gres_one gamma (Some g)))
       (Rgres (gres_one gamma (Some (existT _ _ g')))).
Proof.
  unfold gimp; ins; desf.
  assert (∃ g1, gres_plus (gres_one gamma (Some (existT _ _ g'))) gres = Some g1).
    unfold gres_plus in *; desf; repeat des_eqrefl; desf; eauto.
    exfalso; clear SAT; symmetry in EQ, EQ0.
    apply lift_plus_none_inv in EQ0; desf; inv_lplus l; ins; desf;
    by destruct g; ins; desf; rewrite H in *; desf.

  desf; eapply GM_update with (g' := g1); eauto.

  intros ? M; case_eq (gres_plus g0 gF) as N; exfalso;
   eapply gres_plusA in N; eauto; desc;
   eapply gres_plusA2 in M; eauto; desf;
  clear - M N H;
  unfold gres_plus in *;
  repeat des_eqrefl; desf;
  symmetry in EQ, EQ0; apply lift_plus_none_inv in EQ;
  desf; inv_lplus l; ins; desf; desf; ins; desf; ins; destruct g; ins;
  desf; rewrite <- eq_rect_eq in *;
  by try rewrite H in *; desf; try rewrite <- H in *; desf.

  unfold gres_plus in *; repeat des_eqrefl; desf; ins.
  clear SAT; inv_lplus gl; desf; ins; desf; congruence.

  apply RgresI; ins.
  by ∃ (Rdef p gres escr); ins; rewrite lift_plus_emp_l, H0.
Qed.

Lemma Permutation_consD A l (a: A) m :
  Permutation l (a :: m) →
  ∃ l1 l2, l = l1 ++ a :: l2 ∧ Permutation (l1 ++ l2) m.
Proof.
  ins.
  assert (X: In a l) by eauto using Permutation_in, Permutation_sym, in_eq.
  apply in_split in X; desf; repeat eexists.
  eauto using Permutation_cons_app_inv, Permutation_sym.
Qed.

Lemma Permutation_nodup_subsetD :
  ∀ A (m l rem l' : list A),
    Permutation l (m ++ rem) →
    NoDup l →
    NoDup l' →
    (∀ a, In a l → In a l') →
    ∃ rem',
      Permutation l' (m ++ rem') ∧
      (∀ x, In x rem → In x rem') ∧
      disjoint m rem'.
Proof.
  induction m; ins; desf.
    by eexists; split; [apply Permutation_refl|split]; eauto using Permutation_in, Permutation_sym.
  eapply Permutation_consD in H; desf.
  assert (M: In a l') by eauto using in_eq, in_or_app.
  eapply in_split in M; destruct M as (k1 & k2 & ?); desf.

  edestruct IHm with (l' := k1 ++ k2) as (r & ? & ? & ?); eauto using NoDup_remove_1.
      ins; eapply NoDup_remove_2 in H0.
      by specialize (H2 a0); rewrite !in_app_iff in *; ins; intuition; desf.
  ∃ r; split; try split; ins.
  by eapply Permutation_sym, Permutation_trans, Permutation_middle;
     eauto using Permutation_sym.
  red; ins; desf; eauto.
  eapply NoDup_remove_2 in H1; destruct H1.
  eapply (Permutation_in _ (Permutation_sym H)), in_or_app; eauto.
Qed.

Theorem rule_conseq :
  ∀ P P' e QQ QQ'
         (PRE: gimp P' P)
         (T: triple P e QQ)
         (POST: ∀ n, gimp (QQ n) (QQ' n)),
    triple P' e QQ'.
Proof.
  red; ins.
  red in T. desf; eexists P'0; split; ins; eauto using gimp_trans.
  eapply T0 in SAT'; clear PRE T0; desf; revert SAT'.
  instantiate (1 := n); clear - POST.
  induction[e r'] n; ins; desf; unfold NW; intuition; desf.
    specialize (POST val).
    by eauto using GM_trans.
  exploit FORK; eauto; intro; desf; repeat eexists; eauto.

  exploit STEP; eauto; intro M; desf; do 2 eexists; eauto; ins.
  exploit M0; eauto; intro; desf; eauto.
Qed.

Corollary rule_pconseq :
  ∀ P P' e QQ
         (PRE: gimp P' P)
         (T: triple P e QQ),
    triple P' e QQ.
Proof.
  ins; eapply rule_conseq; eauto using gimp_refl.
Qed.

Theorem rule_frame :
  ∀ P e QQ F (T: triple P e QQ),
    triple (Rstar P F) e (fun v ⇒ Rstar (QQ v) F).
Proof.
  unfold triple; ins; desf.
  eexists (Rstar P' F); split; ins; desf; eauto using gimp_frame.
  specialize (T0 _ SAT'0 n); clear - T0 SAT'1 SAT'.
  induction[e r1 T0 SAT'] n; ins; desc; unfold NW; repeat split; ins; desf.
    by eauto using GM_frame.
  {
    exploit FORK; eauto; instantiate; clear - SAT'1 SAT' IHn; intro M; desf.
    eexists (res_plus r0 r2), r3; repeat (split; eauto).
    rewrite res_plusC, <- res_plusA; f_equal; apply res_plusC.
    eapply IHn; eauto.
    rewrite res_plusC, <- res_plusA, (res_plusC r2) in SAT'.
    by intro X; rewrite X in SAT'.
  }

  rewrite res_plusA in RELY.
  exploit STEP; eauto; clear STEP FORK END.
  intro X; desf.
  eexists; split; eauto; ins; specialize (X0 _ IN' WPE); desf.
  rewrite <- res_plusA in X0; eexists; eexists; split; eauto.
  eapply IHn; eauto.
  by eapply guar_def in X0; intro Z; rewrite Z in *; desf.
Qed.

Theorem rule_false e QQ : triple Rfalse e QQ.
Proof.
  ∃ Rfalse; split; try red; ins; desf; eauto.
Qed.

Theorem rule_disj :
  ∀ P e QQ (T: triple P e QQ)
         P' (T: triple P' e QQ),
    triple (Rdisj P P') e QQ.
Proof.
  unfold triple; ins; desf.
  ∃ (Rdisj P'0 P'1); split; ins; desf; eauto.
  red; ins; desf; eapply GM_weaken_post; eauto; ins; eauto.
Qed.

Theorem rule_exists :
  ∀ A PP e QQ (T: ∀ x: A, triple (PP x) e QQ),
    triple (Rexists PP) e QQ.
Proof.
  unfold triple; ins; eapply choice in T; desf.
  ∃ (Rexists f); split; ins; desf; [eapply gimp_exists; ins|];
    specialize (T x); desf; eauto.
  eapply gimp_trans; eauto; try eapply gimp_implies; ins.
  by split; vauto; intro; destruct (f x); ins; desf.
Qed.

Lemma triple_conj_pure :
  ∀ (P : Prop) P' e QQ (T: ∀ (HYP: P), triple P' e QQ),
    triple (Rconj (Rpure P) P') e QQ.
Proof.
  unfold triple; ins.
  destruct (classic P).
    specialize (T H); desf; eexists P'0; split; ins.
    eapply gimp_trans; ins; eauto.
    by eapply gimp_implies; red; ins; desf.
  by ∃ Rfalse; split; ins; red; ins; desf.
Qed.

Theorem rule_val P v :
  triple P (Evalue v) (fun z ⇒ if z == v then P else Rfalse).
Proof.
  eexists; split; eauto using gimp_refl; ins.
  destruct n; ins; unfold NW; repeat split; ins; desf; try destruct CTX; desf;
  eauto using ghost_move.
Qed.

Lemma safe_let :
  ∀ n r' e QQ (T : safe IE n e QQ r')
    e' QQ' (T' : ∀ v,
       ∃ P' : RProp,
         gimp (QQ v) P' ∧
         (∀ r', P' r' → ∀ n' (LT: lt n' n), safe IE n' (e' v) QQ' r')),
  safe IE n (Elet e e') QQ' r'.
Proof.
  ins; induction[r' e T T'] n; ins; desf; unnw; repeat (split; ins).
    inv CTX; specialize (FORK _ CTX0 _ eq_refl); desf; eauto.
    repeat eexists; eauto; eapply IHn; eauto.
    by ins; specialize (T' v); desf; ∃ P'; split; ins; eapply T'0; ins;
       auto with arith.
  desf.
    exploit STEP; eauto; instantiate; clear - IHn T'; intro X; desf.
    eexists; split; eauto; ins; exploit X0; eauto; ins; desf; eauto.
    repeat eexists; eauto; eapply IHn; eauto.
    by ins; specialize (T' v); desf; ∃ P'0; split; ins; eapply T'0; ins;
       auto with arith.

  specialize (END _ eq_refl); clear FORK STEP.
  ins; desf; specialize (T' n0); desf.

  eexists (Rstar P' (Rsingl rF)); split; ins; eauto; desf.
    apply GM_frame; eauto using GM_trans; split; eauto using res_plus_emp_r.
    by destruct r'; ins; desf.
  ins; desf.
  rewrite (res_plusC rF), <- res_plusA in ×.
  repeat eexists; ins; eapply T'0; auto with arith; apply RP_ext; eauto.
  by intro X; rewrite X in ×.
Qed.

Theorem rule_let :
  ∀ P e QQ (T: triple P e QQ) e' QQ'
    (T': ∀ v, triple (QQ v) (e' v) QQ'),
    triple P (Elet e e') QQ'.
Proof.
  ins; red in T; desf; eexists P'; split; ins; clear T.
  eapply safe_let; eauto.
  ins; edestruct T' as (? & ? & ?); eauto.
Qed.

Corollary rule_seq :
  ∀ P e Q (T: triple P e (fun _ ⇒ Q)) e' QQ'
    (T': triple Q e' QQ'),
    triple P (Elet e (fun _ ⇒ e')) QQ'.
Proof.
  by ins; eapply rule_let; eauto.
Qed.

Theorem rule_repeat :
  ∀ P e QQ
         (T: triple P e QQ)
         (IMP: implies (QQ 0) P),
    triple P (Erepeat e) (fun r ⇒ Rconj (Rpure (r ≠ 0)) (QQ r)).
Proof.
  unfold triple.
  ins; desf.
  eexists; split; try apply gimp_refl; ins.
  revert r' SAT'.

  induction n using (well_founded_ind Wf_nat.lt_wf).
  destruct n; ins; unnw; repeat split; ins; desf; try (by inv CTX).
  ins; desf.
  eexists (Rstar P' (Rsingl rF)); split.
  eapply GM_frame; ins; vauto; split; try kundef.
    by ∃ res_emp; rewrite res_plus_emp_r.
  ins; desf.
  ∃ (res_plus r1 r'1), res_emp; repeat split; ins.
  by rewrite res_plusAC, res_plusC.
  rewrite res_plusAC, res_plusC in IN'.
  eapply RP_ext with (r' := r'1) in IN'0; [|by intro X; rewrite X in *].
  eapply safe_let; ins; eauto.
  ∃ (QQ v); split; eauto using gimp_refl; ins; desf; desf; eauto.
  destruct n'; ins; unnw; repeat split; ins; desf; try by inv CTX.
  eapply GM_base; ins; repeat split; ins; intro; destruct (QQ val); desf.
Qed.

Theorem rule_fork P e :
  triple P e (fun _ ⇒ Rtrue) →
  triple P (Efork e) (fun _ ⇒ Rtrue).
Proof.
  unfold triple; ins; desf.
  eexists P'; split; ins.
  destruct n; ins; unfold NW; repeat split; ins; desf.
  destruct CTX; ins; desf.
  eexists res_emp, _; rewrite res_plus_emp_l; repeat split; eauto.
  destruct n; ins; unfold NW; repeat split; ins; desf; ins; try destruct CTX; vauto.
Qed.

Theorem rule_alloc_one :
    triple (Rtrue) (Ealloc 0) (fun z ⇒ Runinit z).
Proof.
  eexists; split; eauto using gimp_refl; intros.
  destruct n; hnf; try done; unfold NW; repeat split; try done.
    by inversion 1.
  ins; desf; ins; desf.
  eexists; split; [by apply GM_singl|]; ins; desf.
  eexists (res_mupd (res_plus r' r'1) l 0 p_uninit), _; repeat split; try done.
    rewrite (res_plusC (res_plus _ _)), <- res_plusA in IN', WPE |- ×.
    rewrite (res_plusC r').
    destruct (res_plus r'1 r'); ins; desf; ins; f_equal.
      by extensionality loc; inv_lplus loc; desf; ins; desf.
    apply lift_plus_none_inv in Heq; desf; desf; inv_lplus l0; desf.
    rewrite WPE in *; ins.
    by simpls; unfold prot_plus in *; desf.

  destruct n; hnf; try done; unfold NW; repeat split; ins; desf; desf;
    try by inv CTX.
  rewrite res_plusC; eapply GM_base.
  ins; rewrite res_plusC, <- res_plusA in IN'.
  destruct (res_plus r'1 r'); ins; clear IN'; desf; desf.
  destruct n0; auto with arith.
Qed.

Theorem rule_read_na k l v :
  triple (Rpt k l v) (Eload RATna l) (fun z ⇒ Rconj (Rpt k l v) (Rpure (z = v))).
Proof.
  eexists; split; eauto using gimp_refl; intros.
  destruct n; hnf; try done; unfold NW; repeat split; try done.
    by inversion 1.
  ins; desf; ins; desf.
  eexists; split; [apply GM_singl; congruence|]; ins; desf.
  rewrite res_plusC, <- res_plusA; eexists _, _; repeat split.
    left; rewrite res_plusA, res_plusC; rewrite res_plusA in ×.
    by eapply or_introl, res_get_plus_naI in SAT'; desf; eauto.
  destruct n; hnf; try done; unfold NW; repeat split; ins; desf; desf;
    try by inv CTX.
  rewrite res_plusC; eapply GM_base.
  eapply RP_ext; try split; rewrite ?Rpt_eq; ins; try split; try kundef; eauto.
    by symmetry; destruct r'; ins; desf; inv_lplus l;
       rewrite SAT' in *; ins; desf; desf; eauto.
  rewrite res_plusC, <- res_plusA in *; kundef.
Qed.

Theorem rule_write_na l v v' :
  triple (Rpt pe_full l v) (Estore WATna l v') (fun _ ⇒ Rpt pe_full l v').
Proof.
  eexists; split; eauto using gimp_refl; intros.
  destruct n; hnf; try done; unfold NW; repeat split; try done.
    by inversion 1.
  ins; desf; ins; desf.
  eexists; split; [apply GM_singl; congruence|]; ins; desf.
  rewrite fraction_le_full in *; desf.
  rewrite res_plusA in ×.
  rewrite <- res_plus_upd_l; ins.
  rewrite <- res_plusA, res_plusC, <- res_plusA; eexists _, _; repeat split.
    left; repeat split.
    by right; ∃ v; apply res_get_plus_na_fullI; eauto.

  rewrite <- res_plusA, res_plusC, res_plusAC, <- res_plusA in IN'.
  rewrite res_plusC, res_plus_upd_l; ins; try kundef.
    destruct n; hnf; try done; unfold NW; repeat split; ins; desf; desf;
      try by inv CTX.
    by apply GM_base; ∃ pe_full; split; vauto; apply res_get_upds; kundef.
  by destruct r'; ins; desf; ins; desf; inv_lplus l; rewrite SAT' in *; ins; desf.
  by destruct r'; ins; desf; ins; desf; inv_lplus l; rewrite SAT' in *; ins; desf.
Qed.

Theorem rule_write_na_uninit l v' :
  triple (Runinit l) (Estore WATna l v') (fun _ ⇒ Rpt pe_full l v').
Proof.
  eexists; split; eauto using gimp_refl; intros.
  destruct n; hnf; try done; unfold NW; repeat split; try done.
    by inversion 1.
  ins; desf; ins; desf.
  eexists; split; [apply GM_singl; congruence|]; ins; desf.
  rewrite res_plusA in ×.
  rewrite <- res_plus_upd_l; ins.
  rewrite <- res_plusA, res_plusC, <- res_plusA; eexists _, _; repeat split.
    left; repeat split.
    left; destruct r'; ins; desf; ins; clear Heq Heq2.
    by inv_lplus l; rewrite SAT' in *; ins; desf.
  rewrite <- res_plusA, res_plusC, res_plusAC, <- res_plusA in IN'.
  rewrite res_plusC, res_plus_upd_l; ins; try kundef.
    destruct n; hnf; try done; unfold NW; repeat split; ins; desf; desf;
      try by inv CTX.
    by apply GM_base; ∃ pe_full; split; vauto; apply res_get_upds; kundef.
  by destruct r'; ins; desf; ins; desf; inv_lplus l; rewrite SAT' in *; ins; desf.
  by destruct r'; ins; desf; ins; desf; inv_lplus l; rewrite SAT' in *; ins; desf.
Qed.

Theorem rule_read_acq :
  ∀ tau s P QQ
         (IMP: ∀ s' (FUT: prot_trans tau s s') z,
                 implies (Rstar (interp_prot IE tau s' z) P)
                         (Rbox (QQ s' z))) typ (TYP: is_acquire_rtyp typ) l,
    triple (Rstar (Rat l tau s) P) (Eload typ l)
           (fun z ⇒ Rexists (fun s' ⇒ Rstar (Rat l tau s') (Rstar P (Rbox (QQ s' z))))).
Proof.
  eexists; split; eauto using gimp_refl; intros.
  destruct n; hnf; try done; unfold NW; repeat split; try done.
    by inversion 1.

  rewrite Rstar_at in SAT'; ins; desf; ins; desf.
  eexists; split; [by apply GM_singl|].

  ins; desf.
  generalize IN';
  rewrite ?(res_plusC _ rF), ?res_plusA, ?(res_plusAC rF), res_plusC.
  eexists _, _; repeat split; try done.

    rewrite !res_plusA in ×.
    by destruct (res_get_plus r' l ((res_plus (res_strip rY) (res_plus r'1 rF))) SAT'0);
       desf; eauto.

  destruct n; repeat split; unfold NW; intros; desf; try (by inv CTX).
  assert (Z: ∃ s', QQ s' val (res_strip (res_plus rY r')) ∧ (Rat l tau s') (res_strip rY)). {
    destruct (res_get_plus r' l rF SAT'0); desf.
      by intro X; rewrite X in ×.
    specialize (RELY0 _ _ H); red in RELY0; desf.
    rewrite GRF, H in TOK; ins; desf; ins; desf.
    apply H0, TOK in SAT'1; desf.
    rewrite res_plusC, <- res_plusA in DEF.

    eexists (get_state Srf); split; eauto using res_get_strip_at, get_state_in.
    eapply IMP; repeat split; eauto.
      by eapply prot_trans_trans, get_state_lt; eauto.
    by intro X; rewrite X in ×.
  }

  desc.
  eapply GM_base, RexistsI with (x:=s'), Rstar_at.
  split.
  2: ins; desc; rewrite res_plusAC.
  2: eapply res_get_plus with (r' := res_plus r' r'1) in Z0; desf; eauto.
  2: by rewrite res_plusAC; kundef.

  eapply Rstar_box; split; ins; desf.
    by eapply RP_ext; eauto; kundef.
  desf; rewrite <- res_plusA in ×.
  eapply RP_strip_ext; try (by intro X; rewrite X in *).
  rewrite res_strip_plus, res_strip_idemp, res_plusC, <- res_strip_plus; ins;
  try kundef; try (by intro X; rewrite X in *; ins; destruct (QQ s' val)); eauto.
Qed.

Theorem rule_store_rel_uninit :
  ∀ typ (REL: is_release_wtyp typ) l v tau s,
    triple (Rstar (Runinit l) (interp_prot IE tau s v))
           (Estore typ l v)
           (fun _ ⇒ Rat l tau s).
Proof.
  eexists; split; eauto using gimp_refl; intros.
  destruct n; hnf; try done; unfold NW; repeat split; try done.
    by inversion 1.
  intros; simpl in STEP; desf; simpl in RELY; desf.
  eexists; split.
    clear SAT'.
    eapply GM_frame with (Q := Rsingl r') (F := Rsingl rF); try eapply GM_base; try split;
    eauto using res_plus_emp_r;
    by intro; desf; destruct r'.
  clear RELY1.
    intros.
    rewrite RstarC in SAT'.
    rewrite Rstar_singl in IN'; try done.
    simpl in IN'; desf.
    hnf in SAT'; desf.
    assert (G2 : res_get r2 l = p_uninit).
      by clear - SAT'1; ins; desf; ins; inv_lplus l; desf; ins; desf.
    clear SAT'1.
    assert (G1 : res_get r1 l = p_bot).
      by eapply res_get_plus_uninit2; eauto; rewrite res_plusC.
    assert (GF : res_get rF l = p_bot).
      eapply res_get_plus_uninit2; eauto; rewrite res_plusA in ×.
      by intro M; rewrite M in *; destruct r1.
    assert (G' : res_get r'1 l = p_bot).
      eapply res_get_plus_uninit2; eauto; rewrite res_plusC, res_plusA in ×.
      rewrite (res_plusAC r2), <- res_plusA in IN'.
      by intro M; rewrite M in ×.

  unfold guar, atomic_guar, NW, env_move; ins; desf.
  ∃ (res_upd (res_plus r2 r'1) l (p_at tau (mk_slist_singl tau s))).
  ∃ (res_upd r1 l (p_at tau (mk_slist_singl tau s))).

  assert (FOO: res_plus (res_plus (res_plus r2 r'1) rF) r1 ≠ Rundef).
    intro X; destruct IN'; rewrite <- X; clear.
    rewrite !res_plusA, (res_plusAC _ r1); f_equal.
    by rewrite !(res_plusAC rF); eauto using f_equal, res_plusC.

  assert (EQ: res_plus (res_upd (res_plus r2 r'1) l (p_at tau (mk_slist_singl tau s))) rF
          = res_upd (res_plus (res_plus r2 r'1) rF) l (p_at tau (mk_slist_singl tau s))).
    by apply res_plus_upd_l; ins; intro X; rewrite X in ×.

  rewrite EQ, !res_get_upds; try (by intro M; rewrite M in *; desf).
  rewrite res_plus_upd_upd with (pi'' := p_at tau (mk_slist_singl tau s)); try done.
  2: by unfold prot_plus; desf; rewrite <- eq_rect_eq, mk_slist_idemp in *; desf.

  repeat eexists; eauto.
    right; repeat eexists; eauto.
    by eapply RP_ext_upd; eauto; rewrite G1.
  f_equal; rewrite !res_plusA, (res_plusAC _ r1); f_equal.
  rewrite !(res_plusAC rF); eauto using f_equal, res_plusC.

  by left; split; ins; rewrite 2!res_get_plus_bot_r, res_get_plus_bot_l.

  by intro X; desf; rewrite res_get_plus_bot_r, res_get_plus_bot_l, G2 in X; ins.

  by ins; desf; rewrite res_get_plus_bot_r, res_get_plus_bot_l, G2 in TOK; ins.

  destruct n; ins; unfold NW; repeat split; ins; desf; try (by inv CTX).
  by eapply GM_base; ins; eexists; split; try eapply res_get_upds; ins; eauto; intro X; rewrite X in ×.
Qed.

Theorem rule_store_rel :
  ∀ typ (REL: is_release_wtyp typ) tau s v P Q s''
         (GHP: gimp P (Rstar (interp_prot IE tau s'' v) Q))
         (IMP: ∀ s' (FUT: prot_trans tau s s') v' r
                      (SAT: Rstar (interp_prot IE tau s' v') P r),
                 prot_trans tau s' s'') l,
    triple (Rstar (Rat l tau s) P) (Estore typ l v)
           (fun _ ⇒ Rstar (Rat l tau s'') Q).
Proof.
  eexists; split; eauto using gimp_refl; intros.
  destruct n; hnf; try done; unfold NW; repeat split; try done.
    by inversion 1.
  rewrite Rstar_at in SAT'; ins; desf; ins; desf.

  assert (M: ∃ S1, res_get (res_plus r' rF) l = p_at tau S1 ∧
               (∀ s, In s (SL_list S) → In s (SL_list S1))).
    destruct r', rF; ins; desf; ins.
    eapply lift_plus_some_inv with (l:=l) in Heq.
    by rewrite SAT'0 in *; ins; desf; eauto 6 using In_mk_slist, in_or_app.
  desf.
  specialize (RELY1 eq_refl _ _ M); desc.

  assert (∀ s0, In s0 (SL_list S1) → prot_trans tau s0 s'').
    red in RELY1; desf; rewrite M in *; ins; desf; desf.
    eapply prot_trans_trans; [eby eapply get_state_lt2|].
    eapply IMP with (r := res_plus rY r'); [eby eapply get_state_lt2; eauto|];
    repeat eexists; eauto.
    by intro X; rewrite res_plusC, <- res_plusA, X in DEF.

  specialize (GHP _ SAT').
  eexists; split.
    rewrite <- (res_plus_strip_idemp r'), res_plusA in RELY0 |- ×.
    apply GM_frame with (F := Rstar (Rat l tau (get_state S)) (Rsingl rF)); try split;
    eauto using res_plus_emp_r.
    by intro X; rewrite X, res_plusC in ×.
    eexists (res_strip r'), rF.
    split; ins; eauto using res_get_strip_at, get_state_in.
    by repeat split; eauto using res_plus_emp_r; intro X; rewrite X in *; destruct r'.

  intros.
  rewrite RstarAC, Rstar_at, RstarA in IN'; ins; desf.
  specialize (WPE eq_refl _ _ _ M IN'0); desf.
  desf.
  red in WPE0; desf.
  rewrite res_plusC in DEF.
  rewrite GRF in *; desf.

  destruct (mk_slist tau (s'' :: SL_list S0)) as [S''|] eqn: Z.
  2: exfalso; unfold mk_slist in *; desf; destruct n0; split; ins.
  2: rewrite slist_ltD in ×.
  2: desf; desf; eauto using prot_trans_refl; [left|right|];
     try eapply prot_trans_trans with (get_state S0); eauto using get_state_lt;
     try rewrite <- WPE0; eauto using get_state_in;
     try eapply prot_trans_trans with (get_state Sxxx); eauto;
     try eapply IMP with (r := res_plus r_env (res_plus r' rF)); try split; eauto 7 using RP_ext;
     eauto using get_state_in, prot_trans_trans, get_state_lt.
  2: by destruct S0; eapply Sorted_total; eauto; ins; try apply prot_trans_ord.

  ins; desf.
  red in RELY1; desf; rewrite M in *; ins; desf; desf.
  assert (FOO:
    res_plus (res_upd (res_plus r0 r'1) l (p_at tau S'')) rF =
    res_upd (res_plus (res_plus r0 r'1) rF) l (p_at tau S'')).
    apply res_plus_upd_l2.
      by intro X; destruct IN'3; rewrite res_plusAC, res_plusC, X.
      rewrite !(res_plusAC rF) in IN'0.
    eapply prot_plus_get_helper with (r' := res_plus r1 (res_plus r0 r'1)); try done.
    rewrite IN'0.
    by eauto using prot_plus_at_bounded, in_cons, In_mk_slist.
    by rewrite IN'0.

  eexists (res_upd (res_plus r0 r'1) l (p_at tau S'')),
          (res_upd r1 l (p_at tau S'')); unfold NW; repeat split; ins.
  right; repeat split; ins.
  red; unfold NW.

{
  eexists _,s'',S''; repeat (eexists; try edone); rewrite ?res_get_upds; try done.

  eapply RP_ext_upd; eauto.
   eapply prot_plus_get_helper; eauto; try done.
    by eauto using prot_plus_at_bounded, in_cons, In_mk_slist.

  erewrite FOO, res_plus_upd_upd; f_equal; eauto.
   by rewrite res_plusC, !res_plusA; do 2 f_equal; apply res_plusC.
  by rewrite res_plusC, !res_plusA, (res_plusC _ rF).
  by ins; desf; desf; rewrite <- eq_rect_eq, mk_slist_idemp in *; desf.

  rewrite FOO, res_get_upds; ins.
  by rewrite res_plusA, (res_plusC _ rF); intro X; rewrite X in *; destruct r0.

  by intro; desf.

  right; eexists; split; eauto; split.
    intros; rewrite slist_ltD in ×.
    intros; eapply prot_trans_trans; [eby eapply get_state_lt|].
    intros; eapply prot_trans_trans; eauto.
    eapply IMP with (r := res_plus r_env (res_plus r' rF)); try split;
      eauto 7 using RP_ext;
      eauto using get_state_in, prot_trans_trans, get_state_lt.

  unfold mk_slist in *; desf; ins.
  by rewrite in_undup_iff, In_sort; ins; intuition.
}

  red in RELY; desf; rewrite res_get_upds; try (by destruct r0); try (by intro; desf).
  rewrite M, GRF0 in *; ins; desf; ∃ eq_refl; ins; red; ins.
  eexists s''; split; eauto using In_mk_slist, in_eq.
  eapply prot_trans_trans; [eby eapply get_state_lt|].
  eapply IMP with (r := res_plus rE r'); [eby eapply get_state_lt2; eauto|].
      repeat eexists; eauto.
      by intro X; rewrite res_plusC, <- res_plusA, X in DEF1.

  destruct n; ins; unfold NW; repeat split; ins; desf; try by inv CTX.
  eapply GM_base.
  rewrite Rstar_at; split.
  eapply RP_ext_upd; eauto using RP_ext.
     rewrite !(res_plusAC rF), <- res_plusA, res_plusC in IN'0.

     eapply prot_plus_get_helper; eauto; try done.
      by eauto using prot_plus_at_bounded, in_cons, In_mk_slist.

  by rewrite res_get_upds; repeat eexists; eauto using In_mk_slist, in_eq.
Qed.

Theorem rule_cas :
  ∀ typ1 (R1: is_release_utyp typ1) (A1: is_acquire_utyp typ1)
    typ2 (A2: is_acquire_rtyp typ2) tau s vo vn P Q R
    (GHP: ∀ s' (FUT: prot_trans tau s s'),
          gimp (Rstar (interp_prot IE tau s' vo) P)
               (Rexists (fun s'' ⇒ Rconj (Rpure (prot_trans tau s' s''))
                                (Rstar (interp_prot IE tau s'' vn) (Q s''))))) l
    (IMP: ∀ s'' (FUT: prot_trans tau s s'') y (NEQ: y ≠ vo),
                 implies (Rstar (interp_prot IE tau s'' y) P) (Rbox (R s''))),
  triple (Rstar (Rat l tau s) P)
         (Ecas typ1 typ2 l vo vn)
         (fun z ⇒ Rexists (fun s'' ⇒
                      Rstar (Rat l tau s'')
                            (if z == 0 then Rstar P (Rbox (R s''))
                             else (Q s'')))).
Proof.
  eexists; split; eauto using gimp_refl; intros.
  destruct n; hnf; try done; unfold NW; repeat split; try done.
    by inversion 1.
  rewrite Rstar_at in SAT'; ins; desf; ins; desf.
  specialize (RELY eq_refl eq_refl); desf.

Case "cas succeeded".
  assert (M: ∃ S1, res_get (res_plus r' rF) l = p_at tau S1 ∧
               (∀ s, In s (SL_list S) → In s (SL_list S1))).
    destruct r', rF; ins; desf; ins.
    eapply lift_plus_some_inv with (l:=l) in Heq.
    by rewrite SAT'0 in *; ins; desf; eauto 6 using In_mk_slist, in_or_app.
  desf.
  specialize (RELY _ _ M); red in RELY; desf.

  rewrite M, GRF in *; ins; desc; subst tau0.
  assert (TR: prot_trans tau s (get_state Srf)).
    by eapply M0, TOK in SAT'1; desf;
       eauto using prot_trans_trans, get_state_lt.
  rewrite res_plusC, <- res_plusA in DEF |- ×.

  exploit (GHP _ TR (res_plus rY r')); clear GHP.
    by split; eauto; kundef.
  intro GM.
  eexists; split.
    apply GM_frame with (F := (Rsingl rF)); try split;
    eauto using res_plus_emp_r.
    by intro X; rewrite X, res_plusC in ×.

  intros.
  destruct (res_get_plus2 _ _ (res_plus r' rF) GRF M) as (S' & GG & CONT).
    by rewrite res_plusC.
  rewrite <- res_plusA in GG.
  specialize (WPE eq_refl eq_refl _ _ GG); desf.
  ins; desf; rename x into s''.

  assert (WPE1: get_state Srf = get_state S').
    apply (prot_trans_ord tau).
      by apply get_state_lt, CONT; eauto using get_state_in.
    assert (X := get_state_in S'); apply CONT in X; desf; eauto using get_state_lt.
    by apply TOK in X; desf; eauto using get_state_lt, prot_trans_trans.

  destruct (mk_slist tau (s'' :: SL_list Su)) as [S''|] eqn: Z.
  2: exfalso; unfold mk_slist in *; desf; destruct n0; split; ins.
  2: desf; desf; eauto using prot_trans_refl; [left|right|];
     try eapply prot_trans_trans with (get_state Su); eauto using get_state_lt;
     try rewrite <- WPE0, <- WPE1; eauto using get_state_in.
  2: by destruct Su; eapply Sorted_total; eauto; ins; try apply prot_trans_ord.

  clear IN'4 IN'5.
  assert (FOO:
    res_plus (res_upd (res_plus r3 r'1) l (p_at tau S'')) rF =
    res_upd (res_plus (res_plus r3 r'1) rF) l (p_at tau S'')).
    rewrite !res_plusA, (res_plusAC r3), !(res_plusC _ r'1), (res_plusAC r'1),
        <- res_plusA in IN', WPE.

    apply res_plus_upd_l2.
      by intro X; destruct IN'; rewrite res_plusAC, res_plusC, X.
    eapply prot_plus_get_helper with (r' := res_plus (res_plus r3 r'1) r0); try done.
    rewrite res_plusC, res_plusA, WPE.
    by eauto using prot_plus_at_bounded, in_cons, In_mk_slist.
    by rewrite res_plusC, res_plusA, WPE.

  eexists (res_upd (res_plus r3 r'1) l (p_at tau S'')),
          (res_upd r0 l (p_at tau S'')); unfold NW; repeat split; ins; eauto.
  2: congruence.

{
  red; unfold NW.
  rewrite FOO, !res_get_upds, res_plus_upd_upd with (pi'' := p_at tau S'');
  eauto.

  eexists _,s'',S''; repeat (eexists; try edone); rewrite ?res_get_upds; try done.

    eapply RP_ext_upd; eauto.
    rewrite res_plusA in ×.
    eapply prot_plus_get_helper; eauto; try done.
    by eauto using prot_plus_at_bounded, in_cons, In_mk_slist.

  by rewrite res_plusC, !res_plusA, (res_plusC rF).

  right; eexists; split; eauto; split.
    intros; eapply prot_trans_trans; eauto.
    eapply prot_trans_trans; [eby eapply get_state_lt|].
    by rewrite <- WPE0, WPE1; apply prot_trans_refl.
  unfold mk_slist in *; desf; ins.
  by rewrite in_undup_iff, In_sort; ins; intuition.

  by rewrite res_plusC; revert IN'; clear; rewrite !res_plusA, (res_plusC rF).

  by simpl; desf; desf; rewrite <- eq_rect_eq, mk_slist_idemp in *; desf.

  by intro; desf.
  intro X; destruct IN'; clear - X.
  by rewrite !res_plusA in *; rewrite (res_plusC rF), X, res_plusC.
}

  destruct n; ins; unfold NW; repeat split; ins; desf; desf; try by inv CTX.
  eapply GM_base.
  rewrite !res_plusA, (res_plusAC r3), !(res_plusC _ r'1), (res_plusAC r'1),
          <- res_plusA in IN', WPE.
  split; [by destruct (res_plus r3 r'1)|].
  eexists s''.
  rewrite Rstar_at; split.
  eapply RP_ext_upd; try apply RP_ext; eauto.
    by destruct (res_plus r3 r'1).

     eapply prot_plus_get_helper; eauto; try done.
      by eauto using prot_plus_at_bounded, in_cons, In_mk_slist.

  by rewrite res_get_upds; repeat eexists; eauto using In_mk_slist, in_eq;
     destruct (res_plus r3 r'1).

Case "cas failed".
  eexists; split; [by apply GM_singl|].
  ins; desf.
  generalize IN';
    rewrite ?(res_plusC _ rF), ?res_plusA, ?(res_plusAC rF), res_plusC.
  eexists _, _; repeat split; try done.

    rewrite !res_plusA in ×.
    by destruct (res_get_plus r' l ((res_plus (res_strip rY) (res_plus r'1 rF))) SAT'0);
       desf; eauto.

  destruct n; repeat split; unfold NW; intros; desf; try (by inv CTX); try done.
  eapply GM_base; intros.
  split; [by intro X; rewrite X in *|].

  assert (Z: ∃ s', R s' (res_strip (res_plus rY r'))
                        ∧ (Rat l tau s') (res_strip rY)). {
    destruct (res_get_plus r' l rF SAT'0); desf.
      by intro X; rewrite X in ×.
    specialize (RELY0 _ _ H); red in RELY0; desf.
    rewrite GRF, H in TOK; ins; desf; ins; desf.
    apply H0, TOK in SAT'1; desf.
    rewrite res_plusC, <- res_plusA in DEF.

    eexists (get_state Srf); split; eauto using res_get_strip_at, get_state_in.
    eapply IMP; repeat split; eauto.
      by eapply prot_trans_trans, get_state_lt; eauto.
    by intro X; rewrite X in ×.
  }

  desf; ∃ s'.

  rewrite Rstar_at, Rstar_box; repeat split.
    by eapply RP_ext; eauto; intro X; rewrite X in ×.

    rewrite <- res_plusA in ×.
    eapply RP_strip_ext; try (by intro X; rewrite X in *).
    rewrite res_strip_plus, res_strip_idemp, res_plusC, <- res_strip_plus; ins;
      intro X; rewrite X in *; ins.
    by destruct (R s').

  ins; desf; apply res_get_plus with (r' := res_plus r' r'1) in Z0; desc;
  rewrite res_plusAC; try kundef; eauto.
Qed.

End GPS_Logic.