From e91acf7670084900bbdb0d9db33bfb98be7c85ef Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 9 Jun 2021 01:37:36 +0200
Subject: [PATCH] Add `Proper`s for maps, and generalise existing ones. Add
 tests to check that the old ones can be derived.

---
 tests/solve_proper.v | 42 ++++++++++++++++++++++++++++++++++++-
 theories/fin_maps.v  | 50 +++++++++++++++++++++++++++++++++++---------
 theories/option.v    |  4 ++--
 3 files changed, 83 insertions(+), 13 deletions(-)

diff --git a/tests/solve_proper.v b/tests/solve_proper.v
index d4e4d665..5efcdbce 100644
--- a/tests/solve_proper.v
+++ b/tests/solve_proper.v
@@ -1,4 +1,4 @@
-From stdpp Require Import prelude.
+From stdpp Require Import prelude fin_maps.
 
 (** Some tests for solve_proper. *)
 Section tests.
@@ -22,3 +22,43 @@ Section tests.
   Goal Proper (pointwise_relation nat (≡) ==> (≡)) test3.
   Proof. solve_proper. Qed.
 End tests.
+
+Section map_tests.
+  Context `{FinMap K M} `{Equiv A}.
+
+  (** For higher-order functions on maps (like [map_with_with], [fmap], etc)
+  we use "higher-order [Proper] instances" [Proper ((≡) ==> (≡)) ==> ...)]
+  that also allow the function to differ. We test that we can derive simpler
+  [Proper]s for a fixed function using both type class inference ([apply _])
+  and std++'s [solve_proper] tactic. *)
+  Global Instance map_zip_proper_test1 `{Equiv B} :
+    Proper ((≡@{M A}) ==> (≡@{M B}) ==> (≡@{M (A * B)})) map_zip.
+  Proof. apply _. Abort.
+  Global Instance map_zip_proper_test2 `{Equiv B} :
+    Proper ((≡@{M A}) ==> (≡@{M B}) ==> (≡@{M (A * B)})) map_zip.
+  Proof. solve_proper. Abort.
+  Global Instance map_zip_with_proper_test1 `{Equiv B, Equiv C} (f : A → B → C) :
+    Proper ((≡) ==> (≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡) ==> (≡)) (map_zip_with (M:=M) f).
+  Proof. apply _. Qed.
+  Global Instance map_zip_with_proper_test2 `{Equiv B, Equiv C} (f : A → B → C) :
+    Proper ((≡) ==> (≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡) ==> (≡)) (map_zip_with (M:=M) f).
+  Proof. solve_proper. Abort.
+  Global Instance map_fmap_proper_test1 `{Equiv B} (f : A → B) :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡@{M _})) (fmap f).
+  Proof. apply _. Qed.
+  Global Instance map_fmap_proper_test2 `{Equiv B} (f : A → B) :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡@{M _})) (fmap f).
+  Proof. solve_proper. Qed.
+  Global Instance map_omap_proper_test1 `{Equiv B} (f : A → option B) :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡@{M _})) (omap f).
+  Proof. apply _. Qed.
+  Global Instance map_omap_proper_test2 `{Equiv B} (f : A → option B) :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡@{M _})) (omap f).
+  Proof. solve_proper. Qed.
+End map_tests.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index b887f0b6..59bd16ce 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -191,11 +191,11 @@ Section setoid.
   Global Instance map_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (M A).
   Proof. intros m1 m2 Hm; apply map_eq; intros i. apply leibniz_equiv, Hm. Qed.
 
