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 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 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 103
  Ltac close_shoot := iNext; (iLeft + iRight); by iFrame.

104 105
  Lemma assign_safe x :
    inv orN (or_inv x)
106 107 108
      WP #x <- #1 {{ _, True }}.
  Proof.
    iIntros "#Hinv".
109 110
    iNext. iInv orN as ">[Hx | Hx]" "Hcl"; wp_store;
      (iMod ("Hcl" with "[-]"); first close_shoot); 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 120 121 122 123
    unlock or. repeat rel_rec_r. repeat rel_rec_l.
    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
    iMod (inv_alloc orN _ (or_inv x) with "[Hx]") as "#Hinv".
125 126 127 128 129
    { close_shoot. }
    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 133 134 135 136 137 138
      iExists _; iFrame; iModIntro; iNext; iIntros "Hx";
      rel_op_l; rel_if_l.
    + apply bin_log_related_spec_ctx.
      iDestruct 1 as (ρ1) "#Hρ1".
      (* TODO: tp tactics should be aware of that ^ *)
      tp_store j.
      rel_load_r.
      repeat (rel_pure_r _).
139 140 141
      iMod ("Hcl" with "[-Hv1 Hv2]"); first close_shoot.
      iApply (bin_log_related_app with "Hv2").
      iApply bin_log_related_unit.
142 143
    + rel_load_r.
      repeat (rel_pure_r _).
144 145 146 147 148
      iMod ("Hcl" with "[-Hv1 Hv2]"); first close_shoot.
      iApply (bin_log_related_app with "Hv1").
      iApply bin_log_related_unit.
  Qed.

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

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

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

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

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

224 225 226 227 228
  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.
229
  Proof.
230
    iIntros "Hv1 Hv2 Hv3".
231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
    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".
    { close_shoot. }
    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 _).
      iMod ("Hcl" with "[-Hv1 Hv2 Hv3]") as "_"; first close_shoot.
      iApply (bin_log_related_app with "Hv1").
      iApply bin_log_related_unit.
    - iMod ("Hcl" with "[-Hv1 Hv2 Hv3 Hy Hj]") as "_"; first close_shoot.
      rel_alloc_l as x' "Hx'". rel_let_l.
      iClear "Hinv".
      iMod (inv_alloc orN _ (or_inv x') with "[Hx']") as "#Hinv".
      { close_shoot. }
      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 _).
        iMod ("Hcl" with "[-Hv1 Hv2 Hv3]") as "_"; first close_shoot.
        iApply (bin_log_related_app with "Hv2").
        iApply bin_log_related_unit.
      + tp_store j.
        rel_load_r; repeat (rel_pure_r _).
        iMod ("Hcl" with "[-Hv1 Hv2 Hv3]") as "_"; first close_shoot.
        iApply (bin_log_related_app with "Hv3").
        iApply bin_log_related_unit.
  Qed.

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

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

Dan Frumin committed
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 370
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.
371

Dan Frumin committed
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 397
  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.