rel_tactics.v 24.4 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.

10
Lemma tac_rel_bind_l `{logrelG Σ} e' K Δ E1 E2 Γ e t Δ' τ :
11
  e = fill K e' 
12 13
  (Δ  bin_log_related E1 E2 Δ' Γ (fill K e') t τ) 
  (Δ  bin_log_related E1 E2 Δ' Γ e t τ).
14
Proof. intros. subst. eauto. Qed.
15

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

22
Ltac tac_bind_helper :=
23 24 25 26 27 28 29 30 31 32 33 34
  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.

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

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

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

Tactic Notation "rel_bind_r" open_constr(efoc) :=
  iStartProof;
  eapply (tac_rel_bind_r efoc);
  [ tac_bind_helper
  | (* new goal *) 
  ].

67
Tactic Notation "rel_vals" :=
Dan Frumin's avatar
Dan Frumin committed
68
  iStartProof;
69
  iApply bin_log_related_val; [ try solve_to_val | try solve_to_val | ].
Dan Frumin's avatar
Dan Frumin committed
70

71 72 73 74 75
(** Pure reductions *)
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
76 77
  Closed  e1 
  Closed  e2 
78 79 80
  ((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
81
Proof.
82 83 84 85 86 87 88 89 90 91 92
  intros Hfill Hpure Hϕ ?? Hb Hp. subst.
  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
93 94
Qed.

95
Tactic Notation "rel_pure_l" open_constr(ef) :=
Dan Frumin's avatar
Dan Frumin committed
96
  iStartProof;
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
  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 *)
      |try (simpl_subst/=; solve_closed)   (* Closed  e2 *) (* we might get subst' here *)
      |first [left; split; reflexivity | right; reflexivity] (* E1 = E2? *)
      |try iNext; simpl_subst/= (* new goal *)])
  || fail "rel_pure_l: cannot find the reduct".

Tactic Notation "rel_rec_l" := rel_pure_l (App _ _).
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
129 130
  Closed  e1 
  Closed  e2 
131 132 133
  nclose specN  E1 
  (Δ'  bin_log_related E1 E2 Δ Γ t (fill K e2) τ) 
  (Δ'  bin_log_related E1 E2 Δ Γ t e τ).
134
Proof.
135 136 137 138 139 140 141 142 143
  intros Hfill Hpure Hϕ ??? Hp. subst.
  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. }
144 145
Qed.

146
Tactic Notation "rel_pure_r" open_constr(ef) :=
147
  iStartProof;
148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176
  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 *)
      |try (simpl_subst/=; solve_closed)   (* Closed  e2 *) (* we might get subst' here *)
      |solve_ndisj                 (* specN  E1 *)
      |try iNext; simpl_subst/=    (* new goal *)])
  || fail "rel_pure_r: cannot find the reduct".

Tactic Notation "rel_rec_r" := rel_pure_r (App _ _).
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 *)
177

178
Lemma tac_rel_fork_l `{logrelG Σ} Δ1 E1 E2 e' K' Γ e t Δ' τ :
179 180
  e = fill K' (Fork e') 
  Closed  e' 
