Generalize the algebraic laws for parallel or composition

theories/examples/or.v

+(* We can simulate non-determinism with concurrency.
+   In this file we derive the algebraic laws for parallel "or"/demonic choice  combinator. *)
 From iris.proofmode Require Import tactics.
 From iris_logrel Require Export logrel examples.various.
 
@@ -30,38 +32,44 @@ Section rules.
     iApply binary_fundamental_masked; eauto with typeable.
   Qed.
 
-  Lemma bin_log_or_choice_1_r_val Δ Γ E (v1 v2 : val) :
+  Lemma bin_log_or_choice_1_r_val Δ Γ E (v1 v1' v2 : val) :
     ↑logrelN ⊆ E →
-    Γ ⊢ₜ v1 : TArrow TUnit TUnit →
-    {E,E;Δ;Γ} ⊨ v1 #() ≤log≤ or v1 v2 : TUnit.
+    {E,E;Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ v1 #() ≤log≤ or v1' v2 : TUnit.
   Proof.
-    iIntros (??).
+    iIntros (?) "Hlog".
     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 _).
-    iApply binary_fundamental_masked; eauto with typeable.
+    iApply (bin_log_related_app with "Hlog").
+    iApply bin_log_related_unit.
   Qed.
 
-  Lemma bin_log_or_choice_1_r Δ Γ E (e1 : expr) (v2 : val) :
+  Lemma bin_log_or_choice_1_r_val_typed Δ Γ E (v1 v2 : val) :
     ↑logrelN ⊆ E →
-    Γ ⊢ₜ e1 : TArrow TUnit TUnit →
-    {E,E;Δ;Γ} ⊨ e1 #() ≤log≤ or e1 v2 : TUnit.
+    Γ ⊢ₜ v1 : TArrow TUnit TUnit →
+    {E,E;Δ;Γ} ⊨ v1 #() ≤log≤ or v1 v2 : TUnit.
   Proof.
     iIntros (??).
+    iApply bin_log_or_choice_1_r_val; eauto.
+    iApply binary_fundamental_masked; eauto with typeable.
+  Qed.
+
+  Lemma bin_log_or_choice_1_r Δ Γ E (e1 e1' : expr) (v2 : val) :
+    ↑logrelN ⊆ E →
+    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ e1 #() ≤log≤ or e1' v2 : TUnit.
+  Proof.
+    iIntros (?) "Hlog".
     rel_bind_l e1.
-    rel_bind_r e1.
-    iApply related_bind.
-    { iApply binary_fundamental_masked; eauto with typeable. }
+    rel_bind_r e1'.
+    iApply (related_bind with "Hlog").
     iIntros ([f f']) "#Hf /=".
-    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 _).
-    iApply related_ret. simpl.
-    iApply ("Hf" $! (#(),#())); eauto.
+    iApply bin_log_or_choice_1_r_val; eauto.
+    iApply (related_ret ⊤).
+    iApply interp_ret; eauto using to_of_val.
   Qed.
 
   Lemma bin_log_or_choice_1_r_body Δ Γ E (e1 : expr) (v2 : val) :
@@ -94,14 +102,14 @@ Section rules.
     + iMod ("Hcl" with "[-]"); first close_shoot; eauto.
   Qed.
 
-  Lemma bin_log_or_commute `{oneshotG Σ} Δ Γ E (v1 v2 : val) :
+  Lemma bin_log_or_commute `{oneshotG Σ} Δ Γ E (v1 v1' v2 v2' : val) :
     ↑shootN ⊆ E →
     ↑logrelN ⊆ E →
-    Γ ⊢ₜ v1 : TArrow TUnit TUnit →
-    Γ ⊢ₜ v2 : TArrow TUnit TUnit →
-    {E,E;Δ;Γ} ⊨ or v2 v1 ≤log≤ or v1 v2 : TUnit.
+    {E,E;Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ v2 ≤log≤ v2' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ or v2 v1 ≤log≤ or v1' v2' : TUnit.
   Proof.
-    iIntros (????).
+    iIntros (??) "Hv1 Hv2".
     unlock or. repeat rel_rec_r. repeat rel_rec_l.
     rel_alloc_l as x "Hx".
     rel_alloc_r as y "Hy".
@@ -116,7 +124,7 @@ Section rules.
     iModIntro. iSplitR; [ by iApply assign_safe | ].
     rel_seq_l.
     rel_load_l_atomic.
-    iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl"; 
+    iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl";
       iExists _; iFrame; iModIntro; iNext; iIntros "Hx";
       rel_op_l; rel_if_l.
     + apply bin_log_related_spec_ctx.
@@ -125,15 +133,26 @@ Section rules.
       tp_store j.
       rel_load_r.
       repeat (rel_pure_r _).
-      iMod ("Hcl" with "[-]"); first close_shoot.
-      iApply binary_fundamental_masked; eauto with typeable.
+      iMod ("Hcl" with "[-Hv1 Hv2]"); first close_shoot.
+      iApply (bin_log_related_app with "Hv2").
+      iApply bin_log_related_unit.
     + rel_load_r.
       repeat (rel_pure_r _).
-      iMod ("Hcl" with "[-]"); first close_shoot.
-      iApply binary_fundamental_masked; eauto with typeable.
+      iMod ("Hcl" with "[-Hv1 Hv2]"); first close_shoot.
+      iApply (bin_log_related_app with "Hv1").
+      iApply bin_log_related_unit.
+  Qed.
+
+  Lemma bin_log_or_idem_r Δ Γ E (v v' : val) :
+    ↑logrelN ⊆ E →
+    {E,E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ v #() ≤log≤ or v' v' : TUnit.
+  Proof.
+    iIntros (?) "Hlog".
+    by iApply bin_log_or_choice_1_r_val.
   Qed.
 
-  Lemma bin_log_or_idem_r Δ Γ E e :
+  Lemma bin_log_or_idem_r_body Δ Γ E e :
     Closed ∅ e →
     ↑logrelN ⊆ E →
     Γ ⊢ₜ e : TUnit →
@@ -144,14 +163,13 @@ Section rules.
     unlock. eauto. (* TODO :( *)
   Qed.
 
-  Lemma bin_log_or_idem_l `{oneshotG Σ} Δ Γ E e :
-    Closed ∅ e →
+  Lemma bin_log_or_idem_l `{oneshotG Σ} Δ Γ E (v v' : val) :
     ↑shootN ⊆ E →
     ↑logrelN ⊆ E →
-    Γ ⊢ₜ e : TUnit →
-    {E,E;Δ;Γ} ⊨ or (λ: <>, e) (λ: <>, e) ≤log≤ e : TUnit.
+    {E,E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ or v v ≤log≤ v' #() : TUnit.
   Proof.
-    iIntros (????).
+    iIntros (??) "Hlog".
     unlock or. repeat rel_rec_l.
     rel_alloc_l as x "Hx".
     repeat rel_let_l.
@@ -164,23 +182,24 @@ Section rules.
     iModIntro. iSplitR; [ by iApply assign_safe | ].
     rel_seq_l.
     rel_load_l_atomic.
-    iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl"; 
+    iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl";
       iExists _; iFrame; iModIntro; iNext; iIntros "Hx";
-        rel_op_l; rel_if_l; rel_seq_l.
-    + iMod ("Hcl" with "[-]"); first close_shoot.
-      iApply binary_fundamental_masked; eauto with typeable.
-    + iMod ("Hcl" with "[-]"); first close_shoot.
-      iApply binary_fundamental_masked; eauto with typeable.    
+        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.
   Qed.
 
-  Lemma bin_log_or_bot_l `{oneshotG Σ} Δ Γ E e :
-    Closed ∅ e →
+  Lemma bin_log_or_bot_l `{oneshotG Σ} Δ Γ E (v v' : val) :
     ↑shootN ⊆ E →
     ↑logrelN ⊆ E →
-    Γ ⊢ₜ e : TUnit →
-    {E,E;Δ;Γ} ⊨ or (λ: <>, e) bot ≤log≤ e : TUnit.
+    {E,E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ or v bot ≤log≤ v' #() : TUnit.
   Proof.
-    iIntros (????).
+    iIntros (??) "Hlog".
     unlock or. repeat rel_rec_l.
     rel_alloc_l as x "Hx".
     repeat rel_let_l.
@@ -193,24 +212,23 @@ Section rules.
     iModIntro. iSplitR; [ by iApply assign_safe | ].
     rel_seq_l.
     rel_load_l_atomic.
-    iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl"; 
+    iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl";
       iExists _; iFrame; iModIntro; iNext; iIntros "Hx";
       rel_op_l; rel_if_l.
-    + iMod ("Hcl" with "[-]"); first close_shoot.
-      rel_seq_l.
-      iApply binary_fundamental_masked; eauto with typeable.
-    + iMod ("Hcl" with "[-]"); first close_shoot.
+    + 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.
       rel_apply_l (bot_l False). iIntros ([]).
   Qed.
 
-  Lemma bin_log_or_bot_r Δ Γ E e :
-    Closed ∅ e →
+  Lemma bin_log_or_bot_r Δ Γ E (v v' : val) :
     ↑logrelN ⊆ E →
-    Γ ⊢ₜ e : TUnit →
-    {E,E;Δ;Γ} ⊨ e ≤log≤ or (λ: <>, e) bot : TUnit.
+    {E,E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗
+    {E,E;Δ;Γ} ⊨ v #() ≤log≤ or v' bot : TUnit.
   Proof.
-    iIntros (???).
-    iApply bin_log_or_choice_1_r_body; eauto.
+    iIntros (?) "Hlog".
+    iApply bin_log_or_choice_1_r_val; eauto.
   Qed.
 
 End rules.