-  Global Instance lookup_proper (i : K) : Proper ((≡@{M A}) ==> (≡)) (lookup i).
+  Global Instance lookup_proper (i : K) : Proper ((≡@{M A}) ==> (≡)) (.!! i).
   Proof. by intros m1 m2 Hm. Qed.
   Global Instance lookup_total_proper (i : K) `{!Inhabited A} :
     Proper (≡@{A}) inhabitant →
-    Proper ((≡@{M A}) ==> (≡)) (lookup_total i).
+    Proper ((≡@{M A}) ==> (≡)) (.!!! i).
   Proof.
     intros ? m1 m2 Hm. unfold lookup_total, map_lookup_total.
     apply from_option_proper; auto. by intros ??.
@@ -237,18 +237,48 @@ Section setoid.
     intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
     by do 2 destruct 1; first [apply Hf | constructor].
   Qed.
+  Global Instance intersection_with_proper :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡@{M A})) intersection_with.
+  Proof.
+    intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
+    by do 2 destruct 1; first [apply Hf | constructor].
+  Qed.
+  Global Instance difference_with_proper :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡@{M A})) difference_with.
+  Proof.
+    intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
+    by do 2 destruct 1; first [apply Hf | constructor].
+  Qed.
+  Global Instance union_proper : Proper ((≡) ==> (≡) ==>(≡@{M A})) (∪).
+  Proof. apply union_with_proper; solve_proper. Qed.
+  Global Instance intersection_proper : Proper ((≡) ==> (≡) ==>(≡@{M A})) (∩).
+  Proof. apply intersection_with_proper; solve_proper. Qed.
+  Global Instance difference_proper : Proper ((≡) ==> (≡) ==>(≡@{M A})) (∖).
+  Proof. apply difference_with_proper. constructor. Qed.
+
+  Global Instance map_zip_with_proper `{Equiv B, Equiv C} :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B}) ==> (≡@{M C}))
+      map_zip_with.
+  Proof.
+    intros f1 f2 Hf m1 m1' Hm1 m2 m2' Hm2. apply merge_ext; try done.
+    destruct 1; destruct 1; repeat f_equiv; constructor || by apply Hf.
+  Qed.
 
-  Global Instance map_fmap_proper `{Equiv B} (f : A → B) :
-    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡@{M _})) (fmap f).
+  Global Instance map_disjoint_proper :
+    Proper ((≡@{M A}) ==> (≡@{M A}) ==> iff) map_disjoint.
+  Proof.
+    intros m1 m1' Hm1 m2 m2' Hm2; split;
+      intros Hm i; specialize (Hm i); by destruct (Hm1 i), (Hm2 i).
+  Qed.
+  Global Instance map_fmap_proper `{Equiv B} :
+    Proper (((≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B})) fmap.
   Proof.
-    intros ? m m' ? k; rewrite !lookup_fmap. by apply option_fmap_proper.
+    intros f f' Hf m m' ? k; rewrite !lookup_fmap. by apply option_fmap_proper.
   Qed.
-  Global Instance map_zip_with_proper `{Equiv B, Equiv C} (f : A → B → C) :
-    Proper ((≡) ==> (≡) ==> (≡)) f →
-    Proper ((≡) ==> (≡) ==> (≡)) (map_zip_with (M:=M) f).
+  Global Instance map_omap_proper `{Equiv B} :
+    Proper (((≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B})) omap.
   Proof.
-    intros Hf m1 m1' Hm1 m2 m2' Hm2. apply merge_ext; try done.
-    destruct 1; destruct 1; repeat f_equiv; constructor || done.
+    intros f f' ? m m' ? k; rewrite !lookup_omap. by apply option_bind_proper.
   Qed.
 End setoid.
 
diff --git a/theories/option.v b/theories/option.v
index 28ecff3b..b69d1dc3 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -145,8 +145,8 @@ Section setoids.
 
   Global Instance is_Some_proper : Proper ((≡@{option A}) ==> iff) is_Some.
   Proof. inversion_clear 1; split; eauto. Qed.
-  Global Instance from_option_proper {B} (R : relation B) (f : A → B) :
-    Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
+  Global Instance from_option_proper {B} (R : relation B) :
+    Proper (((≡@{A}) ==> R) ==> R ==> (≡) ==> R) from_option.
   Proof. destruct 3; simpl; auto. Qed.
 End setoids.
 
-- 
GitLab