Commit 5cb675da authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'robbert/model'

parents 36f40743 270596d4
Pipeline #25956 canceled with stage
in 1 minute and 15 seconds
......@@ -5,6 +5,7 @@ theories/utils/llist.v
theories/utils/compare.v
theories/utils/contribution.v
theories/utils/group.v
theories/utils/cofe_solver_2.v
theories/channel/proto_model.v
theories/channel/proto.v
theories/channel/channel.v
......
......@@ -174,6 +174,21 @@ Section channel.
by apply iProto_message_proper=> /= -[].
Qed.
Lemma iProto_le_branch a P1 P2 p1 p2 p1' p2' :
(P1 - P1 iProto_le p1 p1') (P2 - P2 iProto_le p2 p2') -
iProto_le (iProto_branch a P1 P2 p1 p2) (iProto_branch a P1 P2 p1' p2').
Proof.
iIntros "H". rewrite /iProto_branch. destruct a.
- iApply iProto_le_send'; iIntros "!>" (b) "HP /=".
iExists b; iSplit; [done|]. destruct b.
+ iDestruct "H" as "[H _]". by iApply "H".
+ iDestruct "H" as "[_ H]". by iApply "H".
- iApply iProto_le_recv'; iIntros "!>" (b) "HP /=".
iExists b; iSplit; [done|]. destruct b.
+ iDestruct "H" as "[H _]". by iApply "H".
+ iDestruct "H" as "[_ H]". by iApply "H".
Qed.
(** ** Specifications of [send] and [recv] *)
Lemma new_chan_spec p :
{{{ True }}}
......
......@@ -39,16 +39,16 @@ Instance action_dual_if_true_recv : ActionDualIf true Recv Send := eq_refl.
Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
(pas : list (bool * iProto Σ)) (q : iProto Σ) :=
proto_normalize :
q (iProto_dual_if d p <++>
foldr (iProto_app curry iProto_dual_if) END pas)%proto.
iProto_le (iProto_dual_if d p <++>
foldr (iProto_app curry iProto_dual_if) END pas)%proto q.
Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
Arguments ProtoNormalize {_} _ _%proto _%proto _%proto.
Class ProtoContNormalize {Σ TT} (d : bool) (pc : TT val * iProp Σ * iProto Σ)
(pas : list (bool * iProto Σ)) (qc : TT val * iProp Σ * iProto Σ) :=
proto_cont_normalize x :
(qc x).1.1 = (pc x).1.1
(qc x).1.2 (pc x).1.2
(pc x).1.1 = (qc x).1.1
(pc x).1.2 (qc x).1.2
ProtoNormalize d ((pc x).2) pas ((qc x).2).
Hint Mode ProtoContNormalize ! ! ! ! ! - : typeclass_instances.
......@@ -61,27 +61,27 @@ Section classes.
Implicit Types TT : tele.
Lemma proto_unfold_eq p1 p2 : p1 p2 ProtoUnfold p1 p2.
Proof. rewrite /ProtoNormalize=> Hp d pas q ->. by rewrite Hp. Qed.
Proof. rewrite /ProtoNormalize=> Hp d pas q. by rewrite Hp. Qed.
Global Instance proto_normalize_done p : ProtoNormalize false p [] p | 0.
Proof. by rewrite /ProtoNormalize /= right_id. Qed.
Proof. rewrite /ProtoNormalize /= right_id. iApply iProto_le_refl. Qed.
Global Instance proto_normalize_done_dual p :
ProtoNormalize true p [] (iProto_dual p) | 0.
Proof. by rewrite /ProtoNormalize /= right_id. Qed.
Proof. rewrite /ProtoNormalize /= right_id. iApply iProto_le_refl. Qed.
Global Instance proto_normalize_done_dual_end :
ProtoNormalize (Σ:=Σ) true END [] END | 0.
Proof. by rewrite /ProtoNormalize /= right_id iProto_dual_end. Qed.
Proof. rewrite /ProtoNormalize /= right_id iProto_dual_end. iApply iProto_le_refl. Qed.
Global Instance proto_normalize_dual d p pas q :
ProtoNormalize (negb d) p pas q
ProtoNormalize d (iProto_dual p) pas q.
Proof. rewrite /ProtoNormalize=> ->. by destruct d; rewrite /= ?involutive. Qed.
Proof. rewrite /ProtoNormalize. by destruct d; rewrite /= ?involutive. Qed.
Global Instance proto_normalize_app_l d p1 p2 pas q :
ProtoNormalize d p1 ((d,p2) :: pas) q
ProtoNormalize d (p1 <++> p2) pas q.
Proof.
rewrite /ProtoNormalize=> -> /=. rewrite assoc.
rewrite /ProtoNormalize /=. rewrite assoc.
by destruct d; by rewrite /= ?iProto_dual_app.
Qed.
......@@ -89,19 +89,25 @@ Section classes.
ProtoNormalize d p pas q
ProtoNormalize d' END ((d,p) :: pas) q | 0.
Proof.
rewrite /ProtoNormalize=> -> /=.
rewrite /ProtoNormalize /=.
destruct d'; by rewrite /= ?iProto_dual_end left_id.
Qed.
Global Instance proto_normalize_app_r d p1 p2 pas q :
ProtoNormalize d p2 pas q
ProtoNormalize false p1 ((d,p2) :: pas) (p1 <++> q) | 0.
Proof. by rewrite /ProtoNormalize=> -> /=. Qed.
Proof.
rewrite /ProtoNormalize /= => H.
iApply iProto_le_app; [iApply iProto_le_refl|done].
Qed.
Global Instance proto_normalize_app_r_dual d p1 p2 pas q :
ProtoNormalize d p2 pas q
ProtoNormalize true p1 ((d,p2) :: pas) (iProto_dual p1 <++> q) | 0.
Proof. by rewrite /ProtoNormalize=> -> /=. Qed.
Proof.
rewrite /ProtoNormalize /= => H.
iApply iProto_le_app; [iApply iProto_le_refl|done].
Qed.
Global Instance proto_cont_normalize_O d v P p q pas :
ProtoNormalize d p pas q
......@@ -127,10 +133,52 @@ Section classes.
Proof.
rewrite /ActionDualIf /ProtoContNormalize /ProtoNormalize=> -> H.
destruct d; simpl.
- rewrite iProto_dual_message iProto_app_message.
apply iProto_message_proper; apply tforall_forall=> x /=; apply H.
- rewrite iProto_app_message.
apply iProto_message_proper; apply tforall_forall=> x /=; apply H.
- rewrite iProto_dual_message iProto_app_message. destruct a1; simpl.
+ iApply iProto_le_recv; iIntros (x) "/= Hpc". iExists x.
destruct (H x) as (-> & -> & Hle). iSplit; [done|]. by iFrame "Hpc".
+ iApply iProto_le_send; iIntros (x) "/= Hpc". iExists x.
destruct (H x) as (-> & -> & Hle). iSplit; [done|]. by iFrame "Hpc".
- rewrite iProto_app_message. destruct a1; simpl.
+ iApply iProto_le_send; iIntros (x) "/= Hpc". iExists x.
destruct (H x) as (-> & -> & Hle). iSplit; [done|]. by iFrame "Hpc".
+ iApply iProto_le_recv; iIntros (x) "/= Hpc". iExists x.
destruct (H x) as (-> & -> & Hle). iSplit; [done|]. by iFrame "Hpc".
Qed.
Global Instance proto_normalize_swap {TT1 TT2} d a1
(pc1 : TT1 val * iProp Σ * iProto Σ)
(vP1 : TT1 -t> val * iProp Σ) (vP2 : TT2 -t> val * iProp Σ)
(pc12 : TT1 -t> TT2 -t> iProto Σ)
(pc2 : TT2 -t> val * iProp Σ * iProto Σ) pas :
ActionDualIf d a1 Recv
ProtoContNormalize d pc1 pas (λ.. x1,
(tele_app vP1 x1, iProto_message Send (λ.. x2,
(tele_app vP2 x2, tele_app (tele_app pc12 x1) x2))))
(.. x2, TCEq (tele_app vP2 x2, iProto_message Recv (λ.. x1,
(tele_app vP1 x1, tele_app (tele_app pc12 x1) x2)))
(tele_app pc2 x2))
ProtoNormalize d (iProto_message a1 pc1) pas
(iProto_message Send (tele_app pc2)).
Proof.
(** TODO: This proof contains twice the same subproof. Refactor. *)
rewrite /ActionDualIf /ProtoContNormalize /ProtoNormalize.
rewrite tforall_forall=> ? Hpc1 Hpc2. destruct d, a1; simplify_eq/=.
- rewrite iProto_dual_message iProto_app_message /=.
iApply iProto_le_swap. iIntros (x1 x2) "/= Hpc1 Hpc2 !>".
move: (Hpc1 x1); rewrite {Hpc1} !tele_app_bind /=; intros (->&->&Hpc).
move: (Hpc2 x2); rewrite {Hpc2} TCEq_eq; intros Hpc2.
iExists TT2, TT1, (λ.. x2, (tele_app vP2 x2, tele_app (tele_app pc12 x1) x2)),
(λ.. x1, (tele_app vP1 x1, tele_app (tele_app pc12 x1) x2)), x2, x1.
rewrite /= !tele_app_bind /= -!Hpc2 /=. do 2 (iSplit; [done|]). iFrame.
iSplitR; [done|]. iSplitR; [iApply iProto_le_refl|]. done.
- rewrite iProto_app_message /=.
iApply iProto_le_swap. iIntros (x1 x2) "/= Hpc1 Hpc2 !>".
move: (Hpc1 x1); rewrite {Hpc1} !tele_app_bind /=; intros (->&->&Hpc).
move: (Hpc2 x2); rewrite {Hpc2} TCEq_eq; intros Hpc2.
iExists TT2, TT1, (λ.. x2, (tele_app vP2 x2, tele_app (tele_app pc12 x1) x2)),
(λ.. x1, (tele_app vP1 x1, tele_app (tele_app pc12 x1) x2)), x2, x1.
rewrite /= !tele_app_bind /= -!Hpc2 /=. do 2 (iSplit; [done|]). iFrame.
iSplitR; [done|]. iSplitR; [iApply iProto_le_refl|]. done.
Qed.
Global Instance proto_normalize_branch d a1 a2 P1 P2 p1 p2 q1 q2 pas :
......@@ -139,8 +187,10 @@ Section classes.
ProtoNormalize d (iProto_branch a1 P1 P2 p1 p2) pas
(iProto_branch a2 P1 P2 q1 q2).
Proof.
rewrite /ActionDualIf /ProtoNormalize=> -> -> ->.
destruct d; by rewrite /= -?iProto_app_branch -?iProto_dual_branch.
rewrite /ActionDualIf /ProtoNormalize=> -> H1 H2. destruct d; simpl.
- rewrite !iProto_dual_branch !iProto_app_branch.
iApply iProto_le_branch; iSplit; by iIntros "!> $".
- rewrite !iProto_app_branch. iApply iProto_le_branch; iSplit; by iIntros "!> $".
Qed.
(** Automatically perform normalization of protocols in the proof mode when
......@@ -149,15 +199,17 @@ Section classes.
ProtoNormalize false p1 [] p2
FromAssumption q (c p1) (c p2).
Proof.
rewrite /FromAssumption /ProtoNormalize=> ->.
by rewrite /= right_id bi.intuitionistically_if_elim.
rewrite /FromAssumption /ProtoNormalize /= right_id.
rewrite bi.intuitionistically_if_elim.
iIntros (?) "H". by iApply (iProto_mapsto_le with "H").
Qed.
Global Instance mapsto_proto_from_frame q c p1 p2 :
ProtoNormalize false p1 [] p2
Frame q (c p1) (c p2) True.
Proof.
rewrite /Frame /ProtoNormalize=> ->.
by rewrite /= !right_id bi.intuitionistically_if_elim.
rewrite /Frame /ProtoNormalize /= right_id.
rewrite bi.intuitionistically_if_elim.
iIntros (?) "[H _]". by iApply (iProto_mapsto_le with "H").
Qed.
End classes.
......@@ -177,7 +229,8 @@ Lemma tac_wp_recv `{!chanG Σ, !heapG Σ} {TT : tele} Δ i j K
envs_entails Δ (WP fill K (recv c) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= tforall_forall right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
rewrite envs_lookup_sound //; simpl.
rewrite (iProto_mapsto_le _ _ (iProto_message Recv pc)) -bi.later_intro -Hp left_id.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply recv_spec|f_equiv].
rewrite -bi.later_intro bi_tforall_forall; apply bi.forall_intro=> x.
specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
......@@ -261,7 +314,8 @@ Lemma tac_wp_send `{!chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
envs_entails Δ (WP fill K (send c v) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id texist_exist=> ? Hp [x HΦ].
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
rewrite envs_lookup_sound //; simpl.
rewrite (iProto_mapsto_le _ _ (iProto_message Send pc)) -bi.later_intro -Hp left_id.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply send_spec|f_equiv].
rewrite bi_texist_exist -(bi.exist_intro x).
destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
......@@ -351,7 +405,8 @@ Lemma tac_wp_branch `{!chanG Σ, !heapG Σ} Δ i j K
envs_entails Δ (WP fill K (recv c) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
rewrite envs_lookup_sound //; simpl.
rewrite (iProto_mapsto_le _ _ (p1 <{P1}&{P2}> p2)%proto) -bi.later_intro -Hp left_id.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply branch_spec|f_equiv].
rewrite -bi.later_intro; apply bi.forall_intro=> b.
specialize (HΦ b). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
......@@ -403,7 +458,8 @@ Lemma tac_wp_select `{!chanG Σ, !heapG Σ} Δ neg i js K
envs_entails Δ (WP fill K (send c #b) {{ Φ }}).
Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
rewrite envs_lookup_sound //; simpl.
rewrite (iProto_mapsto_le _ _ (p1 <{P1}+{P2}> p2)%proto) -bi.later_intro -Hp left_id.
rewrite -wp_bind. eapply bi.wand_apply; [by eapply select_spec|].
rewrite -assoc; f_equiv.
destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
......
......@@ -29,6 +29,7 @@ From iris.program_logic Require Import language.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import lib.own.
From actris.channel Require Import proto_model.
Set Default Proof Using "Type".
Export action.
(** * Setup of Iris's cameras *)
......@@ -56,11 +57,11 @@ Arguments iProto_end {_ _}.
Program Definition iProto_message_def {Σ V} {TT : tele} (a : action)
(pc : TT V * iProp Σ * iProto Σ V) : iProto Σ V :=
proto_message a (λ v, λne f, x : TT,
proto_message a (λ v, λne p', x : TT,
(** We need the later to make [iProto_message] contractive *)
v = (pc x).1.1
(pc x).1.2
f (Next (pc x).2))%I.
p' Next (pc x).2)%I.
Next Obligation. solve_proper. Qed.
Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
Definition iProto_message := iProto_message_aux.(unseal).
......@@ -145,8 +146,52 @@ Notation "<?> 'MSG' v ; p" :=
Notation "'END'" := iProto_end : proto_scope.
(** * Operations *)
Definition iProto_dual {Σ V} (p : iProto Σ V) : iProto Σ V :=
proto_map action_dual cid cid p.
Program Definition iProto_map_cont {Σ V}
(rec : iProto Σ V iProto Σ V) (pc : laterO (iProto Σ V) -n> iPropO Σ) :
laterO (iProto Σ V) -n> iPropO Σ :=
λne p2, ( p1, pc (Next p1) p2 Next (rec p1))%I.
Next Obligation. solve_proper. Qed.
Program Definition iProto_map_app_aux {Σ V}
(f : action action) (p2 : iProto Σ V)
(rec : iProto Σ V -n> iProto Σ V) : iProto Σ V -n> iProto Σ V := λne p1,
match proto_unfold p1 return _ with
| None => p2
| Some (a, pc) => proto_message (f a) (iProto_map_cont rec pc)
end.
Next Obligation.
intros Σ V f p2 rec n p1 p1'
[[??][??] [-> Hf]|]%(ofe_mor_ne _ _ proto_unfold); last done.
f_equiv=> v pc; rewrite /= /iProto_map_cont /=. by repeat f_equiv.
Qed.
Instance iProto_map_app_aux_contractive {Σ V} f (p2 : iProto Σ V) :
Contractive (iProto_map_app_aux f p2).
Proof.
intros n rec1 rec2 Hrec p1. simpl.
destruct (proto_unfold p1) as [[a c]|]; last done.
f_equiv=> v p' /=. by repeat (f_contractive || f_equiv).
Qed.
Definition iProto_map_app {Σ V} (f : action action)
(p2 : iProto Σ V) : iProto Σ V -n> iProto Σ V :=
fixpoint (iProto_map_app_aux f p2).
Definition iProto_app_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V :=
iProto_map_app id p2 p1.
Definition iProto_app_aux : seal (@iProto_app_def). by eexists. Qed.
Definition iProto_app := iProto_app_aux.(unseal).
Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
Arguments iProto_app {_ _} _%proto _%proto.
Instance: Params (@iProto_app) 2 := {}.
Infix "<++>" := iProto_app (at level 60) : proto_scope.
Definition iProto_dual_def {Σ V} (p : iProto Σ V) : iProto Σ V :=
iProto_map_app action_dual proto_end p.
Definition iProto_dual_aux : seal (@iProto_dual_def). by eexists. Qed.
Definition iProto_dual := iProto_dual_aux.(unseal).
Definition iProto_dual_eq :
@iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
Arguments iProto_dual {_ _} _%proto.
Instance: Params (@iProto_dual) 2 := {}.
Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
......@@ -154,17 +199,8 @@ Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
Arguments iProto_dual_if {_ _} _ _%proto.
Instance: Params (@iProto_dual_if) 3 := {}.
Definition iProto_app {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V := proto_app p1 p2.
Arguments iProto_app {_ _} _%proto _%proto.
Instance: Params (@iProto_app) 2 := {}.
Infix "<++>" := iProto_app (at level 60) : proto_scope.
(** * Auxiliary definitions and invariants *)
Definition proto_eq_next {Σ V} (p : iProto Σ V) : laterO (iProto Σ V) -n> iPropO Σ :=
OfeMor (sbi_internal_eq (Next p)).
(*
The definition [iProto_le] generalizes the following inductive definition
(** * Protocol entailment *)
(* The definition [iProto_le] generalizes the following inductive definition
for subtyping on session types:
p1 <: p2 p1 <: p2
......@@ -191,19 +227,19 @@ Definition iProto_le_pre {Σ V}
p2 proto_message a2 pc2
match a1, a2 with
| Recv, Recv =>
v p1', pc1 v (proto_eq_next p1') -
p2', rec p1' p2' pc2 v (proto_eq_next p2')
v p1', pc1 v (Next p1') -
p2', rec p1' p2' pc2 v (Next p2')
| Send, Send =>
v p2', pc2 v (proto_eq_next p2') -
p1', rec p1' p2' pc1 v (proto_eq_next p1')
v p2', pc2 v (Next p2') -
p1', rec p1' p2' pc1 v (Next p1')
| Recv, Send =>
v1 v2 p1' p2',
pc1 v1 (proto_eq_next p1') - pc2 v2 (proto_eq_next p2') -
pc1 v1 (Next p1') - pc2 v2 (Next p2') -
pc1' pc2' pt,
rec p1' (proto_message Send pc1')
rec (proto_message Recv pc2') p2'
pc1' v2 (proto_eq_next pt)
pc2' v1 (proto_eq_next pt)
pc1' v2 (Next pt)
pc2' v1 (Next pt)
| Send, Recv => False
end.
Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V iProto Σ V iProp Σ) :
......@@ -220,7 +256,8 @@ Proof.
intros n rec1 rec2 Hrec p1 p2. rewrite /iProto_le_pre' /iProto_le_pre /=.
by repeat (f_contractive || f_equiv).
Qed.
Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ := fixpoint iProto_le_pre' p1 p2.
Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
fixpoint iProto_le_pre' p1 p2.
Arguments iProto_le {_ _} _%proto _%proto.
Instance: Params (@iProto_le) 2 := {}.
......@@ -236,12 +273,12 @@ Fixpoint iProto_interp_aux {Σ V} (n : nat)
( vl vsl' pc p2',
vsl = vl :: vsl'
iProto_le (proto_message Recv pc) pr
pc vl (proto_eq_next p2')
pc vl (Next p2')
iProto_interp_aux n vsl' vsr pl p2')
( vr vsr' pc p1',
vsr = vr :: vsr'
iProto_le (proto_message Recv pc) pl
pc vr (proto_eq_next p1')
pc vr (Next p1')
iProto_interp_aux n vsl vsr' p1' pr)
end.
Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
......@@ -272,7 +309,7 @@ Definition side_elim {A} (s : side) (l r : A) : A :=
match s with Left => l | Right => r end.
Definition iProto_unfold {Σ V} (p : iProto Σ V) : proto V (iPrePropO Σ) (iPrePropO Σ) :=
proto_map id iProp_fold iProp_unfold p.
proto_map iProp_fold iProp_unfold p.
Definition iProto_own_frag `{!protoG Σ V} (γ : proto_name) (s : side)
(p : iProto Σ V) : iProp Σ :=
own (side_elim s proto_l_name proto_r_name γ) (E (Next (iProto_unfold p))).
......@@ -334,60 +371,103 @@ Section proto.
(** ** Dual *)
Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V).
Proof. solve_proper. Qed.
Proof. rewrite iProto_dual_eq. solve_proper. Qed.
Global Instance iProto_dual_proper : Proper (() ==> ()) (@iProto_dual Σ V).
Proof. apply (ne_proper _). Qed.
Global Instance iProto_dual_if_ne d : NonExpansive (@iProto_dual_if Σ V d).
Proof. solve_proper. Qed.
Global Instance iProto_dual_if_proper d : Proper (() ==> ()) (@iProto_dual_if Σ V d).
Global Instance iProto_dual_if_proper d :
Proper (() ==> ()) (@iProto_dual_if Σ V d).
Proof. apply (ne_proper _). Qed.
Global Instance iProto_dual_involutive : Involutive () (@iProto_dual Σ V).
Lemma iProto_dual_end' : iProto_dual (Σ:=Σ) (V:=V) proto_end proto_end.
Proof.
intros p. rewrite /iProto_dual -proto_map_compose -{2}(proto_map_id p).
apply: proto_map_ext=> //. by intros [].
rewrite iProto_dual_eq /iProto_dual_def /iProto_map_app.
etrans; [eapply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
pose proof (proto_unfold_fold (V:=V)
(PROP:=iPropO Σ) (PROPn:=iPropO Σ) None) as Hfold.
by destruct (proto_unfold (proto_fold None))
as [[??]|] eqn:E; rewrite E; inversion Hfold.
Qed.
Lemma iProto_dual_message' a pc :
iProto_dual (Σ:=Σ) (V:=V) (proto_message a pc)
proto_message (action_dual a) (iProto_map_cont iProto_dual pc).
Proof.
rewrite iProto_dual_eq /iProto_dual_def /iProto_map_app /proto_message.
etrans; [eapply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
pose proof (proto_unfold_fold (V:=V) (PROP:=iPropO Σ)
(PROPn:=iPropO Σ) (Some (a,pc))) as Hfold.
destruct (proto_unfold (proto_fold (Some (a, pc))))
as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hpc]|]; simplify_eq/=.
rewrite /proto_message. do 3 f_equiv; intros v p'; simpl. by repeat f_equiv.
Qed.
Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END END%proto.
Proof. by rewrite iProto_end_eq /iProto_dual proto_map_end. Qed.
Proof. rewrite iProto_end_eq. apply iProto_dual_end'. Qed.
Lemma iProto_dual_message {TT} a (pc : TT V * iProp Σ * iProto Σ V) :
iProto_dual (iProto_message a pc)
iProto_message (action_dual a) (prod_map id iProto_dual pc).
Proof.
rewrite /iProto_dual iProto_message_eq /iProto_message_def proto_map_message.
by f_equiv=> v f /=.
rewrite iProto_message_eq /iProto_message_def iProto_dual_message' /=.
do 2 f_equiv; intros p'; simpl. iSplit.
- iDestruct 1 as (pd) "[H Hp']". iDestruct "H" as (x ->) "[Hpc Hpd]".
iExists x. iSplit; [done|]; iFrame. iRewrite "Hp'". iNext. by iRewrite "Hpd".
- iDestruct 1 as (x ->) "[Hpc Hpd]"; auto 10.
Qed.
(** Helpers for duals *)
Global Instance proto_eq_next_ne : NonExpansive (proto_eq_next (Σ:=Σ) (V:=V)).
Proof. solve_proper. Qed.
Global Instance proto_eq_next_proper :
Proper (() ==> ()) (proto_eq_next (Σ:=Σ) (V:=V)).
Proof. solve_proper. Qed.
Lemma proto_eq_next_dual p :
ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid
(proto_eq_next (iProto_dual p)) proto_eq_next p.
Global Instance iProto_dual_involutive : Involutive () (@iProto_dual Σ V).
Proof.
intros lp. iSplit; iIntros "Hlp /="; last by iRewrite -"Hlp".
destruct (Next_uninj lp) as [p' ->].
rewrite /later_map /= !bi.later_equivI. iNext.
rewrite -{2}(involutive iProto_dual p) -{2}(involutive iProto_dual p').
by iRewrite "Hlp".
intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
iLöb as "IH" forall (p). destruct (proto_case p) as [->|(a&pc&->)].
{ by rewrite !iProto_dual_end'. }
rewrite !iProto_dual_message' involutive.
iApply proto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
iApply prop_ext; iIntros "!>"; iSplit.
- iDestruct 1 as (pd) "[H Hp']". iRewrite "Hp'".
iDestruct "H" as (pdd) "[H #Hpd]".
iApply (bi.internal_eq_rewrite); [|done]; iModIntro.
iRewrite "Hpd". by iRewrite ("IH" $! pdd).
- iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists (iProto_dual p'').
rewrite Hp'. iSplitL; [by auto|]. iNext. by iRewrite ("IH" $! p'').
Qed.
Lemma proto_eq_next_dual' p :
ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid (proto_eq_next p)
proto_eq_next (iProto_dual p).
(** ** Append *)
Lemma iProto_app_end' p : (proto_end <++> p)%proto p.
Proof.
rewrite iProto_app_eq /iProto_app_def /iProto_map_app.
etrans; [eapply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
pose proof (proto_unfold_fold (V:=V)
(PROP:=iPropO Σ) (PROPn:=iPropO Σ) None) as Hfold.
by destruct (proto_unfold (proto_fold None))
as [[??]|] eqn:E; rewrite E; inversion Hfold.
Qed.
Lemma iProto_app_message' a pc p2 :
(proto_message a pc <++> p2)%proto
proto_message a (iProto_map_cont (flip iProto_app p2) pc).
Proof.
rewrite -(proto_eq_next_dual (iProto_dual p))=> lp /=.
by rewrite involutive.
rewrite iProto_app_eq /iProto_app_def /iProto_map_app /proto_message.
etrans; [eapply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
pose proof (proto_unfold_fold (V:=V) (PROP:=iPropO Σ)
(PROPn:=iPropO Σ) (Some (a,pc))) as Hfold.
destruct (proto_unfold (proto_fold (Some (a, pc))))
as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hpc]|]; simplify_eq/=.
rewrite /proto_message. do 3 f_equiv; intros v p'; simpl. by repeat f_equiv.
Qed.
(** ** Append *)
Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
Proof. apply _. Qed.
Proof.
assert ( n, Proper (dist n ==> (=) ==> dist n) (@iProto_app Σ V)).
{ intros n p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
assert (Proper (() ==> (=) ==> ()) (@iProto_app Σ V)).
{ intros p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
intros n p1 p1' Hp1 p2 p2' Hp2. rewrite Hp1. clear p1 Hp1.
revert p1'. induction (lt_wf n) as [n _ IH]; intros p1.
destruct (proto_case p1) as [->|(a&pc&->)].
{ by rewrite !iProto_app_end'. }
rewrite !iProto_app_message'. f_equiv=> v p' /=. f_equiv=> p12.
do 2 f_equiv. f_contractive. apply IH; eauto using dist_le with lia.
Qed.
Global Instance iProto_app_proper : Proper (() ==> () ==> ()) (@iProto_app Σ V).
Proof. apply (ne_proper_2 _). Qed.
......@@ -395,24 +475,62 @@ Section proto.
(iProto_message a pc <++> p2)%proto
iProto_message a (prod_map id (flip iProto_app p2) pc).
Proof.
rewrite /iProto_app iProto_message_eq /iProto_message_def proto_app_message.
by f_equiv=> v f /=.
rewrite iProto_message_eq /iProto_message_def iProto_app_message' /=.
f_equiv=> v ps /=. iSplit.
- iDestruct 1 as (p1') "[H Hps]". iDestruct "H" as (x ->) "[Hpc #Hp1']".
iExists x. iSplit; [done|]. iFrame. iRewrite "Hps". iNext. by iRewrite "Hp1'".
- iDestruct 1 as (x ->) "[Hpc Hps]". auto 10.
Qed.
Global Instance iProto_app_end_l : LeftId () END%proto (@iProto_app Σ V).
Proof.
intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_l.
Qed.
Proof. intros p. by rewrite iProto_end_eq /iProto_end_def iProto_app_end'. Qed.