Cleaned up examples and added lob recursion example

theories/examples/basics.v

@@ -88,8 +88,8 @@ Definition prog_swap : val := λ: <>,
   let: "c" := start_chan (λ: "c'",
     send "c'" #20;;
     let: "y" := recv "c'" in
-    send "c'" "y") in
-  send "c" #22;;
+    send "c'" ("y" + #2)) in
+  send "c" #20;;
   recv "c" + recv "c".
 
 Definition prog_swap_twice : val := λ: <>,
@@ -189,7 +189,7 @@ Fixpoint prot_lock (n : nat) : iProto Σ :=
 Definition prot_swap : iProto Σ :=
   (<! (x : Z)> MSG #x;
    <?> MSG #20;
-   <?> MSG #x; END)%proto.
+   <?> MSG #(x + 2); END)%proto.
 
 Definition prot_swap_twice : iProto Σ :=
   (<! (x : Z)> MSG #x;

theories/examples/subprotocols.v

 From actris.channel Require Import proofmode proto channel.
 From iris.proofmode Require Import tactics.
-From actris.utils Require Import llist.
-From actris.examples Require Import swap_mapper.
 
-Section basics.
+Section subprotocol_basics.
   Context `{heapG Σ, chanG Σ}.
 
-  Lemma reference_example (l2' : loc) :
-    l2' ↦ #22 -∗
+  Lemma reference_example (l1' : loc) :
+    l1' ↦ #20 -∗
     (<! (l1 l2 : loc)> MSG (#l1, #l2) {{ l1 ↦ #20 ∗ l2 ↦ #22 }}; END) ⊑
-    (<! (l1 : loc)> MSG (#l1, #l2') {{ l1 ↦ #20 }}; END).
-  Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame "Hl1 Hl2'". Qed.
+    (<! (l2 : loc)> MSG (#l1', #l2) {{ l2 ↦ #22 }}; END).
+  Proof. iIntros "Hl1'" (l2) "Hl2". iExists l1', l2. by iFrame "Hl1' Hl2". Qed.
 
   Lemma framing_example (P Q R : iProp Σ) (v w : val) :
     ⊢ ((<!> MSG v {{ P }} ; <?> MSG w {{ Q }}; END)%proto ⊑
@@ -20,49 +18,34 @@ Section basics.
     iIntros "HQ". iFrame "HQ HR". eauto.
   Qed.
 
-  Section program_reuse.
-    Context {T U R : Type}.
-    Context (IT : T -> val -> iProp Σ).
-    Context (ITR : (T * R) -> val -> iProp Σ).
-    Context (IU : U -> val -> iProp Σ).
-    Context (IUR : (U * R) -> val -> iProp Σ).
-    Context (IR : R -> iProp Σ).
-    Context (f : T -> U).
+  Definition prot1_aux (prot : iProto Σ) : iProto Σ :=
+    (<! (x:Z)> MSG #x ; <?> MSG #(x+2) ; prot)%proto.
+  Definition prot2_aux (prot : iProto Σ) : iProto Σ :=
+    (<! (x:Z)> MSG #x ; <! (y:Z)> MSG #y ;
+     <?> MSG #(x+2) ; <?> MSG #(y+2) ; prot)%proto.
 
-    Axiom HIT : ∀ v t r, ITR (t,r) v -∗ IT t v ∗ IR r.
-    Axiom HIU : ∀ v u r, (IU u v ∗ IR r) -∗ IUR (u,r) v.
+  Instance prot1_aux_contractive : Contractive prot1_aux.
+  Proof. solve_proto_contractive. Qed.
+  Instance prot2_aux_contractive : Contractive prot2_aux.
+  Proof. solve_proto_contractive. Qed.
 
-    Lemma example prot prot' :
-      ▷ (prot ⊑ prot') -∗
-           (<! (x : T) (v : val)> MSG v {{ IT x v }};
-           <? (w : val)> MSG w {{ IU (f x) w }}; prot) ⊑
-           (<! (x : T * R) (v : val)> MSG v {{ ITR x v }};
-           <? (w : val)> MSG w {{ IUR (f x.1,x.2) w }}; prot').
-    Proof.
-      iIntros "Hprot".
-      iIntros ([t r] v) "HTR".
-      iDestruct (HIT with "HTR") as "[HT HR]".
-      iExists t,v. iFrame "HT".
-      iModIntro.
-      iIntros (w) "HU". iDestruct (HIU with "[$HR $HU]") as "HUR".
-      iExists w. iFrame "HUR".
-      iModIntro. iApply "Hprot".
-    Qed.
+  Definition prot1 : iProto Σ := fixpoint prot1_aux.
+  Definition prot2 : iProto Σ := fixpoint prot2_aux.
 
-    Lemma mapper_prot_reuse_example :
-      ⊢ mapper_prot IT IU f ⊑ mapper_prot ITR IUR (λ tr, (f tr.1, tr.2)).
-    Proof.
-      iLöb as "IH".
-      iEval (rewrite /mapper_prot).
-      rewrite (fixpoint_unfold (mapper_prot_aux IT _ _)).
-      rewrite (fixpoint_unfold (mapper_prot_aux ITR _ _)).
-      rewrite {1 3}/mapper_prot_aux.
-      rewrite /iProto_choice.
-      iIntros (b). iExists (b).
-      destruct b=> //. iModIntro.
-      iApply example. iApply "IH".
-    Qed.
-
-  End program_reuse.
+  Lemma nonstructural_recursion_example :
+    ⊢ prot1 ⊑ prot2.
+  Proof.
+    iLöb as "IH".
+    iEval (rewrite /prot1 /prot2).
+    do 2 rewrite (fixpoint_unfold prot1_aux).
+    rewrite (fixpoint_unfold prot2_aux).
+    iIntros (x). iExists x. iModIntro.
+    iIntros (y).
+    iApply (iProto_le_trans).
+    { iModIntro. iExists y. iApply iProto_le_refl. }
+    iApply iProto_le_trans; [ iApply iProto_le_base_swap | ].
+    iModIntro. iModIntro. iModIntro.
+    iApply "IH".
+  Qed.
 
-End basics.
+End subprotocol_basics.

[Robbert Krebbers]

All these scopes! %proto%proto even!!!!

I think all such scope annotations in this file can be removed.

[Jonas Kastberg]

Removing %proto from this line gives Error: Unknown interpretation for notation "<! _ .. _ > _".

[Robbert Krebbers]

For Definitions you do need it, but never for the arguments of ↦, ⊑, etc.

[Robbert Krebbers]

Somehow Gitlab put this comment at the wrong place, it was primarily aimed at framing_example.