181 182
  (Δ1  |={E1,E2}=>  WP e' {{ _ , True }}  bin_log_related E2 E1 Δ' Γ (fill K' (Lit Unit)) t τ) 
  (Δ1  bin_log_related E1 E1 Δ' Γ e t τ).
183 184 185
Proof.
  intros ???.
  subst e.
186
  rewrite -(bin_log_related_fork_l Δ' Γ E1 E2); eassumption.
187 188 189 190 191 192 193 194 195
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 *) ].

196
Lemma tac_rel_alloc_l `{logrelG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P e' v' K' Γ e t Δ' τ :
197 198 199 200 201 202 203 204 205
  nclose N  E1 
  envs_lookup i1 Δ1 = Some (p, inv N P) 
  E2 = E1  N 
  e = fill K' (Alloc e') 
  to_val e' = Some v' 
  envs_lookup nam Δ1 = None 
  envs_lookup nam_cl Δ1 = None 
  nam_cl  nam 
  Δ2 = envs_snoc (envs_snoc Δ1 false nam ( P)%I) false nam_cl ( P ={E1  N,E1}= True)%I 
Dan Frumin's avatar
Dan Frumin committed
206
  (Δ2  |={E2}=>   l,
207 208
     (l ↦ᵢ v' - bin_log_related E2 E1 Δ' Γ (fill K' (Loc l)) t τ)) 
  (Δ1  bin_log_related E1 E1 Δ' Γ e t τ).
209 210 211 212 213 214 215
Proof.
  intros ??????????.
  rewrite -(idemp uPred_and Δ1).
  rewrite {1}envs_lookup_sound'. 2: eassumption.
  rewrite uPred.sep_elim_l uPred.always_and_sep_l.
  rewrite inv_open. 2: eassumption.
  subst e.
216
  rewrite -(bin_log_related_alloc_l Δ' Γ E1 E2). 2: eassumption.
217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239
  rewrite fupd_frame_r.
  rewrite -(fupd_trans E1 E2 E2).
  subst E2.
  apply fupd_mono.  
  rewrite -H9.
  subst Δ2.
  rewrite (envs_snoc_sound Δ1 false nam (P)) /=. 2: eassumption.
  rewrite comm.
  rewrite assoc.
  rewrite uPred.wand_elim_l.
  rewrite (envs_snoc_sound (envs_snoc Δ1 false nam ( P)) false nam_cl ( P ={E1  N,E1}= True)) //;
          last first.
  { rewrite (envs_lookup_snoc_ne Δ1); eassumption. }
  apply uPred.wand_elim_l.
Qed.

Tactic Notation "rel_alloc_l" "under" constr(N) "as" constr(nam) constr(nam_cl) :=
  iStartProof;
  eapply (tac_rel_alloc_l nam nam_cl);
    [solve_ndisj || fail "rel_alloc_l: cannot prove 'nclose " N " ⊆ ?'"
    |iAssumptionCore || fail "rel_alloc_l: cannot find inv " N " ?" 
    |try fast_done (* E2 = E1 \ N *)
    |tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
240
    |solve_to_val (* to_val e' = Some v *)
241 242 243 244 245 246
    |try fast_done (* nam fresh *)
    |try fast_done (* nam_cl fresh *)
    |eauto (* nam =/= nam_cl *)
    |env_cbv; reflexivity || fail "rel_alloc_l: this should not happen"
    |(* new goal *)].

247
Lemma tac_rel_alloc_l_simp `{logrelG Σ} Δ1 Δ2 E1 e' v' K' Γ e t Δ' τ :
248
  e = fill K' (Alloc e') 
Dan Frumin's avatar
Dan Frumin committed
249
  IntoLaterNEnvs 1 Δ1 Δ2 
250
  to_val e' = Some v' 
Dan Frumin's avatar
Dan Frumin committed
251
  (Δ2   l,
252 253
     (l ↦ᵢ v' - bin_log_related E1 E1 Δ' Γ (fill K' (Loc l)) t τ)) 
  (Δ1  bin_log_related E1 E1 Δ' Γ e t τ).
254 255 256
Proof.
  intros ???.
  subst e.
Dan Frumin's avatar
Dan Frumin committed
257
  rewrite into_laterN_env_sound /=.
258
  rewrite -(bin_log_related_alloc_l' Δ' Γ E1); eauto.
Dan Frumin's avatar
Dan Frumin committed
259
  apply uPred.later_mono.
260 261 262 263 264 265
Qed.

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

270
Lemma tac_rel_load_l `{logrelG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l K' Γ e t Δ' τ :
271 272 273 274 275 276 277 278 279
  nclose N  E1 
  envs_lookup i1 Δ1 = Some (p, inv N P) 
  E2 = E1  N 
  e = fill K' (Load (Loc l)) 
  envs_lookup nam Δ1 = None 
  envs_lookup nam_cl Δ1 = None 
  nam_cl  nam 
  Δ2 = envs_snoc (envs_snoc Δ1 false nam ( P)%I) false nam_cl ( P ={E1  N,E1}= True)%I 
  (Δ2  |={E2}=>  v,  (l ↦ᵢ v) 
280 281
      (l ↦ᵢ v - bin_log_related E2 E1 Δ' Γ (fill K' (of_val v)) t τ)) 
  (Δ1  bin_log_related E1 E1 Δ' Γ e t τ).
282 283 284 285 286 287 288
Proof.
  intros ?????????.
  rewrite -(idemp uPred_and Δ1).
  rewrite {1}envs_lookup_sound'. 2: eassumption.
  rewrite uPred.sep_elim_l uPred.always_and_sep_l.
  rewrite inv_open. 2: eassumption.
  subst e.
289
  rewrite -(bin_log_related_load_l Δ' Γ E1 E2).
290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319
  rewrite fupd_frame_r.
  rewrite -(fupd_trans E1 E2 E2).
  subst E2.
  apply fupd_mono.  
  rewrite -H8.
  subst Δ2.
  rewrite (envs_snoc_sound Δ1 false nam (P)) /=. 2: eassumption.
  rewrite comm.
  rewrite assoc.
  rewrite uPred.wand_elim_l.
  rewrite (envs_snoc_sound (envs_snoc Δ1 false nam ( P)) false nam_cl ( P ={E1  N,E1}= True)) //;
          last first.
  { rewrite (envs_lookup_snoc_ne Δ1); eassumption. }
  rewrite uPred.wand_elim_l.
  done.
Qed.

Tactic Notation "rel_load_l" "under" constr(N) "as" constr(nam) constr(nam_cl) :=
  iStartProof;
  eapply (tac_rel_load_l nam nam_cl);
    [solve_ndisj || fail "rel_load_l: cannot prove 'nclose " N " ⊆ ?'"
    |iAssumptionCore || fail "rel_load_l: cannot find inv " N " ?" 
    |try fast_done (* E2 = E1 \ N *)
    |tac_bind_helper (* e = fill K' .. *)
    |try fast_done (* nam fresh *)
    |try fast_done (* nam_cl fresh *)
    |eauto (* nam =/= nam_cl *)
    |env_cbv; reflexivity || fail "rel_load_l: this should not happen"
    |(* new goal *)].

320
Lemma tac_rel_load_l_simp `{logrelG Σ} Δ1 Δ2 E1 i1 l v K' Γ e t Δ' τ :
Dan Frumin's avatar
Dan Frumin committed
321 322 323
  e = fill K' (Load (Loc l)) 
  IntoLaterNEnvs 1 Δ1 Δ2 
  envs_lookup i1 Δ2 = Some (false, l ↦ᵢ v)%I 
324 325
  (Δ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
326 327 328 329 330 331 332
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'.
333
  by rewrite -(bin_log_related_load_l' Δ' Γ E1).
Dan Frumin's avatar
Dan Frumin committed
334 335 336 337 338 339
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
340 341
    |apply _  (* IntoLaterNenvs _ Δ1 Δ2 *)
    |iAssumptionCore || fail 3 "rel_load_l: cannot find ? ↦ᵢ ?"
Dan Frumin's avatar
Dan Frumin committed
342 343
    | (* new goal *)].

344
Lemma tac_rel_store_l `{logrelG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l e' v' K' Γ e t Δ' τ :
345 346 347 348 349 350 351 352 353 354
  nclose N  E1 
  envs_lookup i1 Δ1 = Some (p, inv N P) 
  E2 = E1  N 
  e = fill K' (Store (Loc l) e') 
  to_val e' = Some v' 
  envs_lookup nam Δ1 = None 
  envs_lookup nam_cl Δ1 = None 
  nam_cl  nam 
  Δ2 = envs_snoc (envs_snoc Δ1 false nam ( P)%I) false nam_cl ( P ={E1  N,E1}= True)%I 
  (Δ2  |={E2}=>  v,  (l ↦ᵢ v) 
355
     (l ↦ᵢ v' - bin_log_related E2 E1 Δ' Γ (fill K' (Lit Unit)) t τ)) 
356
  (Δ1  bin_log_related E1 E1 Δ' Γ e t τ).
357 358 359 360 361 362 363
Proof.
  intros ??????????.
  rewrite -(idemp uPred_and Δ1).
  rewrite {1}envs_lookup_sound'. 2: eassumption.
  rewrite uPred.sep_elim_l uPred.always_and_sep_l.
  rewrite inv_open. 2: eassumption.
  subst e.
364
  rewrite -(bin_log_related_store_l Δ' Γ E1 E2). 2: eassumption.
365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388
  rewrite fupd_frame_r.
  rewrite -(fupd_trans E1 E2 E2).
  subst E2.
  apply fupd_mono.  
  rewrite -H9.
  subst Δ2.
  rewrite (envs_snoc_sound Δ1 false nam (P)) /=. 2: eassumption.
  rewrite comm.
  rewrite assoc.
  rewrite uPred.wand_elim_l.
  rewrite (envs_snoc_sound (envs_snoc Δ1 false nam ( P)) false nam_cl ( P ={E1  N,E1}= True)) //;
          last first.
  { rewrite (envs_lookup_snoc_ne Δ1); eassumption. }
  rewrite uPred.wand_elim_l.
  done.
Qed.

Tactic Notation "rel_store_l" "under" constr(N) "as" constr(nam) constr(nam_cl) :=
  iStartProof;
  eapply (tac_rel_store_l nam nam_cl);
    [solve_ndisj || fail "rel_store_l: cannot prove 'nclose " N " ⊆ ?'"
    |iAssumptionCore || fail "rel_store_l: cannot find inv " N " ?" 
    |try fast_done (* E2 = E1 \ N *)
    |tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
389
    |solve_to_val (* to_val e' = Some v *)
390 391 392 393 394 395
    |try fast_done (* nam fresh *)
    |try fast_done (* nam_cl fresh *)
    |eauto (* nam =/= nam_cl *)
    |env_cbv; reflexivity || fail "rel_store_l: this should not happen"
    |(* new goal *)].

396

397
Lemma tac_rel_store_l_simp `{logrelG Σ} Δ1 Δ2 i1 E1 l v e' v' K' Γ e t Δ' τ :
398 399 400 401
  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 
402 403
  (Δ2  bin_log_related E1 E1 Δ' Γ (fill K' (Lit Unit)) t τ) 
  (Δ1  bin_log_related E1 E1 Δ' Γ e t τ).
404 405 406 407 408 409
Proof.
  intros ?????.
  subst e.
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id.
  rewrite (uPred.later_intro (l ↦ᵢ v)%I).
410
  rewrite (bin_log_related_store_l' Δ' Γ E1). 2: eassumption.
411 412 413 414 415 416 417 418
  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' .. *)    
419
    |solve_to_val (* to_val e' = Some v' *)
420 421 422 423
    |iAssumptionCore || fail "rel_store_l: cannot find '? ↦ᵢ ?'"
    |env_cbv; reflexivity || fail "rel_store_l: this should not happen"
    | (* new goal *)].

424
Lemma tac_rel_cas_l `{logrelG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l e1 e2 v1 v2 K' Γ e t Δ' τ :
425 426 427 428 429 430 431 432 433 434 435
  nclose N  E1 
  envs_lookup i1 Δ1 = Some (p, inv N P) 
  E2 = E1  N 
  e = fill K' (CAS (Loc l) e1 e2) 
  to_val e1 = Some v1 
  to_val e2 = Some v2 
  envs_lookup nam Δ1 = None 
  envs_lookup nam_cl Δ1 = None 
  nam_cl  nam 
  Δ2 = envs_snoc (envs_snoc Δ1 false nam ( P)%I) false nam_cl ( P ={E1  N,E1}= True)%I 
  (Δ2  |={E2}=>  v,  (l ↦ᵢ v) 
436 437 438
     ((v  v1   (l ↦ᵢ v  - {E2,E1;Δ';Γ}  fill K' (# false) log t : τ)) 
      (v = v1   (l ↦ᵢ v2 - {E2,E1;Δ';Γ}  fill K' (# true) log t : τ)))) 
  (Δ1  bin_log_related E1 E1 Δ' Γ e t τ).
439 440 441 442 443 444 445
Proof.
  intros ???????????.
  rewrite -(idemp uPred_and Δ1).
  rewrite {1}envs_lookup_sound'. 2: eassumption.
  rewrite uPred.sep_elim_l uPred.always_and_sep_l.
  rewrite inv_open. 2: eassumption.
  subst e.
446
  rewrite -(bin_log_related_cas_l Δ' Γ E1 E2); try eassumption.
447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476
  rewrite fupd_frame_r.
  rewrite -(fupd_trans E1 E2 E2).
  subst E2.
  apply fupd_mono.  
  subst Δ2.
  rewrite (envs_snoc_sound Δ1 false nam (P)) /=. 2: eassumption.
  rewrite comm.
  rewrite assoc.
  rewrite uPred.wand_elim_l.
  rewrite (envs_snoc_sound (envs_snoc Δ1 false nam ( P)) false nam_cl ( P ={E1  N,E1}= True)) //;
          last first.
  { rewrite (envs_lookup_snoc_ne Δ1); eassumption. }
  rewrite H10.
  rewrite uPred.wand_elim_l.
  apply fupd_mono.
  iDestruct 1 as (v) "[Hl Hv]". iExists v. iFrame "Hl".
  iDestruct "Hv" as "[[% Hv] | [% Hv]]"; subst.
  - iSplitL; last first; iIntros "%". by exfalso.
    done.
  - iSplitR; iIntros "%". by exfalso.
    done.
Qed.

Tactic Notation "rel_cas_l" "under" constr(N) "as" constr(nam) constr(nam_cl) :=
  iStartProof;
  eapply (tac_rel_cas_l nam nam_cl);
    [solve_ndisj || fail "rel_store_l: cannot prove 'nclose " N " ⊆ ?'"
    |iAssumptionCore || fail "rel_store_l: cannot find inv " N " ?" 
    |try fast_done (* E2 = E1 \ N *)
    |tac_bind_helper (* e = fill K' ... *)
477 478
    |solve_to_val (* to_val e1 = Some .. *)
    |solve_to_val (* to_val e2 = Some .. *)
479 480 481 482 483 484 485 486 487
    |try fast_done (* nam fresh *)
    |try fast_done (* nam_cl fresh *)
    |eauto (* nam =/= nam_cl *)
    |env_cbv; reflexivity || fail "rel_store_l: this should not happen"
    |(* new goal *)].


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

488
Lemma tac_rel_fork_r `{logrelG Σ} Δ1 E1 E2  t' K' Γ e t Δ' τ :
489 490 491
  nclose specN  E1 
  t = fill K' (Fork t') 
  Closed  t' 
492 493
  (Δ1   i, i  t' - bin_log_related E1 E2 Δ' Γ e (fill K' (Lit Unit)) τ) 
  (Δ1  bin_log_related E1 E2 Δ' Γ e t τ).
494 495 496
Proof.
  intros ????.
  subst t.
497
  rewrite -(bin_log_related_fork_r Δ' Γ E1 E2); eassumption.
498 499 500 501 502 503 504 505 506 507
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 *)].

508
Lemma tac_rel_store_r `{logrelG Σ} Δ1 Δ2 E1 E2 i1 l t' v' K' Γ e t Δ' τ v :
509 510 511 512 513
  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 
514 515
  (Δ2  bin_log_related E1 E2 Δ' Γ e (fill K' (Lit Unit)) τ) 
  (Δ1  bin_log_related E1 E2 Δ' Γ e t τ).
516 517 518 519 520
Proof.
  intros ??????.
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id.
  subst t.
521
  rewrite (bin_log_related_store_r Δ' Γ E1 E2); [ | eassumption | eassumption ].
522 523 524 525 526 527 528 529 530
  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') *)
531
    |solve_to_val (* to_val e' = Some v *)
532 533 534 535
    |iAssumptionCore || fail "rel_store_l: cannot find ? ↦ₛ ?" 
    |env_cbv; reflexivity || fail "rel_store_r: this should not happen"
    |(* new goal *)].

536
Lemma tac_rel_alloc_r `{logrelG Σ} Δ1 E1 E2  t' v' K' Γ e t Δ' τ :
537 538 539
  nclose specN  E1 
  t = fill K' (Alloc t') 
  to_val t' = Some v' 
540 541
  (Δ1   l, l ↦ₛ v' - bin_log_related E1 E2 Δ' Γ e (fill K' (Loc l)) τ) 
  (Δ1  bin_log_related E1 E2 Δ' Γ e t τ).
542 543 544
Proof.
  intros ????.
  subst t.
545
  rewrite -(bin_log_related_alloc_r Δ' Γ E1 E2); eassumption.
546 547 548 549 550 551 552
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'"
553
    |solve_to_val (* to_val t' = Some v' *)
554 555 556 557 558 559 560
    |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.

561
Lemma tac_rel_load_r `{logrelG Σ} Δ1 Δ2 E1 E2 i1 l K' Γ e t Δ' τ v :
562 563 564 565 566
  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 
567 568
  (Δ2  bin_log_related E1 E2 Δ' Γ e (fill K' (of_val v)) τ) 
  (Δ1  bin_log_related E1 E2 Δ' Γ e t τ).
569 570 571 572 573
Proof.
  intros ?????.
  rewrite (envs_simple_replace_sound Δ1 Δ2 i1) //; simpl. 
  rewrite right_id.
  subst t.
574
  rewrite {1}(bin_log_related_load_r Δ' Γ E1 E2); [ | eassumption ].
575 576 577 578 579 580 581 582 583
  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
584
    |iAssumptionCore || fail "rel_load_r: cannot find ? ↦ₛ ?" 
585 586 587
    |env_cbv; reflexivity || fail "rel_load_r: this should not happen"
    |simpl (* new goal *)].

588
Lemma tac_rel_cas_fail_r `{logrelG Σ} Δ1 Δ2 E1 E2 i1 l K' Γ e t e1 e2 v1 v2 Δ' τ v :
589 590 591 592 593 594 595 596
  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 
597 598
  (Δ2  bin_log_related E1 E2 Δ' Γ e (fill K' (# false)) τ) 
  (Δ1  bin_log_related E1 E2 Δ' Γ e t τ).
599 600 601 602 603
Proof.
  intros ????????.
  rewrite (envs_simple_replace_sound Δ1 Δ2 i1) //; simpl. 
  rewrite right_id.
  subst t.
604
  rewrite {1}(bin_log_related_cas_fail_r Δ' Γ E1 E2 _ l e1 e2 v1 v2 v); eauto.
605 606 607 608 609 610 611 612 613
  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 ..'"
614 615
    |solve_to_val
    |solve_to_val
616 617 618 619 620 621
    |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 *)].


622
Lemma tac_rel_cas_suc_r `{logrelG Σ} Δ1 Δ2 E1 E2 i1 l K' Γ e t e1 e2 v1 v2 Δ' τ v :
623 624 625 626 627 628 629 630
  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 
631 632
  (Δ2  bin_log_related E1 E2 Δ' Γ e (fill K' (# true)) τ) 
  (Δ1  bin_log_related E1 E2 Δ' Γ e t τ).
633 634 635 636 637
Proof.
  intros ????????.
  rewrite (envs_simple_replace_sound Δ1 Δ2 i1) //; simpl. 
  rewrite right_id.
  subst t.
638
  rewrite {1}(bin_log_related_cas_suc_r Δ' Γ E1 E2 _ l e1 e2 v1 v2 v); eauto.
639 640 641 642 643 644 645 646 647
  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 ..'"
648 649
    |solve_to_val
    |solve_to_val
650 651 652 653 654
    |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 *)].

655
Section test.
656
  From iris_logrel.F_mu_ref_conc Require Import reflection.
657
  Context `{logrelG Σ}.
658
  
659 660 661 662 663 664 665
  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.

666
  Lemma test_store Γ y y':
667
    inv choiceN (choice_inv y y')
668
    - Γ  (storeFalse (Fst (#y, 3))) log (storeFalse #y') : TUnit.
669 670 671
  Proof.
    iIntros "#Hinv".
    unfold storeFalse. unlock.
672
    rel_fst_l.
673 674 675 676 677
    rel_rec_l.
    rel_rec_r.

    rel_store_l under choiceN as "Hs" "Hcl".
      iDestruct "Hs" as (f) "[>Hy >Hy']". iExists _. iFrame "Hy".
678
      iModIntro. iNext. iIntros "Hy".
679 680 681 682 683 684 685 686 687
      rel_store_r. simpl.

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

    iApply bin_log_related_val; eauto.
  Qed.

End test.