diff --git a/multris/channel/proto.v b/multris/channel/proto.v
index 950d5f43e8bb68f3bd8e5726d39dc10a997965c2..8849b59948c1dfe7603ad3c6178fcd6e6cbd96cf 100644
--- a/multris/channel/proto.v
+++ b/multris/channel/proto.v
@@ -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.
diff --git a/multris/channel/proto_model.v b/multris/channel/proto_model.v
index c706776fe04507d862210b42352a8ea4fdf23fa2..2e112b1079861576bd6654526f24ba5ab315c0e2 100644
--- a/multris/channel/proto_model.v
+++ b/multris/channel/proto_model.v
@@ -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 *.