rel_tactics.v 17.3 KB
Newer Older
1 2 3
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics sel_patterns.
From iris.proofmode Require Export tactics.
4
From iris_logrel.F_mu_ref_conc Require Import rules rules_binary hax.
5 6
From iris_logrel.F_mu_ref_conc Require Export lang logrel_binary relational_properties.
From iris_logrel.F_mu_ref_conc.proofmode Require Export tactics classes.
7 8 9
Set Default Proof Using "Type".
Import lang.

Dan Frumin's avatar
Dan Frumin committed
10
(** General tactics *)
11
Lemma tac_rel_bind_l `{logrelG Σ} e' K Δ E1 E2 Γ e t Δ' τ :
12
  e = fill K e' 
13 14
  (Δ  bin_log_related E1 E2 Δ' Γ (fill K e') t τ) 
  (Δ  bin_log_related E1 E2 Δ' Γ e t τ).
15
Proof. intros. subst. eauto. Qed.
16

17
Lemma tac_rel_bind_r `{logrelG Σ} t' K Δ E1 E2 Γ e t Δ' τ :
18
  t = fill K t' 
19 20
  (Δ  bin_log_related E1 E2 Δ' Γ e (fill K t') τ) 
  (Δ  bin_log_related E1 E2 Δ' Γ e t τ).
21
Proof. intros. subst. eauto. Qed.
22

23
Ltac tac_bind_helper :=
24 25 26 27 28 29 30 31 32 33 34 35
  lazymatch goal with   
  | |- fill ?K ?e = fill _ ?efoc =>
     reshape_expr e ltac:(fun K' e' =>
       unify e' efoc;
       let K'' := eval cbn[app] in (K' ++ K) in
       replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app))
  | |- ?e = fill _ ?efoc =>
     reshape_expr e ltac:(fun K' e' =>
       unify e' efoc;
       replace e with (fill K' e') by (by rewrite ?fill_app))
  end; reflexivity.

36 37
Ltac rel_reshape_cont_r tac :=
  lazymatch goal with
38
  | |- _  bin_log_related _ _ _ _ _ (fill ?K ?e) _ =>
39 40
    reshape_expr e ltac:(fun K' e' =>
      tac (K' ++ K) e')
41
  | |- _  bin_log_related _ _ _ _ _ ?e _ =>
42 43 44
    reshape_expr e ltac:(fun K' e' => tac K' e')
  end.

45 46
Ltac rel_reshape_cont_l tac :=
  lazymatch goal with
47
  | |- _  bin_log_related _ _ _ _ (fill ?K ?e) _ _ =>
48 49
    reshape_expr e ltac:(fun K' e' =>
      tac (K' ++ K) e')
50
  | |- _  bin_log_related _ _ _ _ ?e _ _ =>
51 52 53
    reshape_expr e ltac:(fun K' e' => tac K' e')
  end.

54 55 56 57 58 59 60
Tactic Notation "rel_bind_l" open_constr(efoc) :=
  iStartProof;
  eapply (tac_rel_bind_l efoc);
  [ tac_bind_helper
  | (* new goal *) 
  ].

Dan Frumin's avatar
Dan Frumin committed
61 62 63 64 65
Ltac rel_bind_ctx_l K :=
  eapply (tac_rel_bind_l _ K);
  [reflexivity || tac_bind_helper
  |].

66 67 68
Tactic Notation "rel_bind_r" open_constr(efoc) :=
  iStartProof;
  eapply (tac_rel_bind_r efoc);
Dan Frumin's avatar
Dan Frumin committed
69
  [tac_bind_helper
70 71 72
  | (* new goal *) 
  ].

Dan Frumin's avatar
Dan Frumin committed
73 74 75 76 77
Ltac rel_bind_ctx_r K :=
  eapply (tac_rel_bind_r _ K);
  [reflexivity || tac_bind_helper
  |].

78
Tactic Notation "rel_vals" :=
Dan Frumin's avatar
Dan Frumin committed
79
  iStartProof;
Dan Frumin's avatar
Dan Frumin committed
80 81 82 83 84 85 86 87 88 89 90 91 92 93
  iApply bin_log_related_val; [ try solve_to_val | try solve_to_val | simpl ].


Tactic Notation "rel_apply_l" open_constr(lem) :=
  iStartProof;
  rel_reshape_cont_l ltac:(fun K e =>
    rel_bind_ctx_l K; iApply lem; tac_rel_done; try iNext; simpl_subst/=)
  || fail "rel_apply_l: Cannot apply " lem.

Tactic Notation "rel_apply_r" open_constr(lem) :=
  iStartProof;
  rel_reshape_cont_r ltac:(fun K e =>
    rel_bind_ctx_r K; iApply lem; tac_rel_done; try iNext; simpl_subst/=)
  || fail "rel_apply_r: Cannot apply " lem.
Dan Frumin's avatar
Dan Frumin committed
94

95
(** Pure reductions *)
Dan Frumin's avatar
Dan Frumin committed
96

97 98 99 100
Lemma tac_rel_pure_l `{logrelG Σ} K e1 Δ' E1 E2 Δ Γ e e2 ϕ t τ (b : bool) :
  e = fill K e1 
  PureExec ϕ e1 e2 
  ϕ 
Dan Frumin's avatar
Dan Frumin committed
101
  Closed  e1 
102 103 104
  ((b = true  E1 = E2)  b = false) 
  (Δ'  ?b bin_log_related E1 E2 Δ Γ (fill K e2) t τ) 
  (Δ'  bin_log_related E1 E2 Δ Γ e t τ).
Dan Frumin's avatar
Dan Frumin committed
105
Proof.
106 107 108
  intros Hfill Hpure Hϕ ? Hb Hp. subst.
  assert (Closed  e2).
  { eapply PureExec_Closed; eauto. }
109 110 111 112 113 114 115 116 117 118
  destruct b.
  - destruct Hb as [[_ ?] | Hb']; last by inversion Hb'. subst.    
    rewrite -(bin_log_pure_l Δ Γ E2 K e1 e2 t τ).
    { exact Hp. }
    { apply pure_exec_safe. exact Hϕ. }
    { apply pure_exec_puredet. exact Hϕ. }
  - rewrite -(bin_log_pure_masked_l Δ Γ E1 E2 K e1 e2 t τ).
    { exact Hp. }
    { apply pure_exec_safe. exact Hϕ. }
    { apply pure_exec_puredet. exact Hϕ. }
Dan Frumin's avatar
Dan Frumin committed
119 120
Qed.

121
Tactic Notation "rel_pure_l" open_constr(ef) :=
Dan Frumin's avatar
Dan Frumin committed
122
  iStartProof;
123 124 125 126 127 128 129 130 131 132 133
  rel_reshape_cont_l ltac:(fun K e' =>
      unify e' ef;
      simple eapply (tac_rel_pure_l K e');
      [tac_bind_helper             (* e = fill K e1' *)
      |apply _                     (* PureExec ϕ e1 e2 *)
      |try (exact I || reflexivity || tac_rel_done)
      |try (simpl; solve_closed)           (* Closed  e1 *)
      |first [left; split; reflexivity | right; reflexivity] (* E1 = E2? *)
      |try iNext; simpl_subst/= (* new goal *)])
  || fail "rel_pure_l: cannot find the reduct".

134
Tactic Notation "rel_rec_l" := rel_pure_l (App (Rec _ _ _) _) || rel_pure_l (App _ _).
135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
Tactic Notation "rel_seq_l" := rel_rec_l.
Tactic Notation "rel_let_l" := rel_rec_l.
Tactic Notation "rel_fst_l" := rel_pure_l (Fst (Pair _ _)).
Tactic Notation "rel_snd_l" := rel_pure_l (Snd (Pair _ _)).
Tactic Notation "rel_proj_l" := rel_pure_l (_ (Pair _ _)).
Tactic Notation "rel_unfold_l" := rel_pure_l (Unfold (Fold _)).
Tactic Notation "rel_fold_l" := rel_unfold_l.
Tactic Notation "rel_if_l" := rel_pure_l (If _ _ _).
Tactic Notation "rel_if_true_l" := rel_pure_l (If true _ _).
Tactic Notation "rel_if_false_l" := rel_pure_l (If false _ _).
Tactic Notation "rel_case_inl_l" := rel_pure_l (Case (InjL _) _ _).
Tactic Notation "rel_case_inr_l" := rel_pure_l (Case (InjL _) _ _).
Tactic Notation "rel_case_l" := rel_pure_l (Case _ _ _).
Tactic Notation "rel_op_l" := rel_pure_l (BinOp _ _ _).

Lemma tac_rel_pure_r `{logrelG Σ} K e1 Δ' E1 E2 Δ Γ e e2 ϕ t τ :
  e = fill K e1 
  PureExec ϕ e1 e2 
  ϕ 
Dan Frumin's avatar
Dan Frumin committed
154
  Closed  e1 
155 156 157
  nclose specN  E1 
  (Δ'  bin_log_related E1 E2 Δ Γ t (fill K e2) τ) 
  (Δ'  bin_log_related E1 E2 Δ Γ t e τ).
158
Proof.
159 160 161
  intros Hfill Hpure Hϕ ?? Hp. subst.
  assert (Closed  e2).
  { eapply PureExec_Closed; eauto. }
162 163 164 165 166 167 168 169
  rewrite -(bin_log_pure_r Δ Γ E1 E2 K e1 e2 t τ).
  { exact Hp. }
  { assumption. } 
  { intros σ.
    destruct Hpure as [Hsafe Hstep].
    destruct (Hsafe Hϕ σ) as [e2' [σ2' [? Hstep']]]. 
    destruct (Hstep Hϕ _ _ _ _ Hstep') as (? & ? & ?); subst.
    done. }
170 171
Qed.

172
Tactic Notation "rel_pure_r" open_constr(ef) :=
173
  iStartProof;
174 175 176 177 178 179 180 181 182 183 184
  rel_reshape_cont_r ltac:(fun K e' =>
      unify e' ef;
      simple eapply (tac_rel_pure_r K e');
      [tac_bind_helper             (* e = fill K e1' *)
      |apply _                     (* PureExec ϕ e1 e2 *)
      |try (exact I || reflexivity || tac_rel_done)
      |try (simpl; solve_closed)           (* Closed  e1 *)
      |solve_ndisj                 (* specN  E1 *)
      |try iNext; simpl_subst/=    (* new goal *)])
  || fail "rel_pure_r: cannot find the reduct".

185
Tactic Notation "rel_rec_r" := rel_pure_r (App (Rec _ _ _) _) || rel_pure_r (App _ _).
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201
Tactic Notation "rel_seq_r" := rel_rec_r.
Tactic Notation "rel_ret_r" := rel_rec_r.
Tactic Notation "rel_fst_r" := rel_pure_r (Fst (Pair _ _)).
Tactic Notation "rel_snd_r" := rel_pure_r (Snd (Pair _ _)).
Tactic Notation "rel_proj_r" := rel_pure_r (_ (Pair _ _)).
Tactic Notation "rel_unfold_r" := rel_pure_r (Unfold (Fold _)).
Tactic Notation "rel_fold_r" := rel_unfold_r.
Tactic Notation "rel_if_r" := rel_pure_r (If _ _ _).
Tactic Notation "rel_if_true_r" := rel_pure_r (If true _ _).
Tactic Notation "rel_if_false_r" := rel_pure_r (If false _ _).
Tactic Notation "rel_case_inl_r" := rel_pure_r (Case (InjL _) _ _).
Tactic Notation "rel_case_inr_r" := rel_pure_r (Case (InjL _) _ _).
Tactic Notation "rel_case_r" := rel_pure_r (Case _ _ _).
Tactic Notation "rel_op_r" := rel_pure_r (BinOp _ _ _).

(** Stateful reductions *)
202

203
Lemma tac_rel_fork_l `{logrelG Σ} Δ1 E1 E2 e' K' Γ e t Δ' τ :
204 205
  e = fill K' (Fork e') 
  Closed  e' 
206 207
  (Δ1  |={E1,E2}=>  WP e' {{ _ , True }}  bin_log_related E2 E1 Δ' Γ (fill K' (Lit Unit)) t τ) 
  (Δ1  bin_log_related E1 E1 Δ' Γ e t τ).
208 209 210
Proof.
  intros ???.
  subst e.
211
  rewrite -(bin_log_related_fork_l Δ' Γ E1 E2); eassumption.
212 213 214 215 216 217 218 219 220
Qed.

Tactic Notation "rel_fork_l" :=
  iStartProof;
  eapply (tac_rel_fork_l);
    [tac_bind_helper || fail "rel_fork_l: cannot find 'fork'"
    |solve_closed
    |simpl (* new goal *) ].

Dan Frumin's avatar
Dan Frumin committed
221
Tactic Notation "rel_alloc_l_atomic" := rel_apply_l bin_log_related_alloc_l.
222

223
Lemma tac_rel_alloc_l_simp `{logrelG Σ} Δ1 Δ2 E1 e' v' K' Γ e t Δ' τ :
224
  e = fill K' (Alloc e') 
Dan Frumin's avatar
Dan Frumin committed
225
  IntoLaterNEnvs 1 Δ1 Δ2 
226
  to_val e' = Some v' 
Dan Frumin's avatar
Dan Frumin committed
227
  (Δ2   l,
228 229
     (l ↦ᵢ v' - bin_log_related E1 E1 Δ' Γ (fill K' (Loc l)) t τ)) 
  (Δ1  bin_log_related E1 E1 Δ' Γ e t τ).
230 231 232
Proof.
  intros ???.
  subst e.
Dan Frumin's avatar
Dan Frumin committed
233
  rewrite into_laterN_env_sound /=.
234
  rewrite -(bin_log_related_alloc_l' Δ' Γ E1); eauto.
Dan Frumin's avatar
Dan Frumin committed
235
  apply uPred.later_mono.
236 237 238 239
Qed.

Tactic Notation "rel_alloc_l" "as" ident(l) constr(H) :=
  iStartProof;
Dan Frumin's avatar
Dan Frumin committed
240 241 242 243 244
  eapply tac_rel_alloc_l_simp;
    [tac_bind_helper       (* e = fill K' .. *)
    |apply _               (* IntoLaterNEnvs _ _ _ *)
    |solve_to_val          (* to_val e' = Some v *)
    |iIntros (l) H         (* new goal *)].
245

Dan Frumin's avatar
Dan Frumin committed
246
Tactic Notation "rel_load_l_atomic" := rel_apply_l bin_log_related_load_l.
247

248
Lemma tac_rel_load_l_simp `{logrelG Σ} Δ1 Δ2 E1 i1 l v K' Γ e t Δ' τ :
Dan Frumin's avatar
Dan Frumin committed
249 250 251
  e = fill K' (Load (Loc l)) 
  IntoLaterNEnvs 1 Δ1 Δ2 
  envs_lookup i1 Δ2 = Some (false, l ↦ᵢ v)%I 
252 253
  (Δ2  bin_log_related E1 E1 Δ' Γ (fill K' (of_val v)) t τ) 
  (Δ1  bin_log_related E1 E1 Δ' Γ e t τ).
Dan Frumin's avatar
Dan Frumin committed
254 255 256 257 258 259 260
Proof.
  intros ??? HΔ2.
  subst e.
  rewrite into_laterN_env_sound envs_lookup_split //; simpl.
  rewrite uPred.later_sep.
  rewrite HΔ2.
  apply uPred.wand_elim_l'.
261
  by rewrite -(bin_log_related_load_l' Δ' Γ E1).
Dan Frumin's avatar
Dan Frumin committed
262 263 264 265 266 267
Qed.

Tactic Notation "rel_load_l" :=
  iStartProof;
  eapply (tac_rel_alloc_l_simp);
    [tac_bind_helper (* e = fill K' .. *)
Dan Frumin's avatar
Dan Frumin committed
268 269
    |apply _  (* IntoLaterNenvs _ Δ1 Δ2 *)
    |iAssumptionCore || fail 3 "rel_load_l: cannot find ? ↦ᵢ ?"
Dan Frumin's avatar
Dan Frumin committed
270 271
    | (* new goal *)].

Dan Frumin's avatar
Dan Frumin committed
272
Tactic Notation "rel_store_l_atomic" := rel_apply_l bin_log_related_store_l.
273

274
Lemma tac_rel_store_l_simp `{logrelG Σ} Δ1 Δ2 i1 E1 l v e' v' K' Γ e t Δ' τ :
275 276 277 278
  e = fill K' (Store (Loc l) e') 
  to_val e' = Some v' 
  envs_lookup i1 Δ1 = Some (false, l ↦ᵢ v)%I 
  envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ᵢ v')) Δ1 = Some Δ2 
279 280
  (Δ2  bin_log_related E1 E1 Δ' Γ (fill K' (Lit Unit)) t τ) 
  (Δ1  bin_log_related E1 E1 Δ' Γ e t τ).
281 282 283 284 285 286
Proof.
  intros ?????.
  subst e.
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id.
  rewrite (uPred.later_intro (l ↦ᵢ v)%I).
287
  rewrite (bin_log_related_store_l' Δ' Γ E1). 2: eassumption.
288 289 290 291 292 293 294 295
  rewrite H4.
  apply uPred.wand_elim_l.
Qed.

Tactic Notation "rel_store_l" :=
  iStartProof;
  eapply (tac_rel_store_l_simp);
    [tac_bind_helper (* e = fill K' .. *)    
296
    |solve_to_val (* to_val e' = Some v' *)
297 298 299 300
    |iAssumptionCore || fail "rel_store_l: cannot find '? ↦ᵢ ?'"
    |env_cbv; reflexivity || fail "rel_store_l: this should not happen"
    | (* new goal *)].

Dan Frumin's avatar
Dan Frumin committed
301
Tactic Notation "rel_cas_l_atomic" := rel_apply_l bin_log_related_cas_l.
302 303 304

(********************************)

305
Lemma tac_rel_fork_r `{logrelG Σ} Δ1 E1 E2  t' K' Γ e t Δ' τ :
306 307 308
  nclose specN  E1 
  t = fill K' (Fork t') 
  Closed  t' 
309 310
  (Δ1   i, i  t' - bin_log_related E1 E2 Δ' Γ e (fill K' (Lit Unit)) τ) 
  (Δ1  bin_log_related E1 E2 Δ' Γ e t τ).
311 312 313
Proof.
  intros ????.
  subst t.
314
  rewrite -(bin_log_related_fork_r Δ' Γ E1 E2); eassumption.
315 316 317 318 319 320 321 322 323 324
Qed.

Tactic Notation "rel_fork_r" "as" ident(i) constr(H) :=
  iStartProof;
  eapply (tac_rel_fork_r);
    [solve_ndisj || fail "rel_fork_r: cannot prove 'nclose specN ⊆ ?'"
    |tac_bind_helper || fail "rel_fork_r: cannot find 'alloc'"
    |solve_closed
    |simpl; iIntros (i) H (* new goal *)].

325
Lemma tac_rel_store_r `{logrelG Σ} Δ1 Δ2 E1 E2 i1 l t' v' K' Γ e t Δ' τ v :
326 327 328 329 330
  nclose specN  E1 
  t = fill K' (Store (Loc l) t') 
  to_val t' = Some v' 
  envs_lookup i1 Δ1 = Some (false, l ↦ₛ v)%I 
  envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v')) Δ1 = Some Δ2 
331 332
  (Δ2  bin_log_related E1 E2 Δ' Γ e (fill K' (Lit Unit)) τ) 
  (Δ1  bin_log_related E1 E2 Δ' Γ e t τ).
333 334 335 336 337
Proof.
  intros ??????.
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id.
  subst t.
338
  rewrite (bin_log_related_store_r Δ' Γ E1 E2); [ | eassumption | eassumption ].
339 340 341 342 343 344 345 346 347
  rewrite H5. 
  apply uPred.wand_elim_l.
Qed.

Tactic Notation "rel_store_r" :=
  iStartProof;
  eapply (tac_rel_store_r);
    [solve_ndisj || fail "rel_store_r: cannot prove 'nclose specN ⊆ ?'"
    |tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
348
    |solve_to_val (* to_val e' = Some v *)
349 350 351 352
    |iAssumptionCore || fail "rel_store_l: cannot find ? ↦ₛ ?" 
    |env_cbv; reflexivity || fail "rel_store_r: this should not happen"
    |(* new goal *)].

353
Lemma tac_rel_alloc_r `{logrelG Σ} Δ1 E1 E2  t' v' K' Γ e t Δ' τ :
354 355 356
  nclose specN  E1 
  t = fill K' (Alloc t') 
  to_val t' = Some v' 
357 358
  (Δ1   l, l ↦ₛ v' - bin_log_related E1 E2 Δ' Γ e (fill K' (Loc l)) τ) 
  (Δ1  bin_log_related E1 E2 Δ' Γ e t τ).
359 360 361
Proof.
  intros ????.
  subst t.
362
  rewrite -(bin_log_related_alloc_r Δ' Γ E1 E2); eassumption.
363 364 365 366 367 368 369
Qed.

Tactic Notation "rel_alloc_r" "as" ident(l) constr(H) :=
  iStartProof;
  eapply (tac_rel_alloc_r);
    [solve_ndisj || fail "rel_alloc_r: cannot prove 'nclose specN ⊆ ?'"
    |tac_bind_helper || fail "rel_alloc_r: cannot find 'alloc'"
370
    |solve_to_val (* to_val t' = Some v' *)
371 372 373 374 375 376 377
    |simpl; iIntros (l) H (* new goal *)].

Tactic Notation "rel_alloc_r" :=
  let l := fresh in
  let H := iFresh "H" in
  rel_alloc_r as l H.

378
Lemma tac_rel_load_r `{logrelG Σ} Δ1 Δ2 E1 E2 i1 l K' Γ e t Δ' τ v :
379 380 381 382 383
  nclose specN  E1 
  t = fill K' (Load (Loc l)) 
  envs_lookup i1 Δ1 = Some (false, l ↦ₛ v)%I 
  envs_simple_replace i1 false 
    (Esnoc Enil i1 (l ↦ₛ v)%I) Δ1 = Some Δ2 
384 385
  (Δ2  bin_log_related E1 E2 Δ' Γ e (fill K' (of_val v)) τ) 
  (Δ1  bin_log_related E1 E2 Δ' Γ e t τ).
386 387 388 389 390
Proof.
  intros ?????.
  rewrite (envs_simple_replace_sound Δ1 Δ2 i1) //; simpl. 
  rewrite right_id.
  subst t.
391
  rewrite {1}(bin_log_related_load_r Δ' Γ E1 E2); [ | eassumption ].
392 393 394 395 396 397 398 399 400
  rewrite H4.
  apply uPred.wand_elim_l.
Qed.

Tactic Notation "rel_load_r" :=
  iStartProof;
  eapply (tac_rel_load_r);
    [solve_ndisj || fail "rel_load_r: cannot prove 'nclose specN ⊆ ?'"
    |tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
Dan Frumin's avatar
Dan Frumin committed
401
    |iAssumptionCore || fail "rel_load_r: cannot find ? ↦ₛ ?" 
402 403 404
    |env_cbv; reflexivity || fail "rel_load_r: this should not happen"
    |simpl (* new goal *)].

405
Lemma tac_rel_cas_fail_r `{logrelG Σ} Δ1 Δ2 E1 E2 i1 l K' Γ e t e1 e2 v1 v2 Δ' τ v :
406 407 408 409 410 411 412 413
  nclose specN  E1 
  t = fill K' (CAS (Loc l) e1 e2) 
  to_val e1 = Some v1 
  to_val e2 = Some v2 
  envs_lookup i1 Δ1 = Some (false, l ↦ₛ v)%I 
  v  v1 
  envs_simple_replace i1 false 
    (Esnoc Enil i1 (l ↦ₛ v)%I) Δ1 = Some Δ2 
414 415
  (Δ2  bin_log_related E1 E2 Δ' Γ e (fill K' (# false)) τ) 
  (Δ1  bin_log_related E1 E2 Δ' Γ e t τ).
416 417 418 419 420
Proof.
  intros ????????.
  rewrite (envs_simple_replace_sound Δ1 Δ2 i1) //; simpl. 
  rewrite right_id.
  subst t.
421
  rewrite {1}(bin_log_related_cas_fail_r Δ' Γ E1 E2 _ l e1 e2 v1 v2 v); eauto.
422 423 424 425 426 427 428 429 430
  rewrite H7.
  apply uPred.wand_elim_l.
Qed.

Tactic Notation "rel_cas_fail_r" :=
  iStartProof;
  eapply (tac_rel_cas_fail_r);
    [solve_ndisj || fail "rel_cas_fail_r: cannot prove 'nclose specN ⊆ ?'"
    |tac_bind_helper || fail "rel_cas_fail_r: cannot find 'CAS ..'"
431 432
    |solve_to_val
    |solve_to_val
433 434 435 436 437 438
    |iAssumptionCore || fail "rel_cas_fail_l: cannot find ? ↦ₛ ?" 
    |try fast_done (* v  v1 *)
    |env_cbv; reflexivity || fail "rel_load_r: this should not happen"
    |(* new goal *)].


439
Lemma tac_rel_cas_suc_r `{logrelG Σ} Δ1 Δ2 E1 E2 i1 l K' Γ e t e1 e2 v1 v2 Δ' τ v :
440 441 442 443 444 445 446 447
  nclose specN  E1 
  t = fill K' (CAS (Loc l) e1 e2) 
  to_val e1 = Some v1 
  to_val e2 = Some v2 
  envs_lookup i1 Δ1 = Some (false, l ↦ₛ v)%I 
  v = v1 
  envs_simple_replace i1 false 
    (Esnoc Enil i1 (l ↦ₛ v2)%I) Δ1 = Some Δ2 
448 449
  (Δ2  bin_log_related E1 E2 Δ' Γ e (fill K' (# true)) τ) 
  (Δ1  bin_log_related E1 E2 Δ' Γ e t τ).
450 451 452 453 454
Proof.
  intros ????????.
  rewrite (envs_simple_replace_sound Δ1 Δ2 i1) //; simpl. 
  rewrite right_id.
  subst t.
455
  rewrite {1}(bin_log_related_cas_suc_r Δ' Γ E1 E2 _ l e1 e2 v1 v2 v); eauto.
456 457 458 459 460 461 462 463 464
  rewrite H7.
  apply uPred.wand_elim_l.
Qed.

Tactic Notation "rel_cas_suc_r" :=
  iStartProof;
  eapply (tac_rel_cas_suc_r);
    [solve_ndisj || fail "rel_cas_suc_r: cannot prove 'nclose specN ⊆ ?'"
    |tac_bind_helper || fail "rel_cas_suc_r: cannot find 'CAS ..'"
465 466
    |solve_to_val
    |solve_to_val
467 468 469 470 471
    |iAssumptionCore || fail "rel_cas_suc_l: cannot find ? ↦ₛ ?" 
    |try fast_done (* v = v1 *)
    |env_cbv; reflexivity || fail "rel_load_r: this should not happen"
    |(* new goal *)].

472
Section test.
473
  From iris_logrel.F_mu_ref_conc Require Import reflection.
474
  Context `{logrelG Σ}.
475
  
476 477 478 479 480 481 482
  Definition choiceN : namespace := nroot .@ "choice".

  Definition choice_inv y y' : iProp Σ :=
    ( f, y ↦ᵢ (#v f)  y' ↦ₛ (#v f))%I.

  Definition storeFalse : val := λ: "y", "y" <- # false.

Dan Frumin's avatar
Dan Frumin committed
483
  Lemma test_store Γ Δ y y':
484
    inv choiceN (choice_inv y y')
Dan Frumin's avatar
Dan Frumin committed
485
    - {,;Δ;Γ}  (storeFalse (Fst (#y, 3))) log (storeFalse #y') : TUnit.
486 487 488
  Proof.
    iIntros "#Hinv".
    unfold storeFalse. unlock.
489
    rel_fst_l.
490 491 492
    rel_rec_l.
    rel_rec_r.

Dan Frumin's avatar
Dan Frumin committed
493 494 495 496 497
    rel_apply_l bin_log_related_store_l.
    iInv choiceN as (f) ">[Hy Hy']" "Hcl".
    iExists _. iFrame "Hy".
    iModIntro. iNext. iIntros "Hy".
    rel_store_r. simpl.
498 499 500 501

    iMod ("Hcl" with "[Hy Hy']").
    { iNext. iExists _. iFrame. }

Dan Frumin's avatar
Dan Frumin committed
502 503

    rel_vals; eauto.
504 505 506
  Qed.

End test.