or.v 12.8 KB
 Dan Frumin committed Nov 29, 2017 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 Dec 01, 2017 14 15 `````` where every v_i is well-typed Unit -> Unit `````` Dan Frumin committed Nov 29, 2017 16 ``````*) `````` Dan Frumin committed Sep 28, 2017 17 ``````From iris.proofmode Require Import tactics. `````` Dan Frumin committed Dec 10, 2017 18 ``````From iris_logrel Require Export logrel examples.bot. `````` Dan Frumin committed Sep 28, 2017 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 Dec 01, 2017 34 ``````Section contents. `````` Dan Frumin committed Sep 28, 2017 35 36 `````` Context `{logrelG Σ}. `````` Dan Frumin committed Jan 28, 2018 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. `````` Dan Frumin committed Sep 28, 2017 41 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 42 `````` iIntros "He1 He2". `````` Dan Frumin committed Sep 28, 2017 43 44 `````` iApply (bin_log_related_app with "[He1] He2"). iApply (bin_log_related_app with "[] He1"). `````` Dan Frumin committed Jan 28, 2018 45 `````` iApply binary_fundamental; eauto with typeable. `````` Dan Frumin committed Sep 28, 2017 46 47 `````` Qed. `````` Dan Frumin committed Jan 28, 2018 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. `````` Dan Frumin committed Sep 28, 2017 51 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 52 `````` iIntros "Hlog". `````` Dan Frumin committed Sep 28, 2017 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 _). `````` Dan Frumin committed Nov 21, 2017 58 59 `````` iApply (bin_log_related_app with "Hlog"). iApply bin_log_related_unit. `````` Dan Frumin committed Sep 28, 2017 60 61 `````` Qed. `````` Dan Frumin committed Jan 28, 2018 62 `````` Lemma bin_log_or_choice_1_r_val_typed Δ Γ (v1 v2 : val) : `````` Dan Frumin committed Nov 21, 2017 63 `````` Γ ⊢ₜ v1 : TArrow TUnit TUnit → `````` Dan Frumin committed Jan 28, 2018 64 `````` {Δ;Γ} ⊨ v1 #() ≤log≤ or v1 v2 : TUnit. `````` Dan Frumin committed Sep 28, 2017 65 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 66 `````` iIntros (?). `````` Dan Frumin committed Nov 21, 2017 67 `````` iApply bin_log_or_choice_1_r_val; eauto. `````` Dan Frumin committed Jan 28, 2018 68 `````` iApply binary_fundamental; eauto with typeable. `````` Dan Frumin committed Nov 21, 2017 69 70 `````` Qed. `````` Dan Frumin committed Jan 28, 2018 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. `````` Dan Frumin committed Nov 21, 2017 74 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 75 `````` iIntros "Hlog". `````` Dan Frumin committed Sep 28, 2017 76 `````` rel_bind_l e1. `````` Dan Frumin committed Nov 21, 2017 77 78 `````` rel_bind_r e1'. iApply (related_bind with "Hlog"). `````` Dan Frumin committed Sep 28, 2017 79 `````` iIntros ([f f']) "#Hf /=". `````` Dan Frumin committed Nov 21, 2017 80 81 82 `````` iApply bin_log_or_choice_1_r_val; eauto. iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val. `````` Dan Frumin committed Sep 28, 2017 83 84 `````` Qed. `````` Dan Frumin committed Jan 28, 2018 85 `````` Lemma bin_log_or_choice_1_r_body Δ Γ (e1 : expr) (v2 : val) : `````` Dan Frumin committed Sep 28, 2017 86 87 `````` Closed ∅ e1 → Γ ⊢ₜ e1 : TUnit → `````` Dan Frumin committed Jan 28, 2018 88 `````` {Δ;Γ} ⊨ e1 ≤log≤ or (λ: <>, e1) v2 : TUnit. `````` Dan Frumin committed Sep 28, 2017 89 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 90 `````` iIntros (??). `````` Dan Frumin committed Sep 28, 2017 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 _). `````` Dan Frumin committed Jan 28, 2018 96 `````` iApply binary_fundamental; eauto with typeable. `````` Dan Frumin committed Sep 28, 2017 97 98 `````` Qed. `````` Dan Frumin committed Nov 29, 2017 99 100 101 `````` Definition or_inv x : iProp Σ := (x ↦ᵢ #0 ∨ x ↦ᵢ #1)%I. Definition orN := nroot .@ "orN". `````` Dan Frumin committed Apr 09, 2018 102 `````` Ltac close_inv := iNext; (iLeft + iRight); by iFrame. `````` Dan Frumin committed Sep 28, 2017 103 `````` `````` Dan Frumin committed Nov 29, 2017 104 105 `````` Lemma assign_safe x : inv orN (or_inv x) `````` Dan Frumin committed Sep 28, 2017 106 107 108 `````` ⊢ ▷ WP #x <- #1 {{ _, True }}. Proof. iIntros "#Hinv". `````` Dan Frumin committed Nov 29, 2017 109 `````` iNext. iInv orN as ">[Hx | Hx]" "Hcl"; wp_store; `````` Dan Frumin committed Apr 09, 2018 110 `````` (iMod ("Hcl" with "[-]"); first close_inv); eauto. `````` Dan Frumin committed Sep 28, 2017 111 112 `````` Qed. `````` Dan Frumin committed Jan 28, 2018 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. `````` Dan Frumin committed Sep 28, 2017 117 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 118 `````` iIntros "Hv1 Hv2". `````` Dan Frumin committed Apr 09, 2018 119 `````` unlock or; simpl. repeat rel_rec_r. repeat rel_rec_l. `````` Dan Frumin committed Sep 28, 2017 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. `````` Dan Frumin committed Apr 09, 2018 124 125 `````` iMod (inv_alloc orN _ (or_inv x) with "[Hx]") as "#Hinv"; first close_inv. `````` Dan Frumin committed Sep 28, 2017 126 127 128 129 `````` rel_fork_l. iModIntro. iSplitR; [ by iApply assign_safe | ]. rel_seq_l. rel_load_l_atomic. `````` Dan Frumin committed Nov 29, 2017 130 `````` iInv orN as ">[Hx|Hx]" "Hcl"; `````` Dan Frumin committed Sep 28, 2017 131 132 `````` iExists _; iFrame; iModIntro; iNext; iIntros "Hx"; rel_op_l; rel_if_l. `````` Dan Frumin committed Apr 09, 2018 133 134 `````` + apply bin_log_related_spec_ctx; iDestruct 1 as (ρ1) "#Hρ1". (* TODO: tp tactics should be aware of spec_ctx *) `````` Dan Frumin committed Sep 28, 2017 135 136 137 `````` tp_store j. rel_load_r. repeat (rel_pure_r _). `````` Dan Frumin committed Apr 09, 2018 138 `````` iMod ("Hcl" with "[-Hv1 Hv2]"); first close_inv. `````` Dan Frumin committed Nov 21, 2017 139 140 `````` iApply (bin_log_related_app with "Hv2"). iApply bin_log_related_unit. `````` Dan Frumin committed Sep 28, 2017 141 142 `````` + rel_load_r. repeat (rel_pure_r _). `````` Dan Frumin committed Apr 09, 2018 143 `````` iMod ("Hcl" with "[-Hv1 Hv2]"); first close_inv. `````` Dan Frumin committed Nov 21, 2017 144 145 146 147 `````` iApply (bin_log_related_app with "Hv1"). iApply bin_log_related_unit. Qed. `````` Dan Frumin committed Jan 28, 2018 148 149 150 `````` Lemma bin_log_or_idem_r Δ Γ (v v' : val) : {Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {Δ;Γ} ⊨ v #() ≤log≤ or v' v' : TUnit. `````` Dan Frumin committed Nov 21, 2017 151 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 152 `````` iIntros "Hlog". `````` Dan Frumin committed Nov 21, 2017 153 `````` by iApply bin_log_or_choice_1_r_val. `````` Dan Frumin committed Sep 28, 2017 154 155 `````` Qed. `````` Dan Frumin committed Jan 28, 2018 156 `````` Lemma bin_log_or_idem_r_body Δ Γ e : `````` Dan Frumin committed Sep 28, 2017 157 158 `````` Closed ∅ e → Γ ⊢ₜ e : TUnit → `````` Dan Frumin committed Jan 28, 2018 159 `````` {Δ;Γ} ⊨ e ≤log≤ or (λ: <>, e) (λ: <>, e) : TUnit. `````` Dan Frumin committed Sep 28, 2017 160 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 161 162 `````` iIntros (??). iPoseProof (bin_log_or_choice_1_r_body Δ _ e (λ: <>, e)) as "HZ"; eauto. `````` Dan Frumin committed Sep 28, 2017 163 164 165 `````` unlock. eauto. (* TODO :( *) Qed. `````` Dan Frumin committed Jan 28, 2018 166 167 168 `````` Lemma bin_log_or_idem_l Δ Γ (v v' : val) : {Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {Δ;Γ} ⊨ or v v ≤log≤ v' #() : TUnit. `````` Dan Frumin committed Sep 28, 2017 169 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 170 `````` iIntros "Hlog". `````` Dan Frumin committed Sep 28, 2017 171 172 173 `````` unlock or. repeat rel_rec_l. rel_alloc_l as x "Hx". repeat rel_let_l. `````` Dan Frumin committed Nov 29, 2017 174 `````` iMod (inv_alloc orN _ (or_inv x)%I with "[Hx]") as "#Hinv". `````` Dan Frumin committed Apr 09, 2018 175 `````` { close_inv. } `````` Dan Frumin committed Sep 28, 2017 176 177 178 179 `````` rel_fork_l. iModIntro. iSplitR; [ by iApply assign_safe | ]. rel_seq_l. rel_load_l_atomic. `````` Dan Frumin committed Nov 29, 2017 180 `````` iInv orN as ">[Hx|Hx]" "Hcl"; `````` Dan Frumin committed Sep 28, 2017 181 `````` iExists _; iFrame; iModIntro; iNext; iIntros "Hx"; `````` Dan Frumin committed Nov 21, 2017 182 `````` rel_op_l; rel_if_l. `````` Dan Frumin committed Apr 09, 2018 183 `````` + iMod ("Hcl" with "[-Hlog]"); first close_inv. `````` Dan Frumin committed Nov 21, 2017 184 185 `````` iApply (bin_log_related_app with "Hlog"). iApply bin_log_related_unit. `````` Dan Frumin committed Apr 09, 2018 186 `````` + iMod ("Hcl" with "[-Hlog]"); first close_inv. `````` Dan Frumin committed Nov 21, 2017 187 188 `````` iApply (bin_log_related_app with "Hlog"). iApply bin_log_related_unit. `````` Dan Frumin committed Sep 28, 2017 189 190 `````` Qed. `````` Dan Frumin committed Jan 28, 2018 191 192 193 `````` Lemma bin_log_or_bot_l Δ Γ (v v' : val) : {Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {Δ;Γ} ⊨ or v bot ≤log≤ v' #() : TUnit. `````` Dan Frumin committed Sep 28, 2017 194 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 195 `````` iIntros "Hlog". `````` Dan Frumin committed Sep 28, 2017 196 197 198 `````` unlock or. repeat rel_rec_l. rel_alloc_l as x "Hx". repeat rel_let_l. `````` Dan Frumin committed Nov 29, 2017 199 `````` iMod (inv_alloc orN _ (or_inv x)%I with "[Hx]") as "#Hinv". `````` Dan Frumin committed Apr 09, 2018 200 `````` { close_inv. } `````` Dan Frumin committed Sep 28, 2017 201 202 203 204 `````` rel_fork_l. iModIntro. iSplitR; [ by iApply assign_safe | ]. rel_seq_l. rel_load_l_atomic. `````` Dan Frumin committed Nov 29, 2017 205 `````` iInv orN as ">[Hx|Hx]" "Hcl"; `````` Dan Frumin committed Sep 28, 2017 206 207 `````` iExists _; iFrame; iModIntro; iNext; iIntros "Hx"; rel_op_l; rel_if_l. `````` Dan Frumin committed Apr 09, 2018 208 `````` + iMod ("Hcl" with "[-Hlog]"); first close_inv. `````` Dan Frumin committed Nov 21, 2017 209 210 `````` iApply (bin_log_related_app with "Hlog"). iApply bin_log_related_unit. `````` Dan Frumin committed Apr 09, 2018 211 `````` + iMod ("Hcl" with "[-Hlog]"); first close_inv. `````` Dan Frumin committed Dec 13, 2017 212 `````` rel_apply_l bot_l. `````` Dan Frumin committed Sep 28, 2017 213 214 `````` Qed. `````` Dan Frumin committed Jan 28, 2018 215 216 217 `````` Lemma bin_log_or_bot_r Δ Γ (v v' : val) : {Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {Δ;Γ} ⊨ v #() ≤log≤ or v' bot : TUnit. `````` Dan Frumin committed Sep 28, 2017 218 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 219 `````` iIntros "Hlog". `````` Dan Frumin committed Nov 21, 2017 220 `````` iApply bin_log_or_choice_1_r_val; eauto. `````` Dan Frumin committed Sep 28, 2017 221 222 `````` Qed. `````` Dan Frumin committed Jan 28, 2018 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. `````` Dan Frumin committed Nov 29, 2017 228 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 229 `````` iIntros "Hv1 Hv2 Hv3". `````` Dan Frumin committed Nov 29, 2017 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". `````` Dan Frumin committed Apr 09, 2018 238 `````` { close_inv. } `````` Dan Frumin committed Nov 29, 2017 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 _). `````` Dan Frumin committed Apr 09, 2018 252 `````` iMod ("Hcl" with "[-Hv1 Hv2 Hv3]") as "_"; first close_inv. `````` Dan Frumin committed Nov 29, 2017 253 254 `````` iApply (bin_log_related_app with "Hv1"). iApply bin_log_related_unit. `````` Dan Frumin committed Apr 09, 2018 255 `````` - iMod ("Hcl" with "[-Hv1 Hv2 Hv3 Hy Hj]") as "_"; first close_inv. `````` Dan Frumin committed Nov 29, 2017 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". `````` Dan Frumin committed Apr 09, 2018 259 `````` { close_inv. } `````` Dan Frumin committed Nov 29, 2017 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 _). `````` Dan Frumin committed Apr 09, 2018 276 `````` iMod ("Hcl" with "[-Hv1 Hv2 Hv3]") as "_"; first close_inv. `````` Dan Frumin committed Nov 29, 2017 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 _). `````` Dan Frumin committed Apr 09, 2018 281 `````` iMod ("Hcl" with "[-Hv1 Hv2 Hv3]") as "_"; first close_inv. `````` Dan Frumin committed Nov 29, 2017 282 283 284 285 `````` iApply (bin_log_related_app with "Hv3"). iApply bin_log_related_unit. Qed. `````` Dan Frumin committed Jan 28, 2018 286 `````` Lemma bin_log_let1 Δ Γ (v : val) (e : expr) τ : `````` Dan Frumin committed Nov 29, 2017 287 288 `````` Closed {["x"]} e → Γ ⊢ₜ subst "x" v e : τ → `````` Dan Frumin committed Jan 28, 2018 289 `````` {Δ;Γ} ⊨ let: "x" := v in e ≤log≤ subst "x" v e : τ. `````` Dan Frumin committed Nov 29, 2017 290 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 291 `````` iIntros (? Hτ). `````` Dan Frumin committed Nov 29, 2017 292 293 294 `````` assert (Closed ∅ (Rec BAnon "x" e)). { unfold Closed. simpl. by rewrite right_id. } rel_let_l. `````` Dan Frumin committed Jan 28, 2018 295 `````` by iApply binary_fundamental. `````` Dan Frumin committed Nov 29, 2017 296 297 `````` Qed. `````` Dan Frumin committed Jan 28, 2018 298 `````` Lemma bin_log_let2 Δ Γ (v : val) (e : expr) τ : `````` Dan Frumin committed Nov 29, 2017 299 300 `````` Closed {["x"]} e → Γ ⊢ₜ subst "x" v e : τ → `````` Dan Frumin committed Jan 28, 2018 301 `````` {Δ;Γ} ⊨ subst "x" v e ≤log≤ (let: "x" := v in e) : τ. `````` Dan Frumin committed Nov 29, 2017 302 `````` Proof. `````` Dan Frumin committed Jan 28, 2018 303 `````` iIntros (? Hτ). `````` Dan Frumin committed Nov 29, 2017 304 305 306 `````` assert (Closed ∅ (Rec BAnon "x" e)). { unfold Closed. simpl. by rewrite right_id. } rel_let_r. `````` Dan Frumin committed Jan 28, 2018 307 `````` by iApply binary_fundamental. `````` Dan Frumin committed Nov 29, 2017 308 309 `````` Qed. `````` Dan Frumin committed Dec 01, 2017 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. `````` Dan Frumin committed Nov 29, 2017 370 `````` `````` Dan Frumin committed Dec 01, 2017 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.``````