Drop `DiagNone` precondition of `lookup_merge` rule of `FinMap` interface.

theories/gmap.v

@@ -83,18 +83,18 @@ Global Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f '(GMap m Hm
   GMap (omap f m) (gmap_omap_wf f m Hm).
 Lemma gmap_merge_wf `{Countable K} {A B C}
     (f : option A → option B → option C) m1 m2 :
-  let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
-  gmap_wf K m1 → gmap_wf K m2 → gmap_wf K (merge f' m1 m2).
+  gmap_wf K m1 → gmap_wf K m2 → gmap_wf K (merge f m1 m2).
 Proof.
-  intros f'; unfold gmap_wf; rewrite !bool_decide_spec.
-  intros Hm1 Hm2 p z; rewrite lookup_merge by done; intros.
+  unfold gmap_wf; rewrite !bool_decide_spec.
+  intros Hm1 Hm2 p z. rewrite lookup_merge; intros.
   destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
 Qed.
-Global Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f '(GMap m1 Hm1) '(GMap m2 Hm2),
-  let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
-  GMap (merge f' m1 m2) (gmap_merge_wf f m1 m2 Hm1 Hm2).
-Global Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ '(GMap m _),
-  omap (λ '(i, x), (., x) <$> decode i) (map_to_list m).
+Global Instance gmap_merge `{Countable K} : Merge (gmap K) :=
+  λ A B C f '(GMap m1 Hm1) '(GMap m2 Hm2),
+    GMap (merge f m1 m2) (gmap_merge_wf f m1 m2 Hm1 Hm2).
+Global Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) :=
+  λ '(GMap m _),
+    omap (λ '(i, x), (., x) <$> decode i) (map_to_list m).
 
 (** * Instantiation of the finite map interface *)
 Global Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
@@ -129,8 +129,7 @@ Proof.
     + intros; exists (encode i,x); simpl.
       by rewrite elem_of_map_to_list, decode_encode.
   - intros A B f [m Hm] i; apply (lookup_omap f m).
-  - intros A B C f ? [m1 Hm1] [m2 Hm2] i; unfold merge, lookup; simpl.
-    set (f' o1 o2 := match o1, o2 with None,None => None | _, _ => f o1 o2 end).
+  - intros A B C f [m1 Hm1] [m2 Hm2] i; unfold merge, lookup; simpl.
     by rewrite lookup_merge by done; destruct (m1 !! _), (m2 !! _).
 Qed.
 

theories/mapset.v

@@ -120,7 +120,7 @@ Lemma elem_of_mapset_dom_with {A} (f : A → bool) m i :
   i ∈ mapset_dom_with f m ↔ ∃ x, m !! i = Some x ∧ f x.
 Proof.
   unfold mapset_dom_with, elem_of, mapset_elem_of.
-  simpl. rewrite lookup_merge by done. destruct (m !! i) as [a|].
+  simpl. rewrite lookup_merge, lookup_empty. destruct (m !! i) as [a|]; simpl.
   - destruct (Is_true_reflect (f a)); naive_solver.
   - naive_solver.
 Qed.

theories/natmap.v

@@ -128,7 +128,7 @@ Definition natmap_merge_raw {A B C} (f : option A → option B → option C) :
   match l1, l2 with
   | [], l2 => natmap_omap_raw (f None ∘ Some) l2
   | l1, [] => natmap_omap_raw (flip f None ∘ Some) l1
-  | o1 :: l1, o2 :: l2 => natmap_cons_canon (f o1 o2) (go l1 l2)
+  | o1 :: l1, o2 :: l2 => natmap_cons_canon (diag_None f o1 o2) (go l1 l2)
   end.
 Lemma natmap_merge_wf {A B C} (f : option A → option B → option C) l1 l2 :
   natmap_wf l1 → natmap_wf l2 → natmap_wf (natmap_merge_raw f l1 l2).
@@ -136,9 +136,8 @@ Proof.
   revert l2. induction l1; intros [|??]; simpl;
     eauto using natmap_omap_raw_wf, natmap_cons_canon_wf, natmap_wf_inv.
 Qed.
-Lemma natmap_lookup_merge_raw {A B C} (f : option A → option B → option C)
-    l1 l2 i : f None None = None →
-  mjoin (natmap_merge_raw f l1 l2 !! i) = f (mjoin (l1 !! i)) (mjoin (l2 !! i)).
+Lemma natmap_lookup_merge_raw {A B C} (f : option A → option B → option C) l1 l2 i :
+  mjoin (natmap_merge_raw f l1 l2 !! i) = diag_None f (mjoin (l1 !! i)) (mjoin (l2 !! i)).
 Proof.
   intros. revert i l2. induction l1; intros [|?] [|??]; simpl;
     autorewrite with natmap; auto;
@@ -230,7 +229,7 @@ Proof.
   - intros ? [??]. by apply natmap_to_list_raw_nodup.
   - intros ? [??] ??. by apply natmap_elem_of_to_list_raw.
   - intros ??? [??] ?. by apply natmap_lookup_omap_raw.
-  - intros ????? [??] [??] ?. by apply natmap_lookup_merge_raw.
+  - intros ???? [??] [??] ?. apply natmap_lookup_merge_raw.
 Qed.
 
 Fixpoint strip_Nones {A} (l : list (option A)) : list (option A) :=

theories/nmap.v

@@ -39,7 +39,7 @@ Global Instance Nomap: OMap Nmap := λ A B f t,
   match t with NMap o t => NMap (o ≫= f) (omap f t) end.
 Global Instance Nmerge: Merge Nmap := λ A B C f t1 t2,
   match t1, t2 with
-  | NMap o1 t1, NMap o2 t2 => NMap (f o1 o2) (merge f t1 t2)
+  | NMap o1 t1, NMap o2 t2 => NMap (diag_None f o1 o2) (merge f t1 t2)
   end.
 Global Instance Nfmap: FMap Nmap := λ A B f t,
   match t with NMap o t => NMap (f <$> o) (f <$> t) end.
@@ -74,7 +74,7 @@ Proof.
         destruct i as [|i]; simpl; [done |].
         intros. exists (i, x). by rewrite elem_of_map_to_list.
   - intros ?? f [??] [|?]; simpl; [done|]; apply (lookup_omap f).
-  - intros ??? f ? [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
+  - intros ??? f [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
 Qed.
 
 (** * Finite sets *)

theories/option.v

@@ -302,18 +302,9 @@ Lemma option_union_Some {A} (mx my : option A) z :
   mx ∪ my = Some z → mx = Some z ∨ my = Some z.
 Proof. destruct mx, my; naive_solver. Qed.
 
-Class DiagNone {A B C} (f : option A → option B → option C) :=
-  diag_none : f None None = None.
-
 Section union_intersection_difference.
   Context {A} (f : A → A → option A).
 
-  Global Instance union_with_diag_none : DiagNone (union_with f).
-  Proof. reflexivity. Qed.
-  Global Instance intersection_with_diag_none : DiagNone (intersection_with f).
-  Proof. reflexivity. Qed.
-  Global Instance difference_with_diag_none : DiagNone (difference_with f).
-  Proof. reflexivity. Qed.
   Global Instance union_with_left_id : LeftId (=) None (union_with f).
   Proof. by intros [?|]. Qed.
   Global Instance union_with_right_id : RightId (=) None (union_with f).

theories/pmap.v

@@ -99,7 +99,7 @@ Fixpoint Pmerge_raw {A B C} (f : option A → option B → option C)
   | PLeaf, t2 => Pomap_raw (f None ∘ Some) t2
   | t1, PLeaf => Pomap_raw (flip f None ∘ Some) t1
   | PNode o1 l1 r1, PNode o2 l2 r2 =>
-      PNode' (f o1 o2) (Pmerge_raw f l1 l2) (Pmerge_raw f r1 r2)
+      PNode' (diag_None f o1 o2) (Pmerge_raw f l1 l2) (Pmerge_raw f r1 r2)
   end.
 
 (** Proofs *)
@@ -241,14 +241,13 @@ Proof.
   revert i. induction t as [|o l IHl r IHr]; intros [i|i|]; simpl;
     rewrite ?PNode_lookup; simpl; auto.
 Qed.
-Lemma Pmerge_lookup {A B C} (f : option A → option B → option C)
-    (Hf : f None None = None) t1 t2 i :
-  Pmerge_raw f t1 t2 !! i = f (t1 !! i) (t2 !! i).
+Lemma Pmerge_lookup {A B C} (f : option A → option B → option C) t1 t2 i :
+  Pmerge_raw f t1 t2 !! i = diag_None f (t1 !! i) (t2 !! i).
 Proof.
   revert t2 i; induction t1 as [|o1 l1 IHl1 r1 IHr1]; intros t2 i; simpl.
   { rewrite Pomap_lookup. by destruct (t2 !! i). }
   unfold compose, flip.
-  destruct t2 as [|l2 o2 r2]; rewrite PNode_lookup.
+  destruct t2 as [|o2 l2 r2]; rewrite PNode_lookup.
   - by destruct i; rewrite ?Pomap_lookup; simpl; rewrite ?Pomap_lookup;
       match goal with |- ?o ≫= _ = _ => destruct o end.
   - destruct i; rewrite ?Pomap_lookup; simpl; auto.
@@ -299,7 +298,7 @@ Proof.
     + by intros [(?&->&?)|].
     + by left; exists i.
   - intros ?? ? [??] ?. by apply Pomap_lookup.
-  - intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
+  - intros ??? ? [??] [??] ?. by apply Pmerge_lookup.
 Qed.
 
 Global Program Instance Pmap_countable `{Countable A} : Countable (Pmap A) := {

theories/zmap.v

@@ -42,9 +42,9 @@ Global Instance Zomap: OMap Zmap := λ A B f t,
 Global Instance Zmerge: Merge Zmap := λ A B C f t1 t2,
   match t1, t2 with
   | ZMap o1 t1 t1', ZMap o2 t2 t2' =>
-     ZMap (f o1 o2) (merge f t1 t2) (merge f t1' t2')
+     ZMap (diag_None f o1 o2) (merge f t1 t2) (merge f t1' t2')
   end.
-Global Instance Nfmap: FMap Zmap := λ A B f t,
+Global Instance Zfmap: FMap Zmap := λ A B f t,
   match t with ZMap o t t' => ZMap (f <$> o) (f <$> t) (f <$> t') end.
 
 Global Instance: FinMap Z Zmap.
@@ -85,7 +85,7 @@ Proof.
         { left; exists (i, x). by rewrite elem_of_map_to_list. }
         right; exists (i, x). by rewrite elem_of_map_to_list.
   - intros ?? f [??] [|?|?]; simpl; [done| |]; apply (lookup_omap f).
-  - intros ??? f ? [??] [??] [|?|?]; simpl; [done| |]; apply (lookup_merge f).
+  - intros ??? f [??] [??] [|?|?]; simpl; [done| |]; apply (lookup_merge f).
 Qed.
 
 (** * Finite sets *)