WIP: Lifting proto_model to a map of protocols

multris/channel/proto_model.v

@@ -34,6 +34,8 @@ The defined functions on the type [proto] are:
   a given protocol.
 - [proto_app], which appends two protocols [p1] and [p2], by substituting
   all terminations [END] in [p1] with [p2]. *)
+From stdpp Require Import gmap.
+From iris.algebra Require Import gmap.
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import proofmode.
 From multris.utils Require Import cofe_solver_2.
@@ -41,19 +43,30 @@ Set Default Proof Using "Type".
 
 Module Export action.
   Inductive tag := Send | Recv.
+  Canonical Structure tagO := leibnizO tag.
+  Global Instance tag_decidable : EqDecision tag.
+  Proof. solve_decision. Qed.
+  Global Program Instance tag_countable : Countable tag :=
+     {|
+  encode t := match t with | Send => 1%positive | Recv => 2%positive end;
+  decode p := Some match p return tag with 1%positive => Send | _ => Recv end
+     |}.
+  Next Obligation. by intros []. Qed.
   Definition action : Set := tag * nat.
   Global Instance action_inhabited : Inhabited action := populate (Send,0).
+  Canonical Structure actionO := leibnizO action.
+  Global Instance action_countable : Countable action.
+  Proof. unfold action. apply prod_countable. Qed.
   Definition action_dual (a : action) : action :=
     match a with (Send, n) => (Recv, n) | (Recv, n) => (Send, n) end.
   Global Instance action_dual_involutive : Involutive (=) action_dual.
   Proof. by intros [[]]. Qed.
-  Canonical Structure actionO := leibnizO action.
 End action.
 
 Definition proto_auxO (V : Type) (PROP : ofe) (A : ofe) : ofe :=
-  optionO (prodO actionO (V -d> laterO A -n> PROP)).
+  (gmapO actionO (V -d> laterO A -n> PROP)).
 Definition proto_auxOF (V : Type) (PROP : ofe) : oFunctor :=
-  optionOF (actionO * (V -d> ▶ ∙ -n> PROP)).
+  (gmapOF actionO ((V -d> ▶ ∙ -n> PROP))).
 
 Definition proto_result (V : Type) := result_2 (proto_auxOF V).
 Definition proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
@@ -77,30 +90,95 @@ Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP}
 Proof. apply (ofe_iso_21 proto_iso). Qed.
 
 Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP :=
