From afdc8633e01d727a959371c3d9ac18c9ed50c121 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Jun 2021 15:11:58 +0200
Subject: [PATCH] `Proper`s for `union`, `union_with`, `intersection_with`,
 `difference_with` on `option`.

---
 theories/option.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/theories/option.v b/theories/option.v
index 767426f1..7d235fca 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -321,6 +321,19 @@ Section union_intersection_difference.
   Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
   Global Instance difference_with_right_id : RightId (=) None (difference_with f).
   Proof. by intros [?|]. Qed.
+
+  Global Instance union_with_proper `{Equiv A} :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{option A}) ==> (≡) ==> (≡)) union_with.
+  Proof. intros ?? Hf; do 2 destruct 1; try constructor; by try apply Hf. Qed.
+  Global Instance intersection_with_proper `{Equiv A} :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{option A}) ==> (≡) ==> (≡)) intersection_with.
+  Proof. intros ?? Hf; do 2 destruct 1; try constructor; by try apply Hf. Qed.
+  Global Instance difference_with_proper `{Equiv A} :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{option A}) ==> (≡) ==> (≡)) difference_with.
+  Proof. intros ?? Hf; do 2 destruct 1; try constructor; by try apply Hf. Qed.
+  Global Instance union_proper `{Equiv A} :
+    Proper ((≡@{option A}) ==> (≡) ==> (≡)) union.
+  Proof. apply union_with_proper. by constructor. Qed.
 End union_intersection_difference.
 
 (** * Tactics *)
-- 
GitLab