WIP: Cleaned things up

multris/channel/proto_model.v

@@ -114,30 +114,22 @@ Section internal_eq_derived.
     {[ 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.
 
+Global Instance subseteq_proper `{Countable K} {A:Type} `{Equiv A} :
+  Proper ((≡@{gmap K A}) ==> (≡@{gmap K A}) ==> iff) (⊆).
+Proof. Admitted.
+Global Instance subset_proper `{Countable K} {A:Type} `{Equiv A} :
+  Proper ((≡@{gmap K A}) ==> (≡@{gmap K A}) ==> iff) (⊂).
+Proof. solve_proper. Qed.
+  
 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 ((proto_unfold p1) ∪ (proto_unfold p2)).
+  proto_fold (((proto_unfold p1):gmap _ _) ∪ (proto_unfold p2)).
 
 Global Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
   Proper (pointwise_relation V (dist n) ==> dist n)
@@ -177,30 +169,20 @@ 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')))).
+    assert (m' ≡ proto_union (proto_message i x) (proto_fold (delete i (proto_unfold m'))))
+      as Heq.
     {
-      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 -Hm /proto_union /proto_message !proto_unfold_fold -(proto_fold_unfold m').
+      f_equiv. rewrite -Hm -insert_union_singleton_l. by rewrite insert_delete.
     }
-    rewrite H1.
+    rewrite Heq.
     apply Hins.
-    { rewrite -Hm.
-      rewrite lookup_proper; [|apply proto_unfold_fold].
-      by rewrite lookup_delete. }
-    eapply IH; [|done].
-    rewrite -Hm.
-    rewrite proto_unfold_fold.
+    { rewrite -Hm lookup_proper; [|apply proto_unfold_fold]. by rewrite lookup_delete. }
+    eapply IH; [|done]. rewrite -Hm (proto_unfold_fold (delete i m)).
     by apply: delete_subset.
   }
   rewrite /proto_end in H.
-  subst.
-  rewrite -H' in H.
-  rewrite -(proto_fold_unfold m'). done.
+  rewrite Hm in H'. rewrite -H' in H. by rewrite -(proto_fold_unfold m').
 Qed.
 
 Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
@@ -216,6 +198,7 @@ Proof.
     - iIntros "Heq". rewrite -{2}(proto_fold_unfold (proto_message _ _)).
       iRewrite "Heq". by rewrite proto_fold_unfold. }
   rewrite /proto_message !proto_unfold_fold.
+  
   rewrite gmap_singleton_equivI /=.
   rewrite discrete_fun_equivI.
   by setoid_rewrite ofe_morO_equivI.