Skip to content
Snippets Groups Projects
Commit 2e3ca514 authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Jonas Kastberg
Browse files

Remove existential quantifiers in swapping case of `iProto_le`.

parent 2007d5b5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/channel/proto.v
+ 104
− 198
View file @ 2e3ca514
......@@ -245,9 +245,8 @@ Definition iProto_le_pre {Σ V}
| Send, Send => ∀ v p2',
iMsg_car m2 v (Next p2') -∗ ∃ p1', ▷ rec p1' p2' ∗ iMsg_car m1 v (Next p1')
| Recv, Send => ∀ v1 v2 p1' p2',
iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ m1' m2' pt,
▷ rec p1' (<!> m1') ∗ ▷ rec (<?> m2') p2' ∗
iMsg_car m1' v2 (Next pt) ∗ iMsg_car m2' v1 (Next pt)
iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt,
▷ rec p1' (<!> MSG v2; pt) ∗ ▷ rec (<?> MSG v1; pt) p2'
| Send, Recv => False
end.
Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V → iProto Σ V → iProp Σ) :
......@@ -275,29 +274,13 @@ Proof. solve_proper. Qed.
Instance iProto_le_proper {Σ V} : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ V).
Proof. solve_proper. Qed.
Fixpoint iProto_interp_aux {Σ V} (n : nat)
(vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
match n with
| 0 => ∃ p,
⌜ vsl = [] ⌝ ∗
⌜ vsr = [] ⌝ ∗
p ⊑ pl ∗
iProto_dual p ⊑ pr
| S n =>
(∃ vl vsl' m p2',
⌜ vsl = vl :: vsl' ⌝ ∗
(<?> m) ⊑ pr ∗
iMsg_car m vl (Next p2') ∗
iProto_interp_aux n vsl' vsr pl p2') ∨
(∃ vr vsr' m p1',
⌜ vsr = vr :: vsr' ⌝ ∗
(<?> m) ⊑ pl ∗
iMsg_car m vr (Next p1') ∗
iProto_interp_aux n vsl vsr' p1' pr)
Fixpoint iProto_app_recvs {Σ V} (vs : list V) (p : iProto Σ V) : iProto Σ V :=
match vs with
| [] => p
| v :: vs => <?> MSG v; iProto_app_recvs vs p
end.
Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
iProto_interp_aux (length vsl + length vsr) vsl vsr pl pr.
Arguments iProto_interp {_ _} _ _ _%proto _%proto : simpl nomatch.
∃ p, iProto_app_recvs vsr p ⊑ pl ∗ iProto_app_recvs vsl (iProto_dual p) ⊑ pr.
Record proto_name := ProtName { proto_l_name : gname; proto_r_name : gname }.
Instance proto_name_inhabited : Inhabited proto_name :=
......@@ -564,9 +547,8 @@ Section proto.
Proof. rewrite iProto_le_unfold. iIntros "H". iRight. auto 10. Qed.
Lemma iProto_le_swap m1 m2 :
(∀ v1 v2 p1' p2',
iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ m1' m2' pt,
▷ (p1' ⊑ <!> m1') ∗ ▷ ((<?> m2') ⊑ p2') ∗
iMsg_car m1' v2 (Next pt) ∗ iMsg_car m2' v1 (Next pt)) -∗
iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt,
▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2')) -∗
(<?> m1) ⊑ (<!> m2).
Proof. rewrite iProto_le_unfold. iIntros "H". iRight. auto 10. Qed.
......@@ -592,9 +574,8 @@ Section proto.
iMsg_car m2 v (Next p2') -∗ ∃ p1',
▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1')
| Recv => ∀ v1 v2 p1' p2',
iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ m1' m2' pt,
▷ (p1' ⊑ <!> m1') ∗ ▷ ((<?> m2') ⊑ p2') ∗
iMsg_car m1' v2 (Next pt) ∗ iMsg_car m2' v1 (Next pt)
iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt,
▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2')
end.
Proof.
rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
......@@ -621,9 +602,8 @@ Section proto.
Qed.
Lemma iProto_le_recv_send_inv m1 m2 v1 v2 p1' p2' :
(<?> m1) ⊑ (<!> m2) -∗
iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ m1' m2' pt,
▷ (p1' ⊑ <!> m1') ∗ ▷ ((<?> m2') ⊑ p2') ∗
iMsg_car m1' v2 (Next pt) ∗ iMsg_car m2' v1 (Next pt).
iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt,
▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2').
Proof.
iIntros "H Hm1 Hm2". iDestruct (iProto_le_send_inv with "H") as (a m1') "[Hm H]".
iDestruct (iProto_message_equivI with "Hm") as (<-) "{Hm} #Hm".
......@@ -677,14 +657,14 @@ Section proto.
iExists p1'. iIntros "{$Hm1} !>". by iApply ("IH" with "Hle'").
* iApply iProto_le_swap. iIntros (v1 v3 p1' p3') "Hm1 Hm3".
iDestruct ("H2" with "Hm3") as (p2') "[Hle Hm2]".
iDestruct ("H1" with "Hm1 Hm2") as (m1' m2' pt) "(Hp1' & Hp2' & Hm)".
iExists m1', m2', pt. iIntros "{$Hp1' $Hm} !>". by iApply ("IH" with "Hp2'").
iDestruct ("H1" with "Hm1 Hm2") as (pt) "[Hp1' Hp2']".
iExists pt. iIntros "{$Hp1'} !>". by iApply ("IH" with "Hp2'").
+ iDestruct (iProto_le_recv_inv with "H1") as (m1) "[Hp1 H1]".
iRewrite "Hp1"; clear p1. iApply iProto_le_swap.
iIntros (v1 v3 p1' p3') "Hm1 Hm3".
iDestruct ("H1" with "Hm1") as (p2') "[Hle Hm2]".
iDestruct ("H2" with "Hm2 Hm3") as (m2' m3' pt) "(Hp2' & Hp3' & Hm)".
iExists m2', m3', pt. iIntros "{$Hp3' $Hm} !>". by iApply ("IH" with "Hle").
iDestruct ("H2" with "Hm2 Hm3") as (pt) "[Hp2' Hp3']".
iExists pt. iIntros "{$Hp3'} !>". by iApply ("IH" with "Hle").
- iDestruct (iProto_le_recv_inv with "H2") as (m2) "[Hp2 H3]".
iRewrite "Hp2" in "H1".
iDestruct (iProto_le_recv_inv with "H1") as (m1) "[Hp1 H2]".
......@@ -694,28 +674,6 @@ Section proto.
iExists p3'. iIntros "{$Hm3} !>". by iApply ("IH" with "Hle").
Qed.
Lemma iProto_le_base a v P p1 p2 :
▷ (p1 ⊑ p2) -∗
(<a> MSG v {{ P }}; p1) ⊑ (<a> MSG v {{ P }}; p2).
Proof.
rewrite iMsg_base_eq. iIntros "H". destruct a.
- iApply iProto_le_send. iIntros (v' p') "(->&Hp&$)".
iExists p1. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
- iApply iProto_le_recv. iIntros (v' p') "(->&Hp&$)".
iExists p2. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
Qed.
Lemma iProto_le_base_swap v1 v2 P1 P2 p :
⊢ (<?> MSG v1 {{ P1 }}; <!> MSG v2 {{ P2 }}; p)
⊑ (<!> MSG v2 {{ P2 }}; <?> MSG v1 {{ P1 }}; p).
Proof.
rewrite iMsg_base_eq. iApply iProto_le_swap.
iIntros (v1' v2' p1' p2') "/= (->&#Hp1&HP1) (->&#Hp2&HP2)". iExists _, _, p.
iSplitR; [iIntros "!>"; iRewrite -"Hp1"; iApply iProto_le_refl|].
iSplitR; [iIntros "!>"; iRewrite -"Hp2"; iApply iProto_le_refl|].
simpl; auto with iFrame.
Qed.
Lemma iProto_le_payload_elim_l a m v P p :
(P -∗ (<?> MSG v; p) ⊑ (<a> m)) -∗
(<?> MSG v {{ P }}; p) ⊑ (<a> m).
......@@ -857,6 +815,28 @@ Section proto.
iApply iProto_le_trans; [|by iApply iProto_le_exist_intro_r]. iApply IH.
Qed.
Lemma iProto_le_base a v P p1 p2 :
▷ (p1 ⊑ p2) -∗
(<a> MSG v {{ P }}; p1) ⊑ (<a> MSG v {{ P }}; p2).
Proof.
rewrite iMsg_base_eq. iIntros "H". destruct a.
- iApply iProto_le_send. iIntros (v' p') "(->&Hp&$)".
iExists p1. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
- iApply iProto_le_recv. iIntros (v' p') "(->&Hp&$)".
iExists p2. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
Qed.
Lemma iProto_le_base_swap v1 v2 P1 P2 p :
⊢ (<?> MSG v1 {{ P1 }}; <!> MSG v2 {{ P2 }}; p)
⊑ (<!> MSG v2 {{ P2 }}; <?> MSG v1 {{ P1 }}; p).
Proof.
rewrite {1 3}iMsg_base_eq. iApply iProto_le_swap.
iIntros (v1' v2' p1' p2') "/= (->&#Hp1&HP1) (->&#Hp2&HP2)". iExists p.
iSplitL "HP2".
- iIntros "!>". iRewrite -"Hp1". by iApply iProto_le_payload_intro_l.
- iIntros "!>". iRewrite -"Hp2". by iApply iProto_le_payload_intro_r.
Qed.
Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
Proof.
iIntros "H". iLöb as "IH" forall (p1 p2).
......@@ -871,14 +851,13 @@ Section proto.
iDestruct ("H" with "Hm1") as (p2') "[H Hm2]".
iDestruct ("IH" with "H") as "H". iExists (iProto_dual p2').
iSplitL "H"; [iIntros "!>"; by iRewrite "Hp1d"|]. simpl; auto.
+ iApply iProto_le_swap. iIntros (v1 p1d v2 p2d).
+ iApply iProto_le_swap. iIntros (v1 v2 p1d p2d).
iDestruct 1 as (p1') "[Hm1 #Hp1d]". iDestruct 1 as (p2') "[Hm2 #Hp2d]".
iDestruct ("H" with "Hm2 Hm1") as (m1' m2' pt) "(H1 & H2 & Hm1 & Hm2)".
iDestruct ("H" with "Hm2 Hm1") as (pt) "[H1 H2]".
iDestruct ("IH" with "H1") as "H1". iDestruct ("IH" with "H2") as "H2 {IH}".
rewrite !iProto_dual_message /=. iExists _, _, (iProto_dual pt).
iSplitL "H2"; [iIntros "!>"; by iRewrite "Hp1d"|].
iSplitL "H1"; [iIntros "!>"; by iRewrite "Hp2d"|].
iSplitL "Hm2"; simpl; auto.
rewrite !iProto_dual_message /=. iExists (iProto_dual pt). iSplitL "H2".
* iIntros "!>". iRewrite "Hp1d". by rewrite -iMsg_dual_base.
* iIntros "!>". iRewrite "Hp2d". by rewrite -iMsg_dual_base.
- iDestruct (iProto_le_recv_inv with "H") as (m2) "[Hp2 H]".
iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message /=).
iApply iProto_le_send. iIntros (v p2d).
......@@ -938,13 +917,14 @@ Section proto.
+ iApply iProto_le_swap. iIntros (v1 v2 p13 p24).
iDestruct 1 as (p1') "[Hm1 #Hp13]". iDestruct 1 as (p2') "[Hm2 #Hp24]".
iSpecialize ("H1" with "Hm1 Hm2").
iDestruct "H1" as (m1' m2' pt) "(H1 & H1' & Hm1 & Hm2)".
iExists (m1' <++> p3)%msg, (m2' <++> p3)%msg, (pt <++> p3).
rewrite -!iProto_app_message /=. iSplitL "H1".
{ iIntros "!>". iRewrite "Hp13". iApply ("IH" with "H1"). iApply iProto_le_refl. }
iSplitL "H2 H1'".
{ iIntros "!>". iRewrite "Hp24". iApply ("IH" with "H1' H2"). }
iSplitL "Hm1"; auto.
iDestruct "H1" as (pt) "[H1 H1']".
iExists (pt <++> p3). iSplitL "H1".
* iIntros "!>". iRewrite "Hp13".
rewrite /= -iMsg_app_base -iProto_app_message.
iApply ("IH" with "H1"). iApply iProto_le_refl.
* iIntros "!>". iRewrite "Hp24".
rewrite /= -iMsg_app_base -iProto_app_message.
iApply ("IH" with "H1' H2").
- iDestruct (iProto_le_recv_inv with "H1") as (m1) "[Hp1 H1]".
iRewrite "Hp1"; clear p1. rewrite !iProto_app_message. iApply iProto_le_recv.
iIntros (v p13). iDestruct 1 as (p1') "[Hm1 #Hp13]".
......@@ -954,12 +934,12 @@ Section proto.
Qed.
(** ** Lemmas about the auxiliary definitions and invariants *)
Global Instance iProto_interp_aux_ne n vsl vsr :
NonExpansive2 (iProto_interp_aux (Σ:=Σ) (V:=V) n vsl vsr).
Proof. revert vsl vsr. induction n; solve_proper. Qed.
Global Instance iProto_interp_aux_proper n vsl vsr :
Proper ((≡) ==> (≡) ==> (≡)) (iProto_interp_aux (Σ:=Σ) (V:=V) n vsl vsr).
Proof. apply (ne_proper_2 _). Qed.
Global Instance iProto_app_recvs_ne vs :
NonExpansive (iProto_app_recvs (Σ:=Σ) (V:=V) vs).
Proof. induction vs; solve_proper. Qed.
Global Instance iProto_app_recvs_proper vs :
Proper ((≡) ==> (≡)) (iProto_app_recvs (Σ:=Σ) (V:=V) vs).
Proof. induction vs; solve_proper. Qed.
Global Instance iProto_interp_ne vsl vsr :
NonExpansive2 (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
Proof. solve_proper. Qed.
......@@ -996,77 +976,21 @@ Section proto.
(φ1 ↔ φ2) → (φ1 → φ2 → P1 ⊣⊢ P2) → (⌜φ1⌝ ∗ P1) ⊣⊢ (⌜φ2⌝ ∗ P2).
Proof. intros -> HP. iSplit; iDestruct 1 as (Hϕ) "H"; rewrite HP; auto. Qed.
Lemma iProto_interp_unfold vsl vsr pl pr :
iProto_interp vsl vsr pl pr ⊣⊢
(∃ p,
⌜ vsl = [] ⌝ ∗
⌜ vsr = [] ⌝ ∗
p ⊑ pl ∗
iProto_dual p ⊑ pr) ∨
(∃ vl vsl' m pr',
⌜ vsl = vl :: vsl' ⌝ ∗
(<?> m) ⊑ pr ∗
iMsg_car m vl (Next pr') ∗
iProto_interp vsl' vsr pl pr') ∨
(∃ vr vsr' m pl',
⌜ vsr = vr :: vsr' ⌝ ∗
(<?> m) ⊑ pl ∗
iMsg_car m vr (Next pl') ∗
iProto_interp vsl vsr' pl' pr).
Proof.
rewrite {1}/iProto_interp. destruct vsl as [|vl vsl]; simpl.
- destruct vsr as [|vr vsr]; simpl.
+ iSplit; first by auto.
iDestruct 1 as "[H | [H | H]]"; first by auto.
* iDestruct "H" as (? ? ? ? [=]) "_".
* iDestruct "H" as (? ? ? ? [=]) "_".
+ symmetry. apply false_disj_cong.
{ iDestruct 1 as (? _ [=]) "_". }
repeat first [apply pure_sep_cong; intros; simplify_eq/= | f_equiv];
by rewrite ?Nat.add_succ_r.
- symmetry. apply false_disj_cong.
{ iDestruct 1 as (? [=]) "_". }
repeat first [apply pure_sep_cong; intros; simplify_eq/= | f_equiv];
by rewrite ?Nat.add_succ_r.
Qed.
Lemma iProto_interp_nil p : ⊢ iProto_interp [] [] p (iProto_dual p).
Proof.
rewrite iProto_interp_unfold. iLeft. iExists p. do 2 (iSplit; [done|]).
iSplitL; iApply iProto_le_refl.
Qed.
Proof. iExists p; simpl. iSplitL; iApply iProto_le_refl. Qed.
Lemma iProto_interp_flip vsl vsr pl pr :
iProto_interp vsl vsr pl pr -∗ iProto_interp vsr vsl pr pl.
Proof.
remember (length vsl + length vsr) as n eqn:Hn.
iInduction (lt_wf n) as [n _] "IH" forall (vsl vsr pl pr Hn); subst.
rewrite !iProto_interp_unfold. iIntros "[H|[H|H]]".
- iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
iLeft. iExists (iProto_dual p). rewrite involutive. iFrame; auto.
- iDestruct "H" as (vl vsl' m' pr' ->) "(Hpr & Hm' & H)".
iRight; iRight. iExists vl, vsl', m', pr'. iSplit; [done|]; iFrame.
iApply ("IH" with "[%] [//] H"); simpl; lia.
- iDestruct "H" as (vr vsr' m' pl' ->) "(Hpl & Hm' & H)".
iRight; iLeft. iExists vr, vsr', m', pl'. iSplit; [done|]; iFrame.
iApply ("IH" with "[%] [//] H"); simpl; lia.
iDestruct 1 as (p) "[Hp Hdp]". iExists (iProto_dual p).
rewrite (involutive iProto_dual). iFrame.
Qed.
Lemma iProto_interp_le_l vsl vsr pl pl' pr :
iProto_interp vsl vsr pl pr -∗ pl ⊑ pl' -∗ iProto_interp vsl vsr pl' pr.
Proof.
remember (length vsl + length vsr) as n eqn:Hn.
iInduction (lt_wf n) as [n _] "IH" forall (vsl vsr pl pr Hn); subst.
rewrite !iProto_interp_unfold. iIntros "[H|[H|H]] Hle".
- iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
iLeft. iExists p. do 2 (iSplit; [done|]). iFrame "Hp'".
by iApply (iProto_le_trans with "Hp").
- iDestruct "H" as (vl vsl' m' pr' ->) "(Hpr & Hm' & H)".
iRight; iLeft. iExists vl, vsl', m', pr'. iSplit; [done|]; iFrame.
iApply ("IH" with "[%] [//] H Hle"); simpl; lia.
- iClear "IH". iDestruct "H" as (vr vsr' m' pl'' ->) "(Hpl & Hm' & H)".
iRight; iRight. iExists vr, vsr', m', pl''. iSplit; [done|]; iFrame.
by iApply (iProto_le_trans with "Hpl").
iDestruct 1 as (p) "[Hp Hdp]". iIntros "Hle". iExists p.
iFrame "Hdp". by iApply (iProto_le_trans with "Hp").
Qed.
Lemma iProto_interp_le_r vsl vsr pl pr pr' :
iProto_interp vsl vsr pl pr -∗ pr ⊑ pr' -∗ iProto_interp vsl vsr pl pr'.
......@@ -1075,62 +999,42 @@ Section proto.
iApply (iProto_interp_le_l with "[H] Hle"). by iApply iProto_interp_flip.
Qed.
Lemma iProto_interp_send vl ml vsl vsr pl pr pl' :
iProto_interp vsl vsr pl pr -∗
pl ⊑ (<!> ml) -∗
Lemma iProto_interp_send vl ml vsl vsr pr pl' :
iProto_interp vsl vsr (<!> ml) pr -∗
iMsg_car ml vl (Next pl') -∗
▷^(length vsr) iProto_interp (vsl ++ [vl]) vsr pl' pr.
Proof.
iIntros "H Hle". iDestruct (iProto_interp_le_l with "H Hle") as "H".
clear pl. iIntros "Hml". remember (length vsl + length vsr) as n eqn:Hn.
iInduction (lt_wf n) as [n _] "IH" forall (ml vsl vsr pr pl' Hn); subst.
rewrite {1}iProto_interp_unfold. iDestruct "H" as "[H|[H|H]]".
- iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
iDestruct (iProto_le_dual with "Hp") as "Hp".
iDestruct (iProto_le_trans with "Hp Hp'") as "Hp".
rewrite iProto_dual_message /=.
iApply iProto_interp_unfold. iRight; iLeft.
iExists vl, [], _, (iProto_dual pl'). iSplit; [done|]. iFrame "Hp"; simpl.
iSplitL; [by auto|]. iApply iProto_interp_nil.
- iDestruct "H" as (vl' vsl' m' pr' ->) "(Hpr & Hm' & H)".
iDestruct ("IH" with "[%] [//] H Hml") as "H"; [simpl; lia|].
iNext. iApply (iProto_interp_le_r with "[-Hpr] Hpr"); clear pr.
iApply iProto_interp_unfold. iRight; iLeft.
iExists vl', (vsl' ++ [vl]), m', pr'. iFrame.
iSplit; [done|]. iApply iProto_le_refl.
- iDestruct "H" as (vr' vsr' m' pl'' ->) "(Hle & Hml' & H) /=".
iDestruct (iProto_le_send_inv with "Hle") as (a ml') "[Hm Hle]".
iDestruct (iProto_message_equivI with "Hm") as (<-) "Hm".
iSpecialize ("Hle" with "[Hml' Hm] Hml").
{ by iRewrite ("Hm" $! vr' (Next pl'')) in "Hml'". }
iDestruct "Hle" as (m1 m2 pt) "(Hpl'' & Hpl' & Hm1 & Hm2)". iIntros "!>".
iDestruct (iProto_interp_le_l with "H Hpl''") as "H".
iDestruct ("IH" with "[%] [//] H Hm1") as "H"; [simpl; lia|..].
iNext. iApply iProto_interp_unfold. iRight; iRight.
iExists vr', vsr', _, pt. iSplit; [done|]. by iFrame.
Qed.
Lemma iProto_interp_recv vl vsl vsr pl pr mr :
iProto_interp (vl :: vsl) vsr pl pr -∗
pr ⊑ (<?> mr) -∗
iDestruct 1 as (p) "[Hp Hdp] /="; iIntros "Hml".
iDestruct (iProto_le_trans _ _ (<!> MSG vl; pl') with "Hp [Hml]") as "Hp".
{ iApply iProto_le_send. rewrite iMsg_base_eq. iIntros (v' p') "(->&Hp&_) /=".
iExists p'. iSplitR; [iApply iProto_le_refl|]. by iRewrite -"Hp". }
iInduction vsr as [|vr vsr] "IH" forall (pl'); simpl.
{ iExists pl'; simpl. iSplitR; [iApply iProto_le_refl|].
iApply (iProto_le_trans with "[Hp] Hdp").
iInduction vsl as [|vl' vsl] "IH"; simpl.
{ iApply iProto_le_dual_r. rewrite iProto_dual_message iMsg_dual_base /=.
by rewrite involutive. }
iApply iProto_le_base; iIntros "!>". by iApply "IH". }
iDestruct (iProto_le_recv_send_inv _ _ vr vl
(iProto_app_recvs vsr p) pl' with "Hp [] []") as (p') "[H1 H2]";
[rewrite iMsg_base_eq; by auto..|].
iIntros "!>". iSpecialize ("IH" with "Hdp H1"). iIntros "!>".
iDestruct "IH" as (p'') "[Hp'' Hdp'']". iExists p''. iFrame "Hdp''".
iApply (iProto_le_trans with "[Hp''] H2"); simpl. by iApply iProto_le_base.
Qed.
Lemma iProto_interp_recv vl vsl vsr pl mr :
iProto_interp (vl :: vsl) vsr pl (<?> mr) -∗
∃ pr, iMsg_car mr vl (Next pr) ∗ ▷ iProto_interp vsl vsr pl pr.
Proof.
iIntros "H Hle". iDestruct (iProto_interp_le_r with "H Hle") as "H".
clear pr. remember (length vsr) as n eqn:Hn.
iInduction (lt_wf n) as [n _] "IH" forall (vsr pl Hn); subst.
rewrite !iProto_interp_unfold. iDestruct "H" as "[H|[H|H]]".
- iClear "IH". iDestruct "H" as (p [=]) "_".
- iClear "IH". iDestruct "H" as (vl' vsl' m' pr' [= -> ->]) "(Hpr & Hm' & H)".
iDestruct (iProto_le_recv_inv with "Hpr") as (m'') "[Hm Hpr]".
iDestruct (iProto_message_equivI with "Hm") as (_) "{Hm} #Hm".
iDestruct ("Hpr" $! vl' pr' with "[Hm']") as (pr'') "[Hler Hpr]".
{ by iRewrite -("Hm" $! vl' (Next pr')). }
iExists pr''. iFrame "Hpr".
by iApply (iProto_interp_le_r with "H").
- iDestruct "H" as (vr vsr' m' pl'' ->) "(Hpl & Hm' & H)".
iDestruct ("IH" with "[%] [//] H") as (pr) "[Hm H]"; [simpl; lia|].
iExists pr. iFrame "Hm".
iApply iProto_interp_unfold. iRight; iRight. eauto 20 with iFrame.
iDestruct 1 as (p) "[Hp Hdp] /=".
iDestruct (iProto_le_recv_inv with "Hdp") as (m) "[#Hm Hpr]".
iDestruct (iProto_message_equivI with "Hm") as (_) "{Hm} #Hm".
iDestruct ("Hpr" $! vl (iProto_app_recvs vsl (iProto_dual p)) with "[]")
as (pr'') "[Hler Hpr]".
{ iRewrite -("Hm" $! vl (Next (iProto_app_recvs vsl (iProto_dual p)))).
rewrite iMsg_base_eq; auto. }
iExists pr''. iIntros "{$Hpr} !>". iExists p. iFrame.
Qed.
Global Instance iProto_own_ne γ s : NonExpansive (iProto_own γ s).
......@@ -1172,8 +1076,8 @@ Section proto.
iDestruct (iProto_own_auth_agree with "H●l H◯") as "#Hp".
iAssert (▷ (pl ⊑ <!> m))%I
with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
iDestruct (iProto_interp_send with "Hinterp Hle [Hm]") as "Hinterp".
{ simpl. auto. }
iDestruct (iProto_interp_le_l with "Hinterp Hle") as "Hinterp".
iDestruct (iProto_interp_send with "Hinterp [Hm //]") as "Hinterp".
iMod (iProto_own_auth_update _ _ _ _ p with "H●l H◯") as "[H●l H◯]".
iIntros "!>". iSplitR "H◯".
- iIntros "!>". iExists p, pr. iFrame.
......@@ -1193,8 +1097,8 @@ Section proto.
iAssert (▷ (pr ⊑ <!> m))%I
with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
iDestruct (iProto_interp_flip with "Hinterp") as "Hinterp".
iDestruct (iProto_interp_send with "Hinterp Hle [Hm]") as "Hinterp".
{ simpl. auto. }
iDestruct (iProto_interp_le_l with "Hinterp Hle") as "Hinterp".
iDestruct (iProto_interp_send with "Hinterp [Hm //]") as "Hinterp".
iMod (iProto_own_auth_update _ _ _ _ p with "H●r H◯") as "[H●r H◯]".
iIntros "!>". iSplitR "H◯".
- iIntros "!>". iExists pl, p. iFrame. by iApply iProto_interp_flip.
......@@ -1212,9 +1116,10 @@ Section proto.
iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
iDestruct 1 as (p) "[Hle H◯]".
iDestruct (iProto_own_auth_agree with "H●l H◯") as "#Hp".
iDestruct (iProto_interp_le_l with "Hinterp [Hle]") as "Hinterp".
{ iIntros "!>". by iRewrite "Hp". }
iDestruct (iProto_interp_flip with "Hinterp") as "Hinterp".
iDestruct (iProto_interp_recv with "Hinterp [Hle]") as (q) "[Hm Hinterp]".
{ iNext. by iRewrite "Hp". }
iDestruct (iProto_interp_recv with "Hinterp") as (q) "[Hm Hinterp]".
iMod (iProto_own_auth_update _ _ _ _ q with "H●l H◯") as "[H●l H◯]".
iIntros "!> !> /=". iExists q. iFrame "Hm". iSplitR "H◯".
- iExists q, pr. iFrame. by iApply iProto_interp_flip.
......@@ -1232,8 +1137,9 @@ Section proto.
iDestruct 1 as (pl pr) "(H●l & H●r & Hinterp)".
iDestruct 1 as (p) "[Hle H◯]".
iDestruct (iProto_own_auth_agree with "H●r H◯") as "#Hp".
iDestruct (iProto_interp_recv with "Hinterp [Hle]") as (q) "[Hm Hinterp]".
{ iNext. by iRewrite "Hp". }
iDestruct (iProto_interp_le_r with "Hinterp [Hle]") as "Hinterp".
{ iIntros "!>". by iRewrite "Hp". }
iDestruct (iProto_interp_recv with "Hinterp") as (q) "[Hm Hinterp]".
iMod (iProto_own_auth_update _ _ _ _ q with "H●r H◯") as "[H●r H◯]".
iIntros "!> !> /=". iExists q. iFrame "Hm". iSplitR "H◯".
- iExists pl, q. iFrame.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment