Associativity of `or` and the "let equivalance"

theories/examples/or.v

@@ -221,4 +221,105 @@ Section rules.
     iApply bin_log_or_choice_1_r_val; eauto.
   Qed.
 
+  Lemma bin_log_or_assoc1 Δ Γ E (v1 v1' v2 v2' v3 v3' : val) :
+    ↑orN ⊆ E →
+    ↑logrelN ⊆ E →
+    {E,E;Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ v2 ≤log≤ v2' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ v3 ≤log≤ v3' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ or v1 (λ: <>, or v2 v3) ≤log≤ or (λ: <>, or v1' v2') v3' : TUnit.
+  Proof.
+    iIntros (??) "Hv1 Hv2 Hv3".
+    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.
+
+  (* 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 bin_log_let1 Δ Γ E (v : val) (e : expr) τ :
+    Closed {["x"]} e →
+    ↑logrelN ⊆ E →
+    Γ ⊢ₜ subst "x" v e : τ →
+    {E,E;Δ;Γ} ⊨ let: "x" := v in e ≤log≤ subst "x" v e : τ.
+  Proof.
+    iIntros (?? Hτ).
+    assert (Closed ∅ (Rec BAnon "x" e)).
+    { unfold Closed. simpl. by rewrite right_id. }
+    rel_let_l.
+    by iApply binary_fundamental_masked.
+  Qed.
+
+  Lemma bin_log_let2 Δ Γ E (v : val) (e : expr) τ :
+    Closed {["x"]} e →
+    ↑logrelN ⊆ E →
+    Γ ⊢ₜ subst "x" v e : τ →
+    {E,E;Δ;Γ} ⊨ subst "x" v e ≤log≤ (let: "x" := v in e) : τ.
+  Proof.
+    iIntros (?? Hτ).
+    assert (Closed ∅ (Rec BAnon "x" e)).
+    { unfold Closed. simpl. by rewrite right_id. }
+    rel_let_r.
+    by iApply binary_fundamental_masked.
+  Qed.
+
 End rules.
+