Skip to content
Snippets Groups Projects
Commit 79b59cb3 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

WIP: Mixed Choice List

parent 74e56d04
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
multris/channel/proto.v
+ 224
− 105
View file @ 79b59cb3
......@@ -117,6 +117,15 @@ Definition iProto_message_eq :
Arguments iProto_message {_ _} _ _%_msg.
Global Instance: Params (@iProto_message) 3 := {}.
Definition iProto_union_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V :=
proto_union p1 p2.
Definition iProto_union_aux : seal (@iProto_union_def). by eexists. Qed.
Definition iProto_union := iProto_union_aux.(unseal).
Definition iProto_union_eq :
@iProto_union = @iProto_union_def := iProto_union_aux.(seal_eq).
Arguments iProto_union {_ _} _ _%_msg.
Global Instance: Params (@iProto_union) 3 := {}.
Notation "'END'" := iProto_end : proto_scope.
Notation "< a > m" := (iProto_message a m)
......@@ -129,6 +138,8 @@ Notation "< a @.. x1 .. xn > m" := (iProto_message a (∃.. x1, .. (∃.. xn, m)
(at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
format "< a @.. x1 .. xn > m") : proto_scope.
Infix "<+>'" := iProto_union (at level 20) : proto_scope.
Class MsgTele {Σ V} {TT : tele} (m : iMsg Σ V)
(tv : TT -t> V) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ V) :=
msg_tele : m ≡ (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg.
......@@ -140,51 +151,134 @@ Program Definition iMsg_map {Σ V}
IMsg (λ v, λne p1', ∃ p1, iMsg_car m v (Next p1) ∗ p1' ≡ 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 p, *)
(* proto_elim p2 (λ a m, *)
(* proto_message (f a) (iMsg_car (iMsg_map rec (IMsg m)))) p. *)
(* Next Obligation. *)
(* intros Σ V f p2 rec n p1 p1' Hp. apply proto_elim_ne=> // a m1 m2 Hm. *)
(* apply proto_message_ne=> v p' /=. by repeat f_equiv. *)
(* Qed. *)
(* Global 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. apply proto_elim_ne=> // a m1 m2 Hm. *)
(* apply proto_message_ne=> v p' /=. by repeat (f_contractive || f_equiv). *)
(* Qed. *)
(* TODO: Move to proto_model.v *)
Lemma fold_left_ne {A B : ofe} (f1 f2 : A → B → A) (xs1 xs2 : list B) (y1 y2 : A) n :
(∀ a1 a2 y1 y2, a1 ≡{n}≡ a2 → y1 ≡{n}≡ y2 → f1 a1 y1 ≡{n}≡ f2 a2 y2) →
y1 ≡{n}≡ y2 →
xs1 ≡{n}≡ xs2 →
fold_left f1 xs1 y1 ≡{n}≡ fold_left f2 xs2 y2.
Proof.
revert xs2. revert y1 y2.
induction xs1 as [|x1 xs1 IHxs1].
- intros y1 y2 xs2 Hf Hx Hxs.
destruct xs2; [|by inversion Hxs].
simpl. done.
- intros y1 y2 xs2 Hf Hx Hxs.
destruct xs2; [by inversion Hxs|].
inversion Hxs; subst.
simpl. apply IHxs1; try done.
by apply Hf.
Qed.
Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A}
(x y : A) (f : A → action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
(p : proto V PROPn PROP) : A :=
match p with
| [] => x
| p => fold_left (λ acc am, f acc (am.1) (λ v, am.2 v ◎ laterO_map proto_unfold)) p y
end.
Global Arguments proto_elim : simpl never.
Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x y : A) (f1 f2 : A → action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) p1 p2 n :
(∀ x1 x2 a m1 m2, x1 ≡{n}≡ x2 → (∀ v, m1 v ≡{n}≡ m2 v) → f1 x1 a m1 ≡{n}≡ f2 x2 a m2) →
p1 ≡{n}≡ p2 →
proto_elim x y f1 p1 ≡{n}≡ proto_elim x y f2 p2.
Proof.
rewrite /proto_elim. intros Hf. revert p2.
destruct p1 as [|[a m] p1].
- intros p2 Hp. by inversion Hp.
- intros p2 Hp. destruct p2 as [|[a2 m2]]; [by inversion Hp|].
apply (fold_left_ne _ _ ((a, m) :: p1)); try done.
intros *. intros Ha Hx. destruct y1, y2. simpl in *.
destruct Hx. simpl in *. destruct H.
apply Hf; try done.
intros *. f_equiv. done.
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). Proof. 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. *)
(* Global Instance: Params (@iProto_app) 2 := {}. *)
(* Infix "<++>" := iProto_app (at level 60) : proto_scope. *)
(* Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_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). Proof. 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. *)
(* Global Instance: Params (@iProto_dual) 2 := {}. *)
(* Notation iMsg_dual := (iMsg_map iProto_dual). *)
(* Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V := *)
(* if d then iProto_dual p else p. *)
(* Arguments iProto_dual_if {_ _} _ _%_proto. *)
(* Global Instance: Params (@iProto_dual_if) 3 := {}. *)
Lemma proto_elim_end {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x y : A) (f : A → action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) :
proto_elim x y f proto_end ≡ x.
Proof. done. Qed.
Lemma proto_elim_message {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x y : A) (f : A → action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) (a:action) m :
(Proper ((≡) ==> (=) ==> (pointwise_relation _ (≡)) ==> (≡)) f) →
proto_elim x y f (proto_message a m) ≡ f y a m.
Proof.
intros. rewrite /proto_elim /proto_message /=. f_equiv=> v p /=. f_equiv.
rewrite -later_map_compose -{2}(later_map_id p).
apply later_map_ext=> p' /=. by rewrite proto_fold_unfold.
Qed.
(* TODO: Consider using cons over union *)
Lemma proto_elim_union {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x y : A) (f : A → action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) p1 p2 :
(Proper ((≡) ==> (=) ==> (pointwise_relation _ (≡)) ==> (≡)) f) →
proto_elim x y f (proto_union p1 p2) ≡ proto_elim x (proto_elim x y f p1) f p2 .
Proof. Admitted.
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 p,
proto_elim p2 proto_end
(λ acc a (m : V → laterO (iProto Σ V) -n> iProp Σ),
proto_union
(proto_message (f a) (iMsg_car (iMsg_map rec (IMsg m)))) acc) p.
Next Obligation.
intros Σ V f p2 rec n p1 p1' Hp. apply proto_elim_ne=> // p1'' p2' m1 m2 Ha Hp' Hm.
apply proto_union_ne; [|done].
simpl.
apply proto_message_ne=> v p' /=. by repeat f_equiv.
Qed.
Global Arguments iProto_map_app_aux : simpl never.
Global 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. apply proto_elim_ne=> // p1' p2' m1 m2 Ha Hm Hf.
f_equiv; [|done].
apply pair_ne; [solve_proper|].
intros v m. simpl.
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). Proof. 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.
Global Instance: Params (@iProto_app) 2 := {}.
Infix "<++>" := iProto_app (at level 60) : proto_scope.
Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope.
Lemma iProto_app_unfold {Σ V} (p1 p2 : iProto Σ V) :
iProto_app p1 p2 ≡ iProto_map_app_aux id p2 (iProto_map_app id p2) p1.
Proof. rewrite iProto_app_eq. rewrite /iProto_app_def /iProto_map_app.
apply: (fixpoint_unfold (iProto_map_app_aux id p2)). Qed.
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). Proof. 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.
Global Instance: Params (@iProto_dual) 2 := {}.
Notation iMsg_dual := (iMsg_map iProto_dual).
Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
if d then iProto_dual p else p.
Arguments iProto_dual_if {_ _} _ _%_proto.
Global Instance: Params (@iProto_dual_if) 3 := {}.
(** * Proofs *)
Section proto.
......@@ -194,11 +288,19 @@ Section proto.
Implicit Types m : iMsg Σ V.
(** ** Equality *)
Lemma iProto_case p : p ≡ END ∨ ∃ t n m ps, p ≡ proto_union (iProto_message (t, n) m) ps.
Proof.
(* rewrite iProto_end_eq. destruct p. left. done. right. *)
(* eexists _, (IMsg <$> p). done. *)
(* done. done. *)
destruct (proto_case p) as [|([t n] & m & ps & Hps)]; [left; by rewrite iProto_end_eq|].
right. exists t, n, (IMsg m), ps. rewrite iProto_message_eq. done.
Qed.
(* Lemma iProto_case p : p ≡ END ∨ ∃ t n m, p ≡ <(t,n)> m. *)
(* Proof. *)
(* rewrite iProto_message_eq iProto_end_eq. *)
(* destruct (proto_case p) as [|([a n]&m&?)]; [by left|right]. *)
(* by exists a, n, (IMsg m). *)
(* exists a, n, (IMsg m). *)
(* Qed. *)
Lemma iProto_message_equivI a1 a2 m1 m2 :
(<a1> m1) ≡ (<a2> m2) ⊣⊢@{iProp Σ} ⌜ a1 = a2 ⌝ ∧
......@@ -316,36 +418,36 @@ Section proto.
Qed.
(** ** Dual *)
(* Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V). *)
(* 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). *)
(* Proof. apply (ne_proper _). Qed. *)
(* Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END. *)
(* Proof. *)
(* rewrite iProto_end_eq iProto_dual_eq /iProto_dual_def /iProto_map_app. *)
(* etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl. *)
(* by rewrite proto_elim_end. *)
(* Qed. *)
(* Lemma iProto_dual_message a m : *)
(* iProto_dual (<a> m) ≡ <action_dual a> iMsg_dual m. *)
(* Proof. *)
(* rewrite iProto_message_eq iProto_dual_eq /iProto_dual_def /iProto_map_app. *)
(* etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl. *)
(* rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|]. *)
(* intros a' m1 m2 Hm; f_equiv; solve_proper. *)
(* Qed. *)
(* Lemma iMsg_dual_base v P p : *)
(* iMsg_dual (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; iProto_dual p)%msg. *)
(* Proof. apply iMsg_map_base, _. Qed. *)
(* Lemma iMsg_dual_exist {A} (m : A → iMsg Σ V) : *)
(* iMsg_dual (∃ x, m x) ≡ (∃ x, iMsg_dual (m x))%msg. *)
(* Proof. apply iMsg_map_exist. Qed. *)
Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V).
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).
Proof. apply (ne_proper _). Qed.
Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END.
Proof.
rewrite iProto_end_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
by rewrite proto_elim_end.
Qed.
Lemma iProto_dual_message a m :
iProto_dual (<a> m) ≡ <action_dual a> iMsg_dual m.
Proof.
rewrite iProto_message_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
intros p1 p2 Hp a' ? <- m1 m2 Hm. f_equiv; [|done]. f_equiv. solve_proper.
Qed.
Lemma iMsg_dual_base v P p :
iMsg_dual (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; iProto_dual p)%msg.
Proof. apply iMsg_map_base, _. Qed.
Lemma iMsg_dual_exist {A} (m : A → iMsg Σ V) :
iMsg_dual (∃ x, m x) ≡ (∃ x, iMsg_dual (m x))%msg.
Proof. apply iMsg_map_exist. Qed.
(* Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ V). *)
(* Proof. *)
......@@ -363,43 +465,60 @@ Section proto.
(* rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p''). *)
(* Qed. *)
(* (** ** Append *) *)
(* Global Instance iProto_app_end_l : LeftId (≡) END (@iProto_app Σ V). *)
(* Proof. *)
(* intros p. rewrite iProto_end_eq iProto_app_eq /iProto_app_def /iProto_map_app. *)
(* etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl. *)
(* by rewrite proto_elim_end. *)
(* Qed. *)
(* Lemma iProto_app_message a m p2 : (<a> m) <++> p2 ≡ <a> m <++> p2. *)
(* Proof. *)
(* rewrite iProto_message_eq iProto_app_eq /iProto_app_def /iProto_map_app. *)
(* etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl. *)
(* rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|]. *)
(* intros a' m1 m2 Hm. f_equiv; solve_proper. *)
(** ** Append *)
Global Instance iProto_app_end_l : LeftId (≡) END (@iProto_app Σ V).
Proof.
intros p. rewrite iProto_end_eq iProto_app_eq /iProto_app_def /iProto_map_app.
etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
by rewrite proto_elim_end.
Qed.
Lemma iProto_app_message a m p : (<a> m) <++> p ≡ <a> m <++> p.
Proof.
rewrite iProto_message_eq iProto_app_eq /iProto_app_def /iProto_map_app.
etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|].
rewrite /iProto_message_def. simpl.
rewrite ->proto_elim_message; [done|].
intros p1 p2 Hp a1 a2 Ha m1 m2 Hm. f_equiv; [|solve_proper].
f_equiv; [done|]. solve_proper.
Qed.
Lemma iProto_app_union p1 p2 p :
p1 ≠ END → p2 ≠ END →
(proto_union p1 p2) <++> p ≡ proto_union (p1 <++> p) (p2 <++> p).
Proof. Admitted.
(* rewrite iProto_app_eq /iProto_app_def /iProto_map_app. *)
(* (* rewrite iProto_message_eq iProto_app_eq /iProto_app_def /iProto_map_app. *) *)
(* etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]. *)
(* simpl. *)
(* rewrite ->proto_elim_union. *)
(* { rewrite /proto_elim. induction p2; [simpl|]. *)
(* { rewrite /proto_union. } *)
(* intros p1' p2' Hp a1 a2 Ha m1 m2 Hm. f_equiv; [|solve_proper]. *)
(* f_equiv; [done|]. solve_proper. *)
(* Qed. *)
(* Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V). *)
(* 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. *)
Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
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.
Admitted.
(* destruct (iProto_case p1) as [->|(a&i&m&->)]. *)
(* { by rewrite !left_id. } *)
(* rewrite !iProto_app_message. f_equiv=> v p' /=. do 4 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. *)
Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
Proof. apply (ne_proper_2 _). Qed.
(* Lemma iMsg_app_base v P p1 p2 : *)
(* ((MSG v {{ P }}; p1) <++> p2)%msg ≡ (MSG v {{ P }}; p1 <++> p2)%msg. *)
(* Proof. apply: iMsg_map_base. Qed. *)
(* Lemma iMsg_app_exist {A} (m : A → iMsg Σ V) p2 : *)
(* ((∃ x, m x) <++> p2)%msg ≡ (∃ x, m x <++> p2)%msg. *)
(* Proof. apply iMsg_map_exist. Qed. *)
Lemma iMsg_app_base v P p1 p2 :
((MSG v {{ P }}; p1) <++> p2)%msg ≡ (MSG v {{ P }}; p1 <++> p2)%msg.
Proof. apply: iMsg_map_base. Qed.
Lemma iMsg_app_exist {A} (m : A → iMsg Σ V) p2 :
((∃ x, m x) <++> p2)%msg ≡ (∃ x, m x <++> p2)%msg.
Proof. apply iMsg_map_exist. Qed.
(* Global Instance iProto_app_end_r : RightId (≡) END (@iProto_app Σ V). *)
(* Proof. *)
......@@ -447,7 +566,7 @@ Section proto.
(* iExists (p1d <++> p2). iSplitL; [by auto|]. *)
(* iRewrite "Hp12". iIntros "!>". iRewrite "Hp1'". by iRewrite ("IH" $! p1d p2). *)
(* Qed. *)
End proto.
Global Instance iProto_inhabited {Σ V} : Inhabited (iProto Σ V) := populate END.
......
multris/channel/proto_model.v
+ 162
− 130
View file @ 79b59cb3
......@@ -64,12 +64,12 @@ Module Export action.
Proof. by intros [[]]. Qed.
End action.
Notation proto_aux V PROP A :=
(gmap action (V -d> laterO A -n> PROP)).
Notation proto_auxO V PROP A :=
(gmapO actionO (V -d> laterO A -n> PROP)).
Definition proto_aux V PROP A :=
(list (prod action (V -d> laterO A -n> PROP))).
Definition proto_auxO V PROP A :=
(listO (prod actionO (V -d> laterO A -n> PROP))).
Definition proto_auxOF V PROP :=
(gmapOF actionO ((V -d> ▶ ∙ -n> PROP))).
(listOF (actionO * ((V -d> ▶ ∙ -n> PROP)))).
Definition proto_result (V : Type) := result_2 (proto_auxOF V).
Definition pre_protoO (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
......@@ -105,25 +105,29 @@ Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP}
proto_unfold (proto_fold p) ≡ p.
Proof. apply (ofe_iso_12 proto_iso). Qed.
Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP := ∅ .
Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP := [].
Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
(m : V -d> later (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
({[a := (λ v, m v ◎ laterO_map proto_fold)]}).
([(a,(λ v, m v ◎ laterO_map proto_fold))]).
Definition proto_union {V} `{!Cofe PROPn, !Cofe PROP} (p1 p2 : proto V PROPn PROP) : proto V PROPn PROP :=
(p1:gmap _ _) ∪ p2.
p1 ++ p2.
Global 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.
apply insert_ne; [|done]. solve_proper.
intros c1 c2 Hc. rewrite /proto_message. simpl.
f_equiv.
- apply pair_ne.
+ done.
+ solve_proper.
- done.
Qed.
Global 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. apply: insert_proper; [|done]. solve_proper.
Proof. intros c1 c2 Hc. rewrite /proto_message. repeat f_equiv. solve_proper.
Qed.
Global Instance proto_union_ne {V} `{!Cofe PROPn, !Cofe PROP} n :
......@@ -141,176 +145,200 @@ Proof.
intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. by f_equiv.
Qed.
(* Should hold in the same way map_ind holds *)
(* TODO: This is FALSE *)
Lemma proto_ind {V} `{!Cofe PROPn, !Cofe PROP} (P : proto V PROPn PROP → Prop) :
Proper ((≡) ==> impl) P →
P proto_end → (∀ i x p, p !! i ≡ None → P p → P (proto_union (proto_message i x) p)) → ∀ m, P m.
Proof.
intros HP ? Hins m.
induction (map_wf m) as [m _ IH].
destruct (map_choose_or_empty m) as [(i&x&?)| H'].
{
assert (m ≡ proto_union (proto_message i (λ v, x v ◎ laterO_map proto_unfold)) (delete i m)) as Heq.
{
rewrite /proto_message /proto_union.
rewrite -insert_union_singleton_l.
intros i'.
(* TODO: Simplify *)
destruct (decide (i=i')) as [->|].
{ rewrite H0. rewrite lookup_insert. f_equiv.
intros v.
intros x''.
simpl.
rewrite -later_map_compose.
simpl. f_equiv.
destruct x''.
rewrite later_map_Next. f_equiv.
simpl. rewrite proto_unfold_fold. done. }
rewrite lookup_insert_ne; [|done].
by rewrite lookup_delete_ne. }
rewrite Heq.
apply Hins.
{ by rewrite lookup_delete. }
eapply IH. by apply: delete_subset.
}
rewrite /proto_end in H.
by rewrite -H' in H.
Qed.
P proto_end → (∀ i x p, p ≡ [] → P p → P (proto_union (proto_message i x) p)) → ∀ m, P m.
(* Proof. *)
(* (* Should hold in the same way map_ind holds *) *)
(* Lemma proto_ind {V} `{!Cofe PROPn, !Cofe PROP} (P : proto V PROPn PROP → Prop) : *)
(* Proper ((≡) ==> impl) P → *)
(* P proto_end → (∀ i x p, p !! i ≡ None → P p → P (proto_union (proto_message i x) p)) → ∀ m, P m. *)
(* Proof. *)
(* intros HP ? Hins m. *)
(* induction (map_wf m) as [m _ IH]. *)
(* destruct (map_choose_or_empty m) as [(i&x&?)| H']. *)
(* { *)
(* assert (m ≡ proto_union (proto_message i (λ v, x v ◎ laterO_map proto_unfold)) (delete i m)) as Heq. *)
(* { *)
(* rewrite /proto_message /proto_union. *)
(* rewrite -insert_union_singleton_l. *)
(* intros i'. *)
(* (* TODO: Simplify *) *)
(* destruct (decide (i=i')) as [->|]. *)
(* { rewrite H0. rewrite lookup_insert. f_equiv. *)
(* intros v. *)
(* intros x''. *)
(* simpl. *)
(* rewrite -later_map_compose. *)
(* simpl. f_equiv. *)
(* destruct x''. *)
(* rewrite later_map_Next. f_equiv. *)
(* simpl. rewrite proto_unfold_fold. done. } *)
(* rewrite lookup_insert_ne; [|done]. *)
(* by rewrite lookup_delete_ne. } *)
(* rewrite Heq. *)
(* apply Hins. *)
(* { by rewrite lookup_delete. } *)
(* eapply IH. by apply: delete_subset. *)
(* } *)
(* rewrite /proto_end in H. *)
(* by rewrite -H' in H. *)
(* Qed. *)
Admitted.
Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
p ≡ proto_end ∨ ∃ a m p', p ≡ proto_union (proto_message a m) p'.
Proof. Admitted.
(* destruct (proto_unfold p) as [[a m]|] eqn:E; simpl in *; last first. *)
(* - left. by rewrite -(proto_fold_unfold p) E. *)
(* - right. exists a, m. by rewrite /proto_message -E proto_fold_unfold. *)
(* Qed. *)
Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
Inhabited (proto V PROPn PROP) := populate proto_end.
Lemma proto_message_equivI {Σ} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 m1 ≡ proto_message a2 m2
⊣⊢@{iProp Σ} ⌜ a1 = a2 ⌝ ∧ (∀ v p', m1 v p' ≡ m2 v p').
Proof.
rewrite /proto_message gmap_equivI /=.
iSplit.
{ destruct (decide (a1=a2)) as [->|Hne]; last first.
{ iIntros "H". iSpecialize ("H" $! a1).
rewrite lookup_insert. rewrite lookup_insert_ne; [|done].
by rewrite option_equivI. }
iIntros "H". iSpecialize ("H" $! a2).
rewrite !lookup_insert option_equivI.
iSplit; [done|].
iIntros (v p). rewrite discrete_fun_equivI.
iSpecialize ("H" $! v).
rewrite ofe_morO_equivI=> /=.
iSpecialize ("H" $! (laterO_map proto_unfold p)).
assert (p ≡ later_map proto_fold (later_map proto_unfold p)) as <-; last by done.
rewrite -later_map_compose. rewrite -(later_map_id p).
apply later_map_ext=> p' /=. by rewrite proto_fold_unfold. }
iIntros "[%Heq H2]" (i). rewrite Heq.
destruct (decide (a2 = i)) as [->|Hneq]; [|by rewrite !lookup_insert_ne].
rewrite !lookup_insert option_equivI discrete_fun_equivI.
iIntros (v). rewrite ofe_morO_equivI. by iIntros (p).
Qed.
Proof. Admitted.
(* rewrite /proto_message list_equivI /=. *)
(* iSplit. *)
(* { destruct (decide (a1=a2)) as [->|Hne]; last first. *)
(* { iIntros "H". iSpecialize ("H" $! 0). simpl. *)
(* rewrite option_equivI. rewrite prod_equivI. simpl. } *)
(* iIntros "H". iSpecialize ("H" $! a2). *)
(* rewrite !lookup_insert option_equivI. *)
(* iSplit; [done|]. *)
(* iIntros (v p). rewrite discrete_fun_equivI. *)
(* iSpecialize ("H" $! v). *)
(* rewrite ofe_morO_equivI=> /=. *)
(* iSpecialize ("H" $! (laterO_map proto_unfold p)). *)
(* assert (p ≡ later_map proto_fold (later_map proto_unfold p)) as <-; last by done. *)
(* rewrite -later_map_compose. rewrite -(later_map_id p). *)
(* apply later_map_ext=> p' /=. by rewrite proto_fold_unfold. } *)
(* iIntros "[%Heq H2]" (i). rewrite Heq. *)
(* destruct (decide (a2 = i)) as [->|Hneq]; [|by rewrite !lookup_insert_ne]. *)
(* rewrite !lookup_insert option_equivI discrete_fun_equivI. *)
(* iIntros (v). rewrite ofe_morO_equivI. by iIntros (p). *)
(* Qed. *)
Lemma proto_message_end_equivI {Σ} {V} `{!Cofe PROPn, !Cofe PROP} a m :
proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ≡ proto_end ⊢@{iProp Σ} False.
Proof.
rewrite /proto_message /proto_end. rewrite gmap_equivI.
iIntros "H". iSpecialize ("H" $! a). rewrite lookup_insert. rewrite lookup_empty.
by rewrite option_equivI.
Qed.
Proof. Admitted.
(* rewrite /proto_message /proto_end. rewrite gmap_equivI. *)
(* iIntros "H". iSpecialize ("H" $! a). rewrite lookup_insert. rewrite lookup_empty. *)
(* by rewrite option_equivI. *)
(* Qed. *)
Lemma proto_end_message_equivI {Σ} {V} `{!Cofe PROPn, !Cofe PROP} a m :
proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ⊢@{iProp Σ} False.
Proof. by rewrite internal_eq_sym proto_message_end_equivI. Qed.
(* Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A} *)
(* (x : A) (f : A → action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) *)
(* (p : proto V PROPn PROP) : A := *)
(* match p with *)
(* | [] => x *)
(* | p' => fold_left (λ acc am, f acc am.1 (λ v, am.2 v ◎ laterO_map proto_unfold)) p' x *)
(* end. *)
(* Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe} *)
(* (x : A) (f1 f2 : A → action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) p1 p2 n : *)
(* (∀ x a m1 m2, (∀ v, m1 v ≡{n}≡ m2 v) → f1 x a m1 ≡{n}≡ f2 x a m2) → *)
(* p1 ≡{n}≡ p2 → *)
(* proto_elim x f1 p1 ≡{n}≡ proto_elim x f2 p2. *)
(* Proof. Admitted. *)
(** Functor *)
(* Program Definition proto_map_aux {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} *)
(* (g : PROP -n> PROP') (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) : *)
(* proto V PROPn PROP -n> proto V PROPn' PROP' := λne p, *)
(* proto_elim proto_end (λ acc a m, proto_union acc $ proto_message a (λ v, g ◎ m v ◎ laterO_map rec)) p. *)
(* Next Obligation. *)
(* intros V PROPn ? PROPn' ? PROP ? PROP' ? g rec n p1 p2 Hp. *)
(* apply proto_elim_ne. *)
(* - intros. repeat f_equiv. done. *)
(* - done. *)
(* Qed. *)
Program Definition proto_map_aux {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(g : PROP -n> PROP') (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) :
(f : action → action) (g : PROP -n> PROP') (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) :
proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
(λ m, λ v, g ◎ m v ◎ laterO_map proto_unfold ◎ laterO_map rec ◎ laterO_map proto_fold) <$> p.
(λ am, (f am.1, λ v, g ◎ am.2 v ◎ laterO_map proto_unfold ◎ laterO_map rec ◎ laterO_map proto_fold)) <$> p.
Next Obligation.
intros V PROPn ? PROPn' ? PROP ? PROP' ? g rec n p1 p2 Hp.
apply: (map_fmap_ne _ n _ p1 p2); [|done].
solve_proper.
intros V PROPn ? PROPn' ? PROP ? PROP' ? f g rec n p1 p2 Hp.
apply: (list_fmap_ne n _ _ _ p1 p2); [|done].
intros [a1 m1] [a2 m2] [Haeq Hmeq]. simpl in *.
apply pair_ne; solve_proper.
Qed.
Global Instance proto_map_aux_contractive {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} (g : PROP -n> PROP') :
Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') g).
Proof.
intros n p1 p2 Hp. rewrite /proto_map_aux.
intros p. simpl.
apply: gmap_fmap_ne_ext.
intros i x Hix v. f_equiv. f_equiv. f_contractive.
done.
Qed.
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} f (g : PROP -n> PROP') :
Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') f g).
Proof. Admitted.
Definition proto_map_aux_2 {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP')
f (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' :=
proto_map_aux g (proto_map_aux gn rec).
proto_map_aux f g (proto_map_aux f gn rec).
Global Instance proto_map_aux_2_contractive {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
Contractive (proto_map_aux_2 (V:=V) gn g).
f (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
Contractive (proto_map_aux_2 (V:=V) f gn g).
Proof.
intros n rec1 rec2 Hrec. rewrite /proto_map_aux_2.
f_equiv. by apply proto_map_aux_contractive.
Qed.
Definition proto_map {V}
`{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
f (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
proto V PROPn PROP -n> proto V PROPn' PROP' :=
fixpoint (proto_map_aux_2 gn g).
fixpoint (proto_map_aux_2 f gn g).
Lemma proto_map_unfold {V}
`{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p :
proto_map (V:=V) gn g p ≡ proto_map_aux g (proto_map g gn) p.
(f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p :
proto_map (V:=V) f gn g p ≡ proto_map_aux f g (proto_map f g gn) p.
Proof.
apply equiv_dist=> n. revert PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
induction (lt_wf n) as [n _ IH]=>
PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 f gn g))|].
apply proto_map_aux_contractive; constructor=> n' ?. symmetry. apply: IH. lia.
Qed.
Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
proto_map (V:=V) gn g proto_end ≡ proto_end.
f (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_map_aux /=.
done.
Qed.
Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a m :
proto_map (V:=V) gn g (proto_message a m)
≡ proto_message a (λ v, g ◎ m v ◎ laterO_map (proto_map g gn)).
f (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a m :
proto_map (V:=V) f gn g (proto_message a m)
≡ proto_message (f a) (λ v, g ◎ m v ◎ laterO_map (proto_map f g gn)).
Proof.
rewrite proto_map_unfold /proto_map_aux /=.
rewrite /proto_message.
rewrite fmap_insert. rewrite fmap_empty.
intros a'. destruct (decide (a=a')).
{ subst. rewrite !lookup_insert.
f_equiv.
intros v. f_equiv. f_equiv.
intros x. simpl. f_equiv. f_equiv.
intros y. simpl. rewrite proto_fold_unfold. done.
}
by rewrite !lookup_insert_ne.
rewrite /proto_message. f_equiv. f_equiv. intros v. simpl. repeat f_equiv.
intros m'. simpl. repeat f_equiv. rewrite -later_map_compose.
destruct m'. simpl. rewrite later_map_Next. simpl. rewrite proto_fold_unfold.
done.
Qed.
Lemma proto_map_union {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p1 p2 :
proto_map (V:=V) gn g (proto_union p1 p2)
≡ proto_union (proto_map gn g p1) (proto_map gn g p2).
f (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p1 p2 :
proto_map (V:=V) f gn g (proto_union p1 p2)
≡ proto_union (proto_map f gn g p1) (proto_map f gn g p2).
Proof.
rewrite proto_map_unfold /proto_map_aux /=.
rewrite proto_map_unfold /proto_map_aux /=.
rewrite proto_map_unfold /proto_map_aux /=.
rewrite !proto_map_unfold !/proto_map_aux /=.
rewrite !/proto_union.
rewrite !map_fmap_union.
f_equiv.
rewrite fmap_app. done.
Qed.
Lemma proto_map_ne {V}
`{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
(gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p n :
f (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p n :
gn1 ≡{n}≡ gn2 → g1 ≡{n}≡ g2 →
proto_map (V:=V) gn1 g1 p ≡{n}≡ proto_map (V:=V) gn2 g2 p.
proto_map (V:=V) f gn1 g1 p ≡{n}≡ proto_map (V:=V) f gn2 g2 p.
Proof.
revert PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn1 gn2 g1 g2 p.
induction (lt_wf n) as [n _ IH]=>
......@@ -319,29 +347,32 @@ Proof.
{ intros p1 p2 Hp H'. rewrite -Hp. done. }
{ rewrite !proto_map_end. done. }
intros a m p' Hp Hp'.
clear Hp. (* Make sure we dont abuse false assumption *)
rewrite !proto_map_union.
rewrite !proto_map_message /=.
apply proto_union_ne.
{ apply proto_message_ne => // v p'' /=. f_equiv; [done|]. f_equiv.
apply proto_union_ne; [|done].
{ rewrite !proto_map_message /=.
apply proto_message_ne => // v p'' /=. f_equiv; [done|]. f_equiv.
apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_le with lia. }
done.
Qed.
Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
gn1 ≡ gn2 → g1 ≡ g2 → proto_map (V:=V) gn1 g1 p ≡ proto_map (V:=V) gn2 g2 p.
(gn1 gn2 : PROPn' -n> PROPn) f (g1 g2 : PROP -n> PROP') p :
gn1 ≡ gn2 → g1 ≡ g2 → proto_map (V:=V) f gn1 g1 p ≡ proto_map (V:=V) f gn2 g2 p.
Proof.
intros Hgn Hg. apply equiv_dist=> n.
apply proto_map_ne=> // ?; by apply equiv_dist.
Qed.
Lemma proto_map_id {V} `{Hcn:!Cofe PROPn, Hc:!Cofe PROP} (p : proto V PROPn PROP) :
proto_map cid cid p ≡ p.
proto_map id cid cid p ≡ p.
Proof.
apply equiv_dist=> n. revert PROPn Hcn PROP Hc p.
induction (lt_wf n) as [n _ IH]=> PROPn ? PROP ? p /=.
pattern p. apply proto_ind.
pattern p.
(* induction p. *)
apply proto_ind.
{ intros p1 p2 Hp H'. rewrite -Hp. done. }
{ rewrite !proto_map_end. done. }
intros a m p' Hp Hp'.
clear Hp. (* Make sure we dont use false assumption *)
rewrite proto_map_union. f_equiv.
{ rewrite !proto_map_message /=. apply proto_message_ne=> // v p'' /=. f_equiv.
apply Next_contractive; dist_later_intro as n' Hn'; auto. }
......@@ -352,7 +383,7 @@ Lemma proto_map_compose {V}
Hc:!Cofe PROP, Hc':!Cofe PROP', Hc'':!Cofe PROP''}
(gn1 : PROPn'' -n> PROPn') (gn2 : PROPn' -n> PROPn)
(g1 : PROP -n> PROP') (g2 : PROP' -n> PROP'') (p : proto V PROPn PROP) :
proto_map (gn2 ◎ gn1) (g2 ◎ g1) p ≡ proto_map gn1 g2 (proto_map gn2 g1 p).
proto_map id (gn2 ◎ gn1) (g2 ◎ g1) p ≡ proto_map id gn1 g2 (proto_map id gn2 g1 p).
Proof.
apply equiv_dist=> n. revert PROPn Hcn PROPn' Hcn' PROPn'' Hcn''
PROP Hc PROP' Hc' PROP'' Hc'' gn1 gn2 g1 g2 p.
......@@ -362,6 +393,7 @@ Proof.
{ intros p1 p2 Hp H'. rewrite -Hp. done. }
{ rewrite !proto_map_end. done. }
intros a m p' Hp Hp'.
clear Hp. (* Make sure we dont use false assumption *)
rewrite !proto_map_union. f_equiv.
{ rewrite !proto_map_message /=. apply proto_message_ne=> // v p'' /=. do 3 f_equiv.
apply Next_contractive; dist_later_intro as n' Hn'; auto. }
......@@ -373,7 +405,7 @@ Program Definition protoOF (V : Type) (Fn F : oFunctor)
`{!∀ 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 (oFunctor_map Fn (fg.2, fg.1)) (oFunctor_map F 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 *.
......
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