WIP: More admits resolved

multris/channel/proto_model.v

@@ -34,7 +34,6 @@ 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.
@@ -63,8 +62,12 @@ Module Export action.
   Proof. by intros [[]]. Qed.
 End action.
 
-Definition proto_auxO (V : Type) (PROP : ofe) (A : ofe) : ofe :=
-  (gmapO actionO (V -d> laterO A -n> PROP)).
+Notation proto_auxO V PROP A :=
+  (gmapO actionO (V -d> later A -n> PROP)).
+(* Notation proto_auxOF V PROP := *)
+(*   (gmapOF actionO ((V -d> ▶ ∙ -n> PROP))). *)
+(* Definition proto_auxO (V : Type) (PROP : ofe) (A : ofe) : ofe := *)
+(*   (gmapO actionO (V -d> laterO A -n> PROP)). *)
 Definition proto_auxOF (V : Type) (PROP : ofe) : oFunctor :=
   (gmapOF actionO ((V -d> ▶ ∙ -n> PROP))).
 
@@ -89,13 +92,52 @@ Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP}
   proto_unfold (proto_fold p) ≡ p.
 Proof. apply (ofe_iso_21 proto_iso). Qed.
 
+(* Derived laws *)
+Section internal_eq_derived.
+  Context {PROP : bi} `{!BiInternalEq PROP}.
+  Context `{Countable K} {A : ofe}.
+  Implicit Types P : PROP.
+
+  (* Force implicit argument PROP *)
+  Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+  Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
+
+  Lemma gmap_equivI (m1 m2 : gmap K A) :
+    m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
+  Proof. Admitted.
+
+  Lemma gmap_union_equiv_eqI (m m1 m2 : gmap K A) :
+    m ≡ m1 ∪ m2 ⊣⊢ ∃ m1' m2', ⌜ m = m1' ∪ m2' ⌝ ∧ m1' ≡ m1 ∧ m2' ≡ m2.
+  Proof. Admitted.
+
+  Lemma gmap_singleton_equivI (k1 k2 : K) (a1 a2 : A) :
+    {[ k1 := a1 ]} ≡ {[ k2 := a2 ]} ⊣⊢ ⌜ k1 = k2 ⌝ ∧ a1 ≡ a2.
+  Proof. Admitted.
+
+  Global Instance gmap_union : Union (gmap K A) := _.
+
+  Global Instance gmap_union_proper :
+    Proper ((≡) ==> (≡) ==> (≡)) (gmap_union).
+  Proof. intros m11 m12 Heq1 m21 m22 Heq2.
+  Admitted.
+
+  Global Instance gmap_sub : SubsetEq (gmap K A) := _.
+  Global Instance gmap_different : Difference (gmap K A) := _.
+  Global Instance gmap_union_partial_order : PartialOrder (gmap_sub) := _.
+  Global Instance gmap_subset_proper :
+    Proper ((≡) ==> (≡) ==> (≡)) (⊂@{gmap K A}).
+  Proof. intros m11 m12 Heq1 m21 m22 Heq2. Admitted.
+
+End internal_eq_derived.
+
 Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP :=
   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 {[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)).
+  (* proto_fold (map_union (proto_unfold p1) (proto_unfold p2)). *)
+  proto_fold ((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)
@@ -117,21 +159,17 @@ Proof.
   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.
+Proof. intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. solve_proper. Qed.
 
-(* Should hold in the same way map_ind holds *)
+(* TODO: Missing Proper stuff *)
 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'.  
+  intros HP ? Hins m'.
   assert (∃ m, m = proto_unfold m') as [m Hm].
   { eexists _. done. }
   revert Hm. revert m'.
@@ -139,46 +177,35 @@ Proof.
   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. }
+    assert (m' ≡ proto_union (proto_message i x) (proto_fold (delete i (proto_unfold m')))).
+    {
+      rewrite -Hm.
+      rewrite /proto_union /proto_message.
+      rewrite !proto_unfold_fold.
+      rewrite -(proto_fold_unfold m'). f_equiv.
+      rewrite -Hm.
+      rewrite -insert_union_singleton_l.
+      by rewrite insert_delete.
+    }
     rewrite H1.
     apply Hins.
-    { admit. }                  (* TODO Map lookup proper stuff *)
+    { rewrite -Hm.
+      rewrite lookup_proper; [|apply proto_unfold_fold].
+      by rewrite lookup_delete. }
     eapply IH; [|done].
-    admit.                      (* TODO: Proper subset stuff *)
+    rewrite -Hm.
+    rewrite proto_unfold_fold.
+    by apply: delete_subset.
   }
   rewrite /proto_end in H.
   subst.
   rewrite -H' in H.
   rewrite -(proto_fold_unfold m'). done.
-Admitted.
+Qed.
 
 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').
@@ -190,7 +217,7 @@ Proof.
       iRewrite "Heq". by rewrite proto_fold_unfold. }
   rewrite /proto_message !proto_unfold_fold.
   rewrite gmap_singleton_equivI /=.
-  rewrite discrete_fun_equivI.  
+  rewrite discrete_fun_equivI.
   by setoid_rewrite ofe_morO_equivI.
 Qed.
 
@@ -198,9 +225,8 @@ Lemma proto_message_end_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe P
   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". }  
+  { 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.
@@ -271,7 +297,12 @@ Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
   proto_map (V:=V) gn g proto_end ≡ proto_end.
 Proof.
   rewrite proto_map_unfold /proto_map_aux /=.
-  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) ∅) as Hfold.
+  (* pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) ∅) as Hfold. *)
+  rewrite /proto_end. f_equiv.
+  rewrite -(fmap_empty (λ (m : V → laterO (proto V PROP PROPn) -n> PROP) (v : V),
+                g ◎ m v ◎ laterO_map (proto_map g gn))).
+  f_equiv.
+  (* proto_unfold_fold not working ??? *)
 Admitted.
 Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a m :
@@ -279,6 +310,7 @@ Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'
   ≡ proto_message a (λ v, g ◎ m v ◎ laterO_map (proto_map g gn)).
 Proof.
   rewrite proto_map_unfold /proto_map_aux /=.
+  rewrite /proto_message. f_equiv.
 Admitted.
 Lemma proto_map_union {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p1 p2 :
@@ -335,7 +367,7 @@ 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'' ?
@@ -374,7 +406,7 @@ Qed.
 Global 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 Fn → oFunctorContractive F →
   oFunctorContractive (protoOF V Fn F).
 Proof.
   intros HFn HF A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.