-  proto_fold None.
+  proto_fold ∅ .
 Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
     (m : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
-  proto_fold (Some (a, m)).
+  proto_fold {[a := m]}.
+Definition proto_union {V} `{!Cofe PROPn, !Cofe PROP} (p1 p2 : proto V PROPn PROP) : proto V PROPn PROP :=
+  proto_fold (map_union (proto_unfold p1) (proto_unfold 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. f_equiv. by repeat constructor. Qed.
+Proof.
+  intros c1 c2 Hc. rewrite /proto_message. f_equiv. by apply insert_ne.
+Qed.
+
+(* TODO: Why does unification algorithm fail here? *)
 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. f_equiv. by repeat constructor. Qed.
+Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by apply: insert_proper. Qed.
 
-Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
-  p ≡ proto_end ∨ ∃ a m, p ≡ proto_message a m.
+Global Instance proto_union_ne {V} `{!Cofe PROPn, !Cofe PROP} n :
+  Proper ((dist n) ==> (dist n) ==> dist n)
+         (proto_union (V:=V) (PROPn:=PROPn) (PROP:=PROP)).
 Proof.
-  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.
+  intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. by do 3 f_equiv.
 Qed.
+
+(* TODO: Why does unification algorithm fail here? *)
+Global Instance proto_union_proper {V} `{!Cofe PROPn, !Cofe PROP} :
+  Proper ((≡) ==> (≡) ==> (≡))
+         (proto_union (V:=V) (PROPn:=PROPn) (PROP:=PROP)).
+Proof.
+  intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. f_equiv.
+  (* TODO: Proper stuff *)
+Admitted.
+
+(* 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, proto_unfold p !! i ≡ None → P p → P (proto_union (proto_message i x) p)) → ∀ m, P m.
+Proof.
+  intros HP ? Hins m'.  
+  assert (∃ m, m = proto_unfold m') as [m Hm].
+  { eexists _. done. }
+  revert Hm. revert m'.
+  induction (map_wf m) as [m _ IH].
+  intros m' Hm.
+  destruct (map_choose_or_empty m) as [(i&x&?)| H'].
+  {
+    assert (m' = proto_union (proto_message i x) (proto_fold (delete i (proto_unfold m')))).
+    { admit. }
+    rewrite H1.
+    apply Hins.
+    { admit. }                  (* TODO Map lookup proper stuff *)
+    eapply IH; [|done].
+    admit.                      (* TODO: Proper subset stuff *)
+  }
+  rewrite /proto_end in H.
+  subst.
+  rewrite -H' in H.
+  rewrite -(proto_fold_unfold m'). done.
+Admitted.
+
 Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
   Inhabited (proto V PROPn PROP) := populate proto_end.
 
+(* Derived laws *)
+Section internal_eq_derived.
+  Context {PROP : bi} `{!BiInternalEq PROP}.
+  Implicit Types P : PROP.
+
+  (* Force implicit argument PROP *)
+  Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+  Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
+
+  Lemma gmap_equivI `{Countable K} {A : ofe} (m1 m2 : gmap K A) :
+    m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
+  Proof. Admitted.
+
+  Lemma gmap_union_equiv_eqI  `{Countable K} {A : ofe} (m m1 m2 : gmap K A) :
+    m ≡ m1 ∪ m2 ⊣⊢ ∃ m1' m2', ⌜ m = m1' ∪ m2' ⌝ ∧ m1' ≡ m1 ∧ m2' ≡ m2.
+  Proof. Admitted.
+    
+  Lemma gmap_singleton_equivI  `{Countable K} {A : ofe} (k1 k2 : K) (a1 a2 : A) :
+    {[ k1 := a1 ]} ≡ {[ k2 := a2 ]} ⊣⊢ ⌜ k1 = k2 ⌝ ∧ a1 ≡ a2.
+  Proof. Admitted.
+
+End internal_eq_derived.
+
 Lemma proto_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
   proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 m1 ≡ proto_message a2 m2
   ⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧ (∀ v p', m1 v p' ≡ m2 v p').
@@ -110,79 +188,52 @@ Proof.
     - 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 option_equivI prod_equivI /=.
-  rewrite discrete_eq discrete_fun_equivI.
+  rewrite /proto_message !proto_unfold_fold.
+  rewrite gmap_singleton_equivI /=.
+  rewrite discrete_fun_equivI.  
   by setoid_rewrite ofe_morO_equivI.
 Qed.
+
 Lemma proto_message_end_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
   proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ≡ proto_end ⊢@{SPROP} False.
 Proof.
   trans (proto_unfold (proto_message a m) ≡ proto_unfold proto_end : SPROP)%I.
-  { iIntros "Heq". by iRewrite "Heq". }
-  by rewrite /proto_message !proto_unfold_fold option_equivI.
-Qed.
+  { iIntros "Heq". by iRewrite "Heq". }  
+  rewrite /proto_message !proto_unfold_fold.
+  rewrite gmap_equivI.
+Admitted.
 Lemma proto_end_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
   proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ⊢@{SPROP} False.
 Proof. by rewrite internal_eq_sym proto_message_end_equivI. Qed.
 
-(** The eliminator [proto_elim x f p] is only well-behaved if the function [f]
-is contractive *)
-Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A}
-    (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
-    (p : proto V PROPn PROP) : A :=
-  match proto_unfold p with None => x | Some (a, m) => f a m end.
-
-Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
-    (x : A) (f1 f2 : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) p1 p2 n :
-  (∀ a m1 m2, (∀ v, m1 v ≡{n}≡ m2 v) → f1 a m1 ≡{n}≡ f2 a m2) →
-  p1 ≡{n}≡ p2 →
-  proto_elim x f1 p1 ≡{n}≡ proto_elim x f2 p2.
-Proof.
-  intros Hf Hp. rewrite /proto_elim.
-  apply (_ : NonExpansive proto_unfold) in Hp
-    as [[a1 m1] [a2 m2] [-> ?]|]; simplify_eq/=; [|done].
-  apply Hf. destruct n; by simpl.
-Qed.
-
-Lemma proto_elim_end {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
-    (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) :
-  proto_elim x f proto_end ≡ x.
-Proof.
-  rewrite /proto_elim /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; inversion Hfold.
-Qed.
-Lemma proto_elim_message {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
-    (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
-    `{Hf : ∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)} a m :
-  proto_elim x f (proto_message a m) ≡ f a m.
-Proof.
-  rewrite /proto_elim /proto_message /=.
-  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn)
-    (PROP:=PROP) (Some (a, m))) as Hfold.
-  destruct (proto_unfold (proto_fold (Some (a, m))))
-    as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hc]|]; simplify_eq/=.
-  by f_equiv=> v.
-Qed.
 
 (** 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 (λ a m, proto_message a (λ v, g ◎ m v ◎ laterO_map rec)) p.
+  (* fmap (λ (m:proto V PROPn PROP), (λ v, g ◎ m v ◎ laterO_map rec)) (proto_unfold p). *)
+  (* proto_fold $ gmap_fmap _ _ (λ m, (λ v, g ◎ m v ◎ laterO_map rec)) (proto_unfold p). *)
+  proto_fold $ fmap (λ m, (λ v, g ◎ m v ◎ laterO_map rec)) (proto_unfold p).
 Next Obligation.
   intros V PROPn ? PROPn' ? PROP ? PROP' ? g rec n p1 p2 Hp.
-  apply proto_elim_ne=> // a m1 m2 Hm. by repeat f_equiv.
-Qed.
+  f_equiv. simpl.
+  apply (_ : NonExpansive proto_unfold) in Hp.
+Admitted.
+(* TODO: Needs non expansiveness of fmap *)
+(* (* Admitted. *) *)
+(*   apply map_fmap_ne. *)
+(*   apply gmap_fmap_ne_ext. *)
+(*   apply proto_elim_ne=> // a m1 m2 Hm. by repeat f_equiv. *)
+(* 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 rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a m1 m2 Hm.
-  f_equiv=> v p' /=. do 2 f_equiv; [done|].
-  apply Next_contractive; by dist_later_intro as n' Hn'.
-Qed.
+Proof. Admitted.
+(*   intros n rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a m1 m2 Hm. *)
+(*   f_equiv=> v p' /=. do 2 f_equiv; [done|]. *)
+(*   apply Next_contractive; by dist_later_intro as n' Hn'. *)
+(* Qed. *)
 
 Definition proto_map_aux_2 {V}
    `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
@@ -218,16 +269,24 @@ 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.
-Proof. by rewrite proto_map_unfold /proto_map_aux /= proto_elim_end. Qed.
+Proof.
+  rewrite proto_map_unfold /proto_map_aux /=.
+  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) ∅) as Hfold.
+Admitted.
 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)).
 Proof.
   rewrite proto_map_unfold /proto_map_aux /=.
-  rewrite ->proto_elim_message; [done|].
-  intros a' m1 m2 Hm. f_equiv; solve_proper.
-Qed.
+Admitted.
+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).
+Proof.
+  rewrite proto_map_unfold /proto_map_aux /=.
+Admitted.
 
 Lemma proto_map_ne {V}
     `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
@@ -237,11 +296,17 @@ Lemma proto_map_ne {V}
 Proof.
   revert PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn1 gn2 g1 g2 p.
   induction (lt_wf n) as [n _ IH]=>
-    PROPn ? PROPn' ? PROP ? PROP' ? gn1 gn2 g1 g2 p Hgn Hg /=.
-  destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
+              PROPn ? PROPn' ? PROP ? PROP' ? gn1 gn2 g1 g2 p Hgn Hg /=.
+  pattern p. apply proto_ind.
+  { intros p1 p2 Hp H'. rewrite -Hp. done. }
+  { rewrite !proto_map_end. done. }
+  intros a m p' Hp Hp'.
+  rewrite !proto_map_union.
   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.
+  apply proto_union_ne.
+  { 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 :
@@ -255,9 +320,14 @@ Lemma proto_map_id {V} `{Hcn:!Cofe PROPn, Hc:!Cofe PROP} (p : proto V PROPn PROP
 Proof.
   apply equiv_dist=> n. revert PROPn Hcn PROP Hc p.
   induction (lt_wf n) as [n _ IH]=> PROPn ? PROP ? p /=.
-  destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
-  rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=. f_equiv.
-  apply Next_contractive; dist_later_intro as n' Hn'; auto.
+    pattern p. apply proto_ind.
+  { intros p1 p2 Hp H'. rewrite -Hp. done. }
+  { rewrite !proto_map_end. done. }
+  intros a m p' Hp Hp'.
+  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. }
+  done.
 Qed.
 Lemma proto_map_compose {V}
    `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
@@ -265,14 +335,19 @@ Lemma proto_map_compose {V}
     (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).
-Proof.
+Proof.  
   apply equiv_dist=> n. revert PROPn Hcn PROPn' Hcn' PROPn'' Hcn''
     PROP Hc PROP' Hc' PROP'' Hc'' gn1 gn2 g1 g2 p.
   induction (lt_wf n) as [n _ IH]=> PROPn ? PROPn' ? PROPn'' ?
     PROP ? PROP' ? PROP'' ? gn1 gn2 g1 g2 p /=.
-  destruct (proto_case p) as [->|(a & c & ->)]; [by rewrite !proto_map_end|].
-  rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=.
-  do 3 f_equiv. apply Next_contractive; dist_later_intro as n' Hn'; simpl; auto.
+  pattern p. apply proto_ind.
+  { intros p1 p2 Hp H'. rewrite -Hp. done. }
+  { rewrite !proto_map_end. done. }
+  intros a m p' Hp Hp'.
+  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. }
+  done.
 Qed.
 
 Program Definition protoOF (V : Type) (Fn F : oFunctor)