or.v 12.8 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
(* (In)equational theory of erratic choice.

   We can simulate (binary) non-determinism with concurrency. In this
   file we derive the algebraic laws for parallel "or"/demonic choice
   combinator. In particular, we show the following ( stands for
   contextual refinement and  stands for contextual equivalence):

   - v or v  v ()           idempotency
   - v1 or v2  v2 or v1     commutativity
   - v or (λ_, )  v ()      is a unit
   - v1 or (λ_, v2 or v3)     associativity
      (λ_, v1 or v2) or v3
   - v1 ()  v1 or v2        choice on the RHS
Dan Frumin's avatar
Dan Frumin committed
14 15

    where every v_i is well-typed Unit -> Unit
16
*)
17
From iris.proofmode Require Import tactics.
18
From iris_logrel Require Export logrel examples.bot.
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33

Definition or : val := λ: "e1" "e2",
  let: "x" := ref #0 in
  Fork ("x" <- #1);;
  if: !"x" = #0
  then "e1" #()
  else "e2" #().

Lemma or_type Γ :
  typed Γ or
        (TArrow (TArrow TUnit TUnit) (TArrow (TArrow TUnit TUnit)
            TUnit)).
Proof. solve_typed. Qed.
Hint Resolve or_type : typeable.

Dan Frumin's avatar
Dan Frumin committed
34
Section contents.
35 36
  Context `{logrelG Σ}.

37 38 39 40
  Lemma bin_log_related_or Δ Γ e1 e2 e1' e2' :
    {Δ;Γ}  e1 log e1' : TArrow TUnit TUnit -
    {Δ;Γ}  e2 log e2' : TArrow TUnit TUnit -
    {Δ;Γ}  or e1 e2 log or e1' e2' : TUnit.
41
  Proof.
42
    iIntros "He1 He2".
43 44
    iApply (bin_log_related_app with "[He1] He2").
    iApply (bin_log_related_app with "[] He1").
45
    iApply binary_fundamental; eauto with typeable.
46 47
  Qed.

48 49 50
  Lemma bin_log_or_choice_1_r_val Δ Γ (v1 v1' v2 : val) :
    {Δ;Γ}  v1 log v1' : TArrow TUnit TUnit -
    {Δ;Γ}  v1 #() log or v1' v2 : TUnit.
51
  Proof.
52
    iIntros "Hlog".
53 54 55 56 57
    unlock or. repeat rel_rec_r.
    rel_alloc_r as x "Hx".
    repeat rel_let_r.
    rel_fork_r as j "Hj". rel_seq_r.
    rel_load_r. repeat (rel_pure_r _).
58 59
    iApply (bin_log_related_app with "Hlog").
    iApply bin_log_related_unit.
60 61
  Qed.

62
  Lemma bin_log_or_choice_1_r_val_typed Δ Γ (v1 v2 : val) :
63
    Γ ⊢ₜ v1 : TArrow TUnit TUnit 
64
    {Δ;Γ}  v1 #() log or v1 v2 : TUnit.
65
  Proof.
66
    iIntros (?).
67
    iApply bin_log_or_choice_1_r_val; eauto.
68
    iApply binary_fundamental; eauto with typeable.
69 70
  Qed.

71 72 73
  Lemma bin_log_or_choice_1_r Δ Γ (e1 e1' : expr) (v2 : val) :
    {Δ;Γ}  e1 log e1' : TArrow TUnit TUnit -
    {Δ;Γ}  e1 #() log or e1' v2 : TUnit.
74
  Proof.
75
    iIntros "Hlog".
76
    rel_bind_l e1.
77 78
    rel_bind_r e1'.
    iApply (related_bind with "Hlog").
79
    iIntros ([f f']) "#Hf /=".
80 81 82
    iApply bin_log_or_choice_1_r_val; eauto.
    iApply (related_ret ).
    iApply interp_ret; eauto using to_of_val.
83 84
  Qed.

85
  Lemma bin_log_or_choice_1_r_body Δ Γ (e1 : expr) (v2 : val) :
86 87
    Closed  e1 
    Γ ⊢ₜ e1 : TUnit 
88
    {Δ;Γ}  e1 log or (λ: <>, e1) v2 : TUnit.
89
  Proof.
90
    iIntros (??).
91 92 93 94 95
    unlock or. repeat rel_rec_r.
    rel_alloc_r as x "Hx".
    repeat rel_let_r.
    rel_fork_r as j "Hj". rel_seq_r.
    rel_load_r. repeat (rel_pure_r _).
96
    iApply binary_fundamental; eauto with typeable.
97 98
  Qed.

99 100 101
  Definition or_inv x : iProp Σ :=
    (x ↦ᵢ #0  x ↦ᵢ #1)%I.
  Definition orN := nroot .@ "orN".
102
  Ltac close_inv := iNext; (iLeft + iRight); by iFrame.
103

104 105
  Lemma assign_safe x :
    inv orN (or_inv x)
106 107 108
      WP #x <- #1 {{ _, True }}.
  Proof.
    iIntros "#Hinv".
109
    iNext. iInv orN as ">[Hx | Hx]" "Hcl"; wp_store;
110
      (iMod ("Hcl" with "[-]"); first close_inv); eauto.
111 112
  Qed.

113 114 115 116
  Lemma bin_log_or_commute Δ Γ (v1 v1' v2 v2' : val) :
    {Δ;Γ}  v1 log v1' : TArrow TUnit TUnit -
    {Δ;Γ}  v2 log v2' : TArrow TUnit TUnit -
    {Δ;Γ}  or v2 v1 log or v1' v2' : TUnit.
117
  Proof.
118
    iIntros "Hv1 Hv2".
119
    unlock or; simpl. repeat rel_rec_r. repeat rel_rec_l.
120 121 122 123
    rel_alloc_l as x "Hx".
    rel_alloc_r as y "Hy".
    repeat rel_let_l. repeat rel_let_r.
    rel_fork_r as j "Hj". rel_seq_r.
124 125
    iMod (inv_alloc orN _ (or_inv x) with "[Hx]") as "#Hinv";
      first close_inv.
126 127 128 129
    rel_fork_l.
    iModIntro. iSplitR; [ by iApply assign_safe | ].
    rel_seq_l.
    rel_load_l_atomic.
130
    iInv orN as ">[Hx|Hx]" "Hcl";
131 132
      iExists _; iFrame; iModIntro; iNext; iIntros "Hx";
      rel_op_l; rel_if_l.
133 134
    + apply bin_log_related_spec_ctx; iDestruct 1 as (ρ1) "#Hρ1".
      (* TODO: tp tactics should be aware of spec_ctx *)
135 136 137
      tp_store j.
      rel_load_r.
      repeat (rel_pure_r _).
138
      iMod ("Hcl" with "[-Hv1 Hv2]"); first close_inv.
139 140
      iApply (bin_log_related_app with "Hv2").
      iApply bin_log_related_unit.
141 142
    + rel_load_r.
      repeat (rel_pure_r _).
143
      iMod ("Hcl" with "[-Hv1 Hv2]"); first close_inv.
144 145 146 147
      iApply (bin_log_related_app with "Hv1").
      iApply bin_log_related_unit.
  Qed.

148 149 150
  Lemma bin_log_or_idem_r Δ Γ (v v' : val) :
    {Δ;Γ}  v log v' : TArrow TUnit TUnit -
    {Δ;Γ}  v #() log or v' v' : TUnit.
151
  Proof.
152
    iIntros  "Hlog".
153
    by iApply bin_log_or_choice_1_r_val.
154 155
  Qed.

156
  Lemma bin_log_or_idem_r_body Δ Γ e :
157 158
    Closed  e 
    Γ ⊢ₜ e : TUnit 
159
    {Δ;Γ}  e log or (λ: <>, e) (λ: <>, e) : TUnit.
160
  Proof.
161 162
    iIntros (??).
    iPoseProof (bin_log_or_choice_1_r_body Δ _ e (λ: <>, e)) as "HZ"; eauto.
163 164 165
    unlock. eauto. (* TODO :( *)
  Qed.

166 167 168
  Lemma bin_log_or_idem_l Δ Γ (v v' : val) :
    {Δ;Γ}  v log v' : TArrow TUnit TUnit -
    {Δ;Γ}  or v v log v' #() : TUnit.
169
  Proof.
170
    iIntros  "Hlog".
171 172 173
    unlock or. repeat rel_rec_l.
    rel_alloc_l as x "Hx".
    repeat rel_let_l.
174
    iMod (inv_alloc orN _ (or_inv x)%I with "[Hx]") as "#Hinv".
175
    { close_inv. }
176 177 178 179
    rel_fork_l.
    iModIntro. iSplitR; [ by iApply assign_safe | ].
    rel_seq_l.
    rel_load_l_atomic.
180
    iInv orN as ">[Hx|Hx]" "Hcl";
181
      iExists _; iFrame; iModIntro; iNext; iIntros "Hx";
182
        rel_op_l; rel_if_l.
183
    + iMod ("Hcl" with "[-Hlog]"); first close_inv.
184 185
      iApply (bin_log_related_app with "Hlog").
      iApply bin_log_related_unit.
186
    + iMod ("Hcl" with "[-Hlog]"); first close_inv.
187 188
      iApply (bin_log_related_app with "Hlog").
      iApply bin_log_related_unit.
189 190
  Qed.

191 192 193
  Lemma bin_log_or_bot_l Δ Γ (v v' : val) :
    {Δ;Γ}  v log v' : TArrow TUnit TUnit -
    {Δ;Γ}  or v bot log v' #() : TUnit.
194
  Proof.
195
    iIntros "Hlog".
196 197 198
    unlock or. repeat rel_rec_l.
    rel_alloc_l as x "Hx".
    repeat rel_let_l.
199
    iMod (inv_alloc orN _ (or_inv x)%I with "[Hx]") as "#Hinv".
200
    { close_inv. }
201 202 203 204
    rel_fork_l.
    iModIntro. iSplitR; [ by iApply assign_safe | ].
    rel_seq_l.
    rel_load_l_atomic.
205
    iInv orN as ">[Hx|Hx]" "Hcl";
206 207
      iExists _; iFrame; iModIntro; iNext; iIntros "Hx";
      rel_op_l; rel_if_l.
208
    + iMod ("Hcl" with "[-Hlog]"); first close_inv.
209 210
      iApply (bin_log_related_app with "Hlog").
      iApply bin_log_related_unit.
211
    + iMod ("Hcl" with "[-Hlog]"); first close_inv.
Dan Frumin's avatar
Dan Frumin committed
212
      rel_apply_l bot_l.
213 214
  Qed.

215 216 217
  Lemma bin_log_or_bot_r Δ Γ (v v' : val) :
    {Δ;Γ}  v log v' : TArrow TUnit TUnit -
    {Δ;Γ}  v #() log or v' bot : TUnit.
218
  Proof.
219
    iIntros "Hlog".
220
    iApply bin_log_or_choice_1_r_val; eauto.
221 222
  Qed.

223 224 225 226 227
  Lemma bin_log_or_assoc1 Δ Γ (v1 v1' v2 v2' v3 v3' : val) :
    {Δ;Γ}  v1 log v1' : TArrow TUnit TUnit -
    {Δ;Γ}  v2 log v2' : TArrow TUnit TUnit -
    {Δ;Γ}  v3 log v3' : TArrow TUnit TUnit -
    {Δ;Γ}  or v1 (λ: <>, or v2 v3) log or (λ: <>, or v1' v2') v3' : TUnit.
228
  Proof.
229
    iIntros "Hv1 Hv2 Hv3".
230 231 232 233 234 235 236 237
    unlock or. simpl.
    rel_rec_l. rel_rec_l. (* TODO: SLOW, i guessbecause of solve_closed? *)
    rel_rec_r. rel_rec_r.
    rel_alloc_l as x "Hx".
    rel_alloc_r as y "Hy".
    repeat rel_let_l. repeat rel_let_r.
    rel_fork_r as j "Hj". rel_seq_r.
    iMod (inv_alloc orN _ (or_inv x) with "[Hx]") as "#Hinv".
238
    { close_inv. }
239 240 241 242 243 244 245 246 247 248 249 250 251
    rel_fork_l.
    iModIntro. iSplitR; [ by iApply assign_safe | ].
    rel_seq_l.
    rel_load_l_atomic.
    iInv orN as ">[Hx|Hx]" "Hcl";
      iExists _; iFrame; iModIntro; iNext; iIntros "Hx";
      repeat (rel_pure_l _).
    - rel_load_r.
      repeat (rel_pure_r _).
      rel_alloc_r as y' "Hy'".
      rel_let_r. rel_fork_r as k "Hk".
      rel_seq_r. rel_load_r.
      repeat (rel_pure_r _).
252
      iMod ("Hcl" with "[-Hv1 Hv2 Hv3]") as "_"; first close_inv.
253 254
      iApply (bin_log_related_app with "Hv1").
      iApply bin_log_related_unit.
255
    - iMod ("Hcl" with "[-Hv1 Hv2 Hv3 Hy Hj]") as "_"; first close_inv.
256 257 258
      rel_alloc_l as x' "Hx'". rel_let_l.
      iClear "Hinv".
      iMod (inv_alloc orN _ (or_inv x') with "[Hx']") as "#Hinv".
259
      { close_inv. }
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275
      rel_fork_l.
      iModIntro. iSplitR; [ by iApply assign_safe | ].
      apply bin_log_related_spec_ctx.
      iDestruct 1 as (ρ1) "#Hρ1".
      rel_seq_l.
      rel_load_l_atomic.
      iInv orN as ">[Hx'|Hx']" "Hcl";
        iExists _; iFrame; iModIntro; iNext; iIntros "Hx'";
        repeat (rel_pure_l _).
      + rel_load_r; repeat (rel_pure_r _).
        rel_alloc_r as y' "Hy'".
        rel_let_r. rel_fork_r as k "Hk".
        rel_let_r.
        tp_store k.
        rel_load_r.
        repeat (rel_pure_r _).
276
        iMod ("Hcl" with "[-Hv1 Hv2 Hv3]") as "_"; first close_inv.
277 278 279 280
        iApply (bin_log_related_app with "Hv2").
        iApply bin_log_related_unit.
      + tp_store j.
        rel_load_r; repeat (rel_pure_r _).
281
        iMod ("Hcl" with "[-Hv1 Hv2 Hv3]") as "_"; first close_inv.
282 283 284 285
        iApply (bin_log_related_app with "Hv3").
        iApply bin_log_related_unit.
  Qed.

286
  Lemma bin_log_let1 Δ Γ (v : val) (e : expr) τ :
287 288
    Closed {["x"]} e 
    Γ ⊢ₜ subst "x" v e : τ 
289
    {Δ;Γ}  let: "x" := v in e log subst "x" v e : τ.
290
  Proof.
291
    iIntros (? Hτ).
292 293 294
    assert (Closed  (Rec BAnon "x" e)).
    { unfold Closed. simpl. by rewrite right_id. }
    rel_let_l.
295
    by iApply binary_fundamental.
296 297
  Qed.

298
  Lemma bin_log_let2 Δ Γ (v : val) (e : expr) τ :
299 300
    Closed {["x"]} e 
    Γ ⊢ₜ subst "x" v e : τ 
301
    {Δ;Γ}  subst "x" v e log (let: "x" := v in e) : τ.
302
  Proof.
303
    iIntros (? Hτ).
304 305 306
    assert (Closed  (Rec BAnon "x" e)).
    { unfold Closed. simpl. by rewrite right_id. }
    rel_let_r.
307
    by iApply binary_fundamental.
308 309
  Qed.

Dan Frumin's avatar
Dan Frumin committed
310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369
End contents.

Section theory.
  Lemma or_idempotency_1 (v : val) :
     ⊢ₜ v : TArrow TUnit TUnit 
      or v v ctx v #() : TUnit.
  Proof.
    intros Ht.
    eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
    iApply bin_log_or_idem_l; eauto.
    by iApply binary_fundamental.
  Qed.
  Lemma or_idempotency_2 (v : val) :
     ⊢ₜ v : TArrow TUnit TUnit 
      v #() ctx or v v : TUnit.
  Proof.
    intros Ht.
    eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
    iApply bin_log_or_idem_r; eauto.
    by iApply binary_fundamental.
  Qed.

  Lemma or_commutativity (v1 v2 : val) :
     ⊢ₜ v1 : TArrow TUnit TUnit 
     ⊢ₜ v2 : TArrow TUnit TUnit 
      or v1 v2 ctx or v2 v1 : TUnit.
  Proof.
    intros Ht1 Ht2.
    eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
    iApply bin_log_or_commute; eauto; by iApply binary_fundamental.
  Qed.

  Lemma or_unital_1 (v : val) :
     ⊢ₜ v : TArrow TUnit TUnit 
      or v bot ctx v #() : TUnit.
  Proof.
    intros Ht.
    eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
    iApply bin_log_or_bot_l; eauto.
    by iApply binary_fundamental.
  Qed.
  Lemma or_unital_2 (v : val) :
     ⊢ₜ v : TArrow TUnit TUnit 
      v #() ctx or v bot : TUnit.
  Proof.
    intros Ht.
    eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
    iApply bin_log_or_bot_r; eauto.
    by iApply binary_fundamental.
  Qed.

  Lemma or_choice_1 (v1 v2 : val) :
     ⊢ₜ v1 : TArrow TUnit TUnit 
      v1 #() ctx or v1 v2 : TUnit.
  Proof.
    intros Ht.
    eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
    iApply bin_log_or_choice_1_r_val; eauto.
    by iApply binary_fundamental.
  Qed.
370

Dan Frumin's avatar
Dan Frumin committed
371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396
  Lemma or_assoc_1 (v1 v2 v3 : val) :
     ⊢ₜ v1 : TArrow TUnit TUnit 
     ⊢ₜ v2 : TArrow TUnit TUnit 
     ⊢ₜ v3 : TArrow TUnit TUnit 
      (or v1 (λ: <>, or v2 v3))%E ctx (or (λ: <>, or v1 v2) v3)%E : TUnit.
  Proof.
    intros Ht1 Ht2 Ht3.
    eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
    iApply bin_log_or_assoc1; eauto; by iApply binary_fundamental.
  Qed.

  (* The associativity in the other direction, assuming commutativity:
     (v1 or v2) or v3
    (v2 or v1) or v3   comm
    v3 or (v2 or v1)   comm
    (v3 or v2) or v1   assoc1
    (v2 or v3) or v1   comm
    v1 or (v2 or v3)
   *)
  (* Lemma or_assoc_2 (v1 v2 v3 : val) : *)
  (*    ⊢ₜ v1 : TArrow TUnit TUnit  *)
  (*    ⊢ₜ v2 : TArrow TUnit TUnit  *)
  (*    ⊢ₜ v3 : TArrow TUnit TUnit  *)
  (*     (or (λ: <>, or v1 v2) v3)%E ctx (or v1 (λ: <>, or v2 v3))%E : TUnit. *)
    
End theory.