From 5424f22a3401877e2998d63b9b37cca23f2bc21d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 26 May 2021 10:57:29 +0200
Subject: [PATCH] Add `Inj` instances for `fmap` on option and maps.

Thanks to @jules for pointing out these were missing.
---
 CHANGELOG.md        | 1 +
 theories/fin_maps.v | 7 +++++++
 theories/option.v   | 5 +++++
 3 files changed, 13 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 36f0f130..b5ec4788 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -29,6 +29,7 @@ API-breaking change is listed.
 - Add tactic `learn_hyp` (by Michael Sammler).
 - Add `Countable` instance for decidable Sigma types (by Simon Gregersen).
 - Add tactics `compute_done` and `compute_by` for solving goals by computation.
+- Add `Inj` instances for `fmap` on option and maps.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 1f0bc31b..45a0cc67 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -663,6 +663,13 @@ Lemma delete_singleton_ne {A} i j (x : A) :
 Proof. intro. apply delete_notin. by apply lookup_singleton_ne. Qed.
 
 (** ** Properties of the map operations *)
+Global Instance map_fmap_inj {A B} (f : A → B) :
+  Inj (=) (=) f → Inj (=@{M A}) (=@{M B}) (fmap f).
+Proof.
+  intros ? m1 m2 Hm. apply map_eq; intros i.
+  apply (inj (fmap (M:=option) f)). by rewrite <-!lookup_fmap, Hm.
+Qed.
+
 Lemma lookup_fmap_Some {A B} (f : A → B) (m : M A) i y :
   (f <$> m) !! i = Some y ↔ ∃ x, f x = y ∧ m !! i = Some x.
 Proof. rewrite lookup_fmap, fmap_Some. naive_solver. Qed.
diff --git a/theories/option.v b/theories/option.v
index 8ca61968..576edfcc 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -175,6 +175,10 @@ Global Instance option_fmap: FMap option := @option_map.
 Global Instance option_guard: MGuard option := λ P dec A f,
   match dec with left H => f H | _ => None end.
 
+Global Instance option_fmap_inj {A B} (f : A → B) :
+  Inj (=) (=) f → Inj (=@{option A}) (=@{option B}) (fmap f).
+Proof. intros ? [x1|] [x2|] [=]; naive_solver. Qed.
+
 Lemma fmap_is_Some {A B} (f : A → B) mx : is_Some (f <$> mx) ↔ is_Some mx.
 Proof. unfold is_Some; destruct mx; naive_solver. Qed.
 Lemma fmap_Some {A B} (f : A → B) mx y :
@@ -210,6 +214,7 @@ Proof. intros; destruct mx; f_equal/=; auto. Qed.
 Lemma option_fmap_equiv_ext {A} `{Equiv B} (f g : A → B) (mx : option A) :
   (∀ x, f x ≡ g x) → f <$> mx ≡ g <$> mx.
 Proof. destruct mx; constructor; auto. Qed.
+
 Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) mx :
   (f <$> mx) ≫= g = mx ≫= g ∘ f.
 Proof. by destruct mx. Qed.
-- 
GitLab