Add Brouwer seminar examples

_CoqProject

@@ -52,3 +52,4 @@ theories/tests/tactics2.v
 theories/tests/liftings.v
 theories/tests/value.v
 theories/examples/coqpl.v
+theories/examples/brouwers.v
\ No newline at end of file

theories/examples/brouwers.v

+(** * ReLoC examples for the brouwers seminar. *)
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import csum agree excl.
+From iris_logrel Require Import logrel.
+
+Section refinements.
+(* boilerplate sprinkled with some "magic" *)
+Context `{logrelG Σ}.
+Notation D := (prodC valC valC -n> iProp Σ).
+Program Definition valrel' : (val * val → iProp Σ) → D :=
+  fun f => λne x, f x.
+Solve Obligations with solve_proper.
+Definition valrel (f : val → val → iProp Σ) : D :=
+  valrel' $ λ vv, f (vv.1) (vv.2).
+
+(** ** Example 1: Bit module refinement *)
+Definition bitT : type := ∃: TVar 0 × (TVar 0 → TVar 0) × (TVar 0 → Bool).
+
+Definition bit_bool : val :=
+  pack (#true, (λ: "b", ¬ "b"), (λ: "b", "b")).
+
+Definition bit_nat : val :=
+  pack (#1, (λ: "n", if: ("n" = #0) then #1 else #0), (λ: "b", "b" = #1)).
+  
+Definition f (b : bool) : nat := if b then 1 else 0.
+(** R ⊆ Bool × Nat = { (true, 1), (false, 0) }*)
+Definition R : D := valrel $ λ v1 v2,
+                    (∃ b : bool, ⌜v1 = #b⌝ ∗ ⌜v2 = #(f b)⌝)%I.
+
+Instance R_persistent ww : Persistent (R ww).
+Proof. apply _. Qed.
+
+Ltac rel_arrow_val := iApply bin_log_related_arrow_val; try by unlock.
+Ltac rel_arrow := iApply bin_log_related_arrow; auto.
+
+Lemma bit_refinement Δ Γ :
+  {Δ;Γ} ⊨ bit_bool ≤log≤ bit_nat : bitT.
+Proof.
+  unlock bit_bool bit_nat; simpl.
+  iApply (bin_log_related_pack R).
+  repeat iApply bin_log_related_pair.
+  - rel_finish.
+  - rel_arrow_val. simpl.
+    iIntros "!#" (v1 v2).
+    iIntros ([b [? ?]]); simplify_eq/=.
+    rel_rec_l. rel_rec_r.
+    rel_op_l. rel_op_r.
+    destruct b; simpl; rel_if_r; rel_finish.
+  - rel_arrow_val. simpl.
+    iIntros "!#" (v1 v2).
+    iIntros ([b [? ?]]); simplify_eq/=.
+    rel_rec_l. rel_rec_r.
+    rel_op_r.
+    destruct b; rel_finish.
+Qed.
+  
+(** ** Example 2: handling mutable state *)
+Lemma test_goal Δ Γ (l k : loc) :
+  l ↦ᵢ #1 -∗ k ↦ₛ #0 -∗
+    {Δ;Γ} ⊨ !#l ≤log≤ (#k <- #1;; !#k) : TNat.
+Proof.
+  iIntros "Hl Hk".
+  rel_store_r. rel_seq_r.
+  rel_load_l. rel_load_r.
+  iApply bin_log_related_nat.
+Qed.
+
+(** ** Example 3: higher-order + state *)
+Definition N := logrelN.@"yolorolo".
+Lemma higher_order_stateful Δ Γ :
+  {Δ;Γ} ⊨
+        let: "x" := ref #1 in
+        (λ: "f", "f" #();; !"x")
+          ≤log≤
+        (λ: "f", "f" #();; #1)
+        : ((Unit → Unit) → TNat).
+Proof.
+  rel_alloc_l as l "Hl".
+  rel_let_l.
+  iMod (inv_alloc N _ (l ↦ᵢ #1)%I with "Hl") as "#Hinv".
+  rel_arrow.
+  iIntros "!#" (f1 f2) "#Hf".
+  rel_let_l; rel_let_r.
+  iApply bin_log_related_seq'; auto.
+  - iApply (bin_log_related_app with "Hf").
+    iApply bin_log_related_unit.
+  - rel_load_l_atomic;
+      iInv N as "Hl" "Hcl"; iModIntro.
+    iExists #1. iNext. iFrame "Hl". simpl.
+    iIntros "Hl".
+    iMod ("Hcl" with "Hl") as "_".
+    iApply bin_log_related_nat.
+Qed.
+
+(** ** Example 4: "Awkward" refinement *)
+(** Defining the "oneshot" RA *)
+Definition oneshotR := csumR (exclR unitR) (agreeR unitR).
+Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
+Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
+Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
+Proof. solve_inG. Qed.
+
+Definition pending γ `{oneshotG Σ} := own γ (Cinl (Excl ())).
+Definition shot γ `{oneshotG Σ} := own γ (Cinr (to_agree ())).
+Lemma new_pending `{oneshotG Σ} : (|==> ∃ γ, pending γ)%I.
+Proof. by apply own_alloc. Qed.
+Lemma shoot γ `{oneshotG Σ} : pending γ ==∗ shot γ.
+Proof.
+  apply own_update.
+  intros n [f |]; simpl; eauto.
+  destruct f; simpl; try by inversion 1.
+Qed.
+Definition shootN := nroot .@ "shootN".
+Lemma shot_not_pending γ `{oneshotG Σ} :
+  shot γ -∗ pending γ -∗ False.
+Proof.
+  iIntros "Hs Hp".
+  iPoseProof (own_valid_2 with "Hs Hp") as "H".
+  iDestruct "H" as %[].
+Qed.
+(** The actual proof *)
+Definition I `{oneshotG Σ} (γ : gname) (x : loc) : iProp Σ :=
+  (x ↦ᵢ #0 ∗ pending γ ∨ x ↦ᵢ #1 ∗ shot γ)%I.
+Lemma awkwardish `{oneshotG Σ} Δ Γ :
+  {Δ;Γ} ⊨
+    let: "x" := ref #0 in
+    (λ: "f", "f" #();; "x" <- #1;; "f" #();; !"x")
+  ≤log≤
+    (λ: "f", "f" #();; "f" #();; #1)
+  : ((Unit → Unit) → TNat).
+Proof.
+  rel_alloc_l as x "Hx". rel_let_l.
+  iMod new_pending as (γ) "Hpending".
+  iMod (inv_alloc shootN _ (I γ x) with "[Hx Hpending]") as "#Hinv".
+  { iNext; unfold I. iLeft. iFrame. }
+  rel_arrow.
+  iIntros "!#" (f1 f2) "#Hf".  
+  rel_let_l. rel_let_r.
+  iApply bin_log_related_seq'.
+  { iApply bin_log_related_app; [eauto|iApply bin_log_related_unit]. }
+  rel_store_l_atomic.
+  iInv shootN as ">Hs" "Hcl"; unfold I. iModIntro.
+  iDestruct "Hs" as "[[Hx Hpending] | [Hx Hshot]]".
+  (* The shot has been still pending *)
+  - iExists #0. iFrame; iNext. iIntros "Hx".
+    iMod (shoot γ with "Hpending") as "#Hshot".
+    iMod ("Hcl" with "[Hx]") as "_".
+    { iNext. iRight. by iFrame. }
+    rel_seq_l.
+    iApply bin_log_related_seq'.
+    { iApply bin_log_related_app; [eauto|iApply bin_log_related_unit]. }
+    rel_load_l_atomic.
+    iInv shootN as ">Hs" "Hcl"; unfold I. iModIntro.
+    iDestruct "Hs" as "[[Hx Hpending] | [Hx _]]".
+    { (* Impossible! *) iExFalso.
+      by iApply shot_not_pending. }
+    iExists #1. iFrame; iNext. iIntros "Hx".
+    iMod ("Hcl" with "[Hx]") as "_".
+    { iNext. iRight. by iFrame. }
+    iApply bin_log_related_nat.
+  - (* x has already been shot *)
+    iExists #1. iFrame; iNext. iIntros "Hx".
+    iDestruct "Hshot" as "#Hshot".
+    iMod ("Hcl" with "[Hx]") as "_".
+    { iNext. iRight. by iFrame. }
+    rel_seq_l.
+    iApply bin_log_related_seq'.
+    { iApply bin_log_related_app; [eauto|iApply bin_log_related_unit]. }
+    rel_load_l_atomic.
+    iInv shootN as ">Hs" "Hcl"; unfold I. iModIntro.
+    iDestruct "Hs" as "[[Hx Hpending] | [Hx _]]".
+    { (* Impossible! *) iExFalso.
+      by iApply shot_not_pending. }
+    iExists #1. iFrame; iNext. iIntros "Hx".
+    iMod ("Hcl" with "[Hx]") as "_".
+    { iNext. iRight. by iFrame. }
+    iApply bin_log_related_nat.
+Qed.    
+
+End refinements.
+
+Theorem bit_ctx_refinement :
+  ∅ ⊨ bit_bool ≤ctx≤ bit_nat : bitT.
+Proof.
+  eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
+  apply bit_refinement.
+Qed.