Commit d9b0b2c4 authored by Robbert Krebbers's avatar Robbert Krebbers

Many changes.

- Allow for binders in protocols.
- Model protocols in CPS style using the COFE solver.
- Change the channel methods so they do not mention sides.
- Lots of refactoring.
- Generalize the `list_sort` example.
- Move stuff to stdpp/Iris.
parent a0c63e6f
-Q theories osiris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/utils/auth_excl.v
theories/proto/encodable.v
theories/proto/list.v
theories/proto/channel.v
theories/proto/involutive.v
theories/proto/side.v
theories/proto/proto_def.v
theories/proto/proto_specs.v
theories/proto/proto_enc.v
theories/proto/branching.v
theories/utils/encodable.v
theories/utils/list.v
theories/channel/channel.v
theories/channel/proto_model.v
theories/channel/proto_channel.v
theories/channel/branching.v
theories/examples/proofs_enc.v
theories/examples/branching_proofs.v
theories/examples/list_sort.v
From iris.heap_lang Require Import proofmode notation.
From osiris.proto Require Export proto_enc.
From osiris.channel Require Export proto_channel.
Definition TSB {PROP : bi} (a : action)
(prot1 prot2 : proto val PROP) : proto val PROP :=
......
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import excl auth list.
From osiris.utils Require Import auth_excl.
From osiris.proto Require Export side.
From osiris.proto Require Import list.
From osiris.utils Require Import auth_excl list.
Set Default Proof Using "Type".
Inductive side := Left | Right.
Instance side_inhabited : Inhabited side := populate Left.
Definition side_elim {A} (s : side) (l r : A) : A :=
match s with Left => l | Right => r end.
Definition new_chan : val :=
λ: <>,
let: "l" := ref (lnil #()) in
let: "r" := ref (lnil #()) in
let: "lk" := newlock #() in
(("l","r"),"lk").
Coercion side_to_bool (s : side) : bool :=
match s with Left => true | Right => false end.
Arguments side_to_bool : simpl never.
Definition side_elim {A} (s : side) (l r : A) : A :=
match s with Left => l | Right => r end.
Definition get_side : val := λ: "c" "s",
(if: "s" = #Left then Fst (Fst "c") else Snd (Fst "c"))%E.
Definition get_lock : val := λ: "c", Snd "c".
Definition get_dual_side : val := λ: "s",
(if: "s" = #Left then #Right else #Left)%E.
((("l","r"),"lk"), (("r","l"),"lk")).
Definition send : val :=
λ: "c" "s" "v",
let: "lk" := get_lock "c" in
λ: "c" "v",
let: "lk" := Snd "c" in
acquire "lk";;
let: "l" := get_side "c" "s" in
let: "l" := Fst (Fst "c") in
"l" <- lsnoc !"l" "v";;
release "lk".
Definition try_recv : val :=
λ: "c" "s",
let: "lk" := get_lock "c" in
λ: "c",
let: "lk" := Snd "c" in
acquire "lk";;
let: "l" := get_side "c" (get_dual_side "s") in
let: "l" := Snd (Fst "c") in
let: "ret" :=
match: !"l" with
SOME "p" => "l" <- Snd "p";; SOME (Fst "p")
......@@ -47,10 +37,10 @@ Definition try_recv : val :=
release "lk";; "ret".
Definition recv : val :=
rec: "go" "c" "s" :=
match: try_recv "c" "s" with
rec: "go" "c" :=
match: try_recv "c" with
SOME "p" => "p"
| NONE => "go" "c" "s"
| NONE => "go" "c"
end.
Class chanG Σ := {
......@@ -80,12 +70,12 @@ Section channel.
is_list_ref r rs own (chan_r_name γ) ( to_auth_excl rs))%I.
Typeclasses Opaque chan_inv.
Definition is_chan (γ : chan_name) (c : val) : iProp Σ :=
Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ :=
( l r lk : val,
c = ((l, r), lk)%V
c1 = ((l, r), lk)%V c2 = ((r, l), lk)%V
is_lock N (chan_lock_name γ) lk (chan_inv γ l r))%I.
Global Instance is_chan_persistent : Persistent (is_chan γ c).
Global Instance is_chan_persistent : Persistent (is_chan γ c1 c2).
Proof. by apply _. Qed.
Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ :=
......@@ -94,24 +84,10 @@ Section channel.
Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
Proof. by apply _. Qed.
Lemma get_side_spec Φ s (l r lk : val) :
Φ (side_elim s l r) -
WP get_side ((l, r), lk)%V #s {{ Φ }}.
Proof. iIntros "?". wp_lam. by destruct s; wp_pures. Qed.
Lemma get_lock_spec Φ (l r lk : val) :
Φ lk -
WP get_lock ((l, r), lk)%V {{ Φ }}.
Proof. iIntros "?". wp_lam. by wp_pures. Qed.
Lemma dual_side_spec Φ s :
Φ #(dual_side s) - WP get_dual_side #s {{ Φ }}.
Proof. iIntros "?". wp_lam. by destruct s; wp_pures. Qed.
Lemma new_chan_spec :
{{{ True }}}
new_chan #()
{{{ c γ, RET c; is_chan γ c chan_own γ Left [] chan_own γ Right [] }}}.
{{{ c1 c2 γ, RET (c1,c2); is_chan γ c1 c2 chan_own γ Left [] chan_own γ Right [] }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_own.
wp_lam.
......@@ -131,7 +107,7 @@ Section channel.
with "[Hl Hr Hls Hrs]").
{ eauto 10 with iFrame. }
iIntros (lk γlk) "#Hlk". wp_pures.
iApply ("HΦ" $! _ (Chan_name γlk lsγ rsγ)); simpl.
iApply ("HΦ" $! _ _ (Chan_name γlk lsγ rsγ)); simpl.
rewrite /chan_inv /=. eauto 20 with iFrame.
Qed.
......@@ -146,22 +122,23 @@ Section channel.
iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
Qed.
Lemma send_spec Φ E γ c v s :
is_chan γ c -
Lemma send_spec Φ E γ c1 c2 v s :
is_chan γ c1 c2 -
(|={,E}=> vs,
chan_own γ s vs
(chan_own γ s (vs ++ [v]) ={E,}= Φ #())) -
WP send c #s v {{ Φ }}.
(chan_own γ s (vs ++ [v]) ={E,}= Φ #())) -
WP send (side_elim s c1 c2) v {{ Φ }}.
Proof.
iIntros "Hc HΦ". wp_lam; wp_pures.
iDestruct "Hc" as (l r lk ->) "#Hlock"; wp_pures.
wp_apply get_lock_spec; wp_pures.
iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
assert (side_elim s (l, r, lk)%V (r, l, lk)%V =
((side_elim s l r, side_elim s r l), lk)%V) as -> by (by destruct s).
wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
wp_apply get_side_spec; wp_pures.
wp_pures.
iDestruct (chan_inv_alt s with "Hinv") as
(vs ws) "(Href & Hvs & Href' & Hws)".
(vs ws) "(Href & Hvs & Href' & Hws)".
iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
wp_load.
wp_load.
wp_apply (lsnoc_spec (A:=val))=> //; iIntros (_).
wp_bind (_ <- _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
......@@ -174,76 +151,56 @@ Section channel.
rewrite /is_list_ref. eauto 20 with iFrame.
Qed.
Lemma try_recv_spec Φ E γ c s :
is_chan γ c -
(|={,E}=> vs,
chan_own γ (dual_side s) vs
((vs = [] - chan_own γ (dual_side s) vs ={E,}= Φ NONEV)
( v vs', vs = v :: vs' -
chan_own γ (dual_side s) vs' ={E,}= Φ (SOMEV v)))) -
WP try_recv c #s {{ Φ }}.
Lemma try_recv_spec Φ E γ c1 c2 s :
is_chan γ c1 c2 -
((|={,E}=> Φ NONEV)
(|={,E}=> vs,
chan_own γ s vs
( v vs', vs = v :: vs' -
chan_own γ s vs' ={E,}= Φ (SOMEV v)))) -
WP try_recv (side_elim s c2 c1) {{ Φ }}.
Proof.
iIntros "Hc HΦ". wp_lam; wp_pures.
iDestruct "Hc" as (l r lk ->) "#Hlock"; wp_pures.
wp_apply get_lock_spec; wp_pures.
wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]". wp_pures.
wp_apply dual_side_spec. wp_apply get_side_spec; wp_pures.
iDestruct (chan_inv_alt (dual_side s) with "Hinv") as
(vs ws) "(Href & Hvs & Href' & Hws)".
iDestruct "Href" as (ll Hslr) "Hll"; rewrite Hslr.
wp_bind (! _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
wp_load.
iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
destruct vs as [|v vs]; simpl.
- iDestruct "HΦ" as "[HΦ _]".
iMod ("HΦ" with "[//] Hchan") as "HΦ".
iModIntro.
iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
assert (side_elim s (r, l, lk)%V (l, r, lk)%V =
((side_elim s r l, side_elim s l r), lk)%V) as -> by (by destruct s).
wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
wp_pures.
iDestruct (chan_inv_alt s with "Hinv")
as (vs ws) "(Href & Hvs & Href' & Hws)".
iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
wp_bind (! _)%E. destruct vs as [|v vs]; simpl.
- iDestruct "HΦ" as "[>HΦ _]". wp_load. iMod "HΦ"; iModIntro.
wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
{ iApply (chan_inv_alt (dual_side s)).
{ iApply (chan_inv_alt s).
rewrite /is_list_ref. eauto 10 with iFrame. }
iIntros (_). wp_pures. by iApply "HΦ".
- iMod (excl_update _ _ _ vs with "Hvs Hchan") as "[Hvs Hchan]".
iDestruct "HΦ" as "[_ HΦ]".
iMod ("HΦ" with "[//] Hchan") as "HΦ".
iModIntro. wp_store.
iIntros (_). by wp_pures.
- iDestruct "HΦ" as "[_ >HΦ]". iDestruct "HΦ" as (vs') "[Hvs' HΦ]".
iDestruct (excl_eq with "Hvs Hvs'") as %<-%leibniz_equiv.
iMod (excl_update _ _ _ vs with "Hvs Hvs'") as "[Hvs Hvs']".
wp_load.
iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro.
wp_store; wp_pures.
wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
{ iApply (chan_inv_alt (dual_side s)).
{ iApply (chan_inv_alt s).
rewrite /is_list_ref. eauto 10 with iFrame. }
iIntros (_). wp_pures. by iApply "HΦ".
iIntros (_). by wp_pures.
Qed.
Lemma recv_spec Φ E γ c s :
is_chan γ c -
( (|={,E}=> vs,
chan_own γ (dual_side s) vs
((vs = [] - chan_own γ (dual_side s) vs ={E,}= True)
( v vs', vs = v :: vs' -
chan_own γ (dual_side s) vs' ={E,}= Φ v)))) -
WP recv c #s {{ Φ }}.
Lemma recv_spec Φ E γ c1 c2 s :
is_chan γ c1 c2 -
(|={,E}=> vs,
chan_own γ s vs
v vs', vs = v :: vs' -
chan_own γ s vs' ={E,}= Φ v) -
WP recv (side_elim s c2 c1) {{ Φ }}.
Proof.
iIntros "#Hc #HΦ".
rewrite /recv.
iLöb as "IH".
wp_apply (try_recv_spec with "Hc")=> //.
iMod "HΦ" as (vs) "[Hchan [HΦfail HΦsucc]]".
iModIntro.
iExists _.
iFrame.
iNext.
iSplitL "HΦfail".
- iIntros "Hvs Hown".
iRename ("HΦfail") into "HΦ".
iDestruct ("HΦ" with "Hvs Hown") as "HΦ".
iMod ("HΦ") as "HΦ".
iModIntro.
wp_match.
by iApply ("IH").
- iRename ("HΦsucc") into "HΦ".
iIntros (v vs') "Hvs Hown".
iMod ("HΦ" with "Hvs Hown") as "HΦ".
iModIntro.
by wp_pures.
iIntros "#Hc HΦ". iLöb as "IH". wp_lam.
wp_apply (try_recv_spec _ E with "Hc")=> //. iSplit.
- iMod (fupd_intro_mask' _ E) as "Hclose"; first done. iIntros "!> !>".
iMod "Hclose" as %_; iIntros "!> !>". wp_pures. by iApply "IH".
- iMod "HΦ" as (vs) "[Hvs HΦ]". iExists vs; iFrame "Hvs".
iIntros "!> !>" (v vs' ->) "Hvs".
iMod ("HΦ" with "[//] Hvs") as "HΦ". iIntros "!> !> !>". by wp_pures.
Qed.
End channel.
\ No newline at end of file
End channel.
This diff is collapsed.
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import cofe_solver.
Set Default Proof Using "Type".
Inductive action := Send | Receive.
Instance action_inhabited : Inhabited action := populate Send.
Definition action_dual (a : action) : action :=
match a with Send => Receive | Receive => Send end.
Instance action_dual_involutive : Involutive (=) action_dual.
Proof. by intros []. Qed.
Canonical Structure actionO := leibnizO action.
Definition protoOF_helper (V : Type) (PROPn PROP : ofeT) : oFunctor :=
optionOF (actionO * (V -d> ( -n> PROPn) -n> PROP)).
Definition proto_result (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} :
solution (protoOF_helper V PROPn PROP) := solver.result _.
Definition proto (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} : ofeT :=
proto_result V PROPn PROP.
Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn PROP).
Proof. apply _. Qed.
Definition proto_fold {V} `{!Cofe PROPn, !Cofe PROP} :
protoOF_helper V PROPn PROP (proto V PROPn PROP) _ -n> proto V PROPn PROP :=
solution_fold (proto_result V PROPn PROP).
Definition proto_unfold {V} `{!Cofe PROPn, !Cofe PROP} :
proto V PROPn PROP -n> protoOF_helper V PROPn PROP (proto V PROPn PROP) _ :=
solution_unfold (proto_result V PROPn PROP).
Lemma proto_fold_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
proto_fold (proto_unfold p) p.
Proof. apply solution_fold_unfold. Qed.
Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP}
(p : protoOF_helper V PROPn PROP (proto V PROPn PROP) _) :
proto_unfold (proto_fold p) p.
Proof. apply solution_unfold_fold. Qed.
Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP :=
proto_fold None.
Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
(pc : V (laterO (proto V PROPn PROP) -n> PROPn) -n> PROP) : proto V PROPn PROP :=
proto_fold (Some (a, pc)).
Lemma proto_message_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 pc1 pc2 :
proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 pc1 proto_message a2 pc2
@{SPROP} a1 = a2 ( v, pc1 v pc2 v).
Proof.
trans (proto_unfold (proto_message a1 pc1) proto_unfold (proto_message a2 pc2) : SPROP)%I.
{ iSplit.
- iIntros "Heq". by iRewrite "Heq".
- iIntros "Heq". rewrite -{2}(proto_fold_unfold (proto_message _ _)).
iRewrite "Heq". by rewrite proto_fold_unfold. }
rewrite /proto_message !proto_unfold_fold bi.option_equivI bi.prod_equivI /=.
by rewrite bi.discrete_fun_equivI bi.discrete_eq.
Qed.
Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
p proto_end a pc, p proto_message a pc.
Proof.
destruct (proto_unfold p) as [[a pc]|] eqn:E; simpl in *; last first.
- left. by rewrite -(proto_fold_unfold p) E.
- right. exists a, pc. by rewrite -(proto_fold_unfold p) E.
Qed.
Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
Inhabited (proto V PROPn PROP) := populate proto_end.
Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
Proper (pointwise_relation V (dist n) ==> dist n)
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
Proper (pointwise_relation V () ==> ())
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
Definition proto_cont_map
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, Cofe PROP', !Cofe A, !Cofe B}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') (h : A -n> B) :
((laterO A -n> PROPn) -n> PROP) -n> (laterO B -n> PROPn') -n> PROP' :=
ofe_morO_map (ofe_morO_map (laterO_map h) gn) g.
Program Definition proto_map_aux {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(f : action action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP')
(rec : proto V PROPn PROP -n> proto V PROPn' PROP') :
proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
match proto_unfold p return _ with
| None => proto_end
| Some (a, c) => proto_message (f a) (proto_cont_map gn g rec c)
end.
Next Obligation.
intros V PROPn ? PROPn' ? PROP ? PROP' ? f g1 g2 rec n p1 p2 Hp.
apply (ofe_mor_ne _ _ proto_unfold) in Hp.
destruct Hp as [[??][??] [-> ?]|]; simplify_eq/=; last done.
f_equiv=> v /=. by f_equiv.
Qed.
Instance proto_map_aux_contractive {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(f : action action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
Contractive (proto_map_aux (V:=V) f gn g).
Proof.
intros n rec1 rec2 Hrec p. simpl.
destruct (proto_unfold p) as [[a c]|]; last done.
f_equiv=> v /=. do 2 f_equiv.
intros=> p'. apply Next_contractive. destruct n as [|n]=> //=.
Qed.
Definition proto_map {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(f : action action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
proto V PROPn PROP -n> proto V PROPn' PROP' :=
fixpoint (proto_map_aux f gn g).
Lemma proto_map_unfold {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(f : action action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p :
proto_map (V:=V) f gn g p proto_map_aux f gn g (proto_map f gn g) p.
Proof. apply (fixpoint_unfold (proto_map_aux f gn g)). Qed.
Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, Cofe PROP'}
(f : action action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
proto_map (V:=V) f gn g proto_end proto_end.
Proof.
rewrite proto_map_unfold /proto_end /=.
pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) None) as Hfold.
by destruct (proto_unfold (proto_fold None))
as [[??]|] eqn:E; rewrite E; inversion Hfold.
Qed.
Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(f : action action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a c :
proto_map (V:=V) f gn g (proto_message a c) proto_message (f a) (proto_cont_map gn g (proto_map f gn g) c).
Proof.
rewrite proto_map_unfold /proto_message /=.
pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) (Some (a, c))) as Hfold.
destruct (proto_unfold (proto_fold (Some (a, c))))
as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hc]|]; simplify_eq/=.
rewrite /proto_message. do 3 f_equiv. intros v=> /=.
apply equiv_dist=> n. f_equiv. by apply equiv_dist.
Qed.
Lemma proto_map_ne {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(f1 f2 : action action) (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p n :
( a, f1 a = f2 a) ( x, gn1 x {n} gn2 x) ( x, g1 x {n} g2 x)
proto_map (V:=V) f1 gn1 g1 p {n} proto_map (V:=V) f2 gn2 g2 p.
Proof.
intros Hf. revert p. induction (lt_wf n) as [n _ IH]=> p Hgn Hg /=.
destruct (proto_case p) as [->|(a & c & ->)].
- by rewrite !proto_map_end.
- rewrite !proto_map_message /= Hf. f_equiv=> v /=. do 2 (f_equiv; last done).
intros p'. apply Next_contractive. destruct n as [|n]=> //=.
apply IH; first lia; auto using dist_S.
Qed.
Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(f1 f2 : action action) (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
( a, f1 a = f2 a) ( x, gn1 x gn2 x) ( x, g1 x g2 x)
proto_map (V:=V) f1 gn1 g1 p proto_map (V:=V) f2 gn2 g2 p.
Proof.
intros Hf Hgn Hg. apply equiv_dist=> n.
apply proto_map_ne=> // ?; by apply equiv_dist.
Qed.
Lemma proto_map_id {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
proto_map id cid cid p p.
Proof.
apply equiv_dist=> n. revert p. induction (lt_wf n) as [n _ IH]=> p /=.
destruct (proto_case p) as [->|(a & c & ->)].
- by rewrite !proto_map_end.
- rewrite !proto_map_message /=. f_equiv=> v c' /=. f_equiv=> p' /=. f_equiv.
apply Next_contractive. destruct n as [|n]=> //=.
apply IH; first lia; auto using dist_S.
Qed.
Lemma proto_map_compose {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROPn'', !Cofe PROP, !Cofe PROP', !Cofe PROP''}
(f1 f2 : action action)
(gn1 : PROPn'' -n> PROPn') (gn2 : PROPn' -n> PROPn)
(g1 : PROP -n> PROP') (g2 : PROP' -n> PROP'') (p : proto V PROPn PROP) :
proto_map (f2 f1) (gn2 gn1) (g2 g1) p proto_map f2 gn1 g2 (proto_map f1 gn2 g1 p).
Proof.
apply equiv_dist=> n. revert p. induction (lt_wf n) as [n _ IH]=> p /=.
destruct (proto_case p) as [->|(a & c & ->)].
- by rewrite !proto_map_end.
- rewrite !proto_map_message /=. f_equiv=> v c' /=. do 3 f_equiv. move=> p' /=.
do 3 f_equiv. apply Next_contractive. destruct n as [|n]=> //=.
apply IH; first lia; auto using dist_S.
Qed.
Program Definition protoOF (V : Type) (Fn F : oFunctor)
`{! A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
`{! A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} : oFunctor := {|
oFunctor_car A _ B _ := proto V (oFunctor_car Fn B A) (oFunctor_car F A B);
oFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
proto_map id (oFunctor_map Fn (fg.2, fg.1)) (oFunctor_map F fg)
|}.
Next Obligation.
intros V Fn F ?? A1 ? A2 ? B1 ? B2 ? n f g [??] p; simpl in *.
apply proto_map_ne=> // y; by apply oFunctor_ne.
Qed.
Next Obligation.
intros V Fn F ?? A ? B ? p; simpl in *. rewrite /= -{2}(proto_map_id p).
apply proto_map_ext=> //= y; by rewrite oFunctor_id.
Qed.
Next Obligation.
intros V Fn F ?? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' p; simpl in *.
rewrite -proto_map_compose.
apply proto_map_ext=> //= y; by rewrite oFunctor_compose.
Qed.
Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
`{! A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
`{! A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} :
oFunctorContractive Fn oFunctorContractive F
oFunctorContractive (protoOF V Fn F).
Proof.
intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
apply proto_map_ne=> //= y.