From bfbef8f74b82c4819a6a64da128283a5142238d8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 7 Jul 2020 15:40:59 +0200
Subject: [PATCH 1/3] prove NoDup_fmap_2_strong

---
 theories/list.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index c0f62879..e4fd5efc 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3496,6 +3496,23 @@ Section fmap.
   Lemma NoDup_fmap `{!Inj (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
   Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
 
+  (** A version of [NoDup_fmap_2] that does not require [f] to be injective for
+      *all* inputs. *)
+  Lemma NoDup_fmap_2_strong l :
+    (∀ x y, x ∈ l → y ∈ l → f x = f y → x = y) →
+    NoDup l →
+    NoDup (f <$> l).
+  Proof.
+    intros Hinj.
+    induction 1 as [|???? IH]; simpl; constructor; cycle 1.
+    { apply IH. clear- Hinj.
+      intros x' y Hx' Hy. apply Hinj; apply elem_of_list_further; done. }
+    rewrite elem_of_list_fmap. intros [y [Hxy ?]].
+    apply Hinj in Hxy; [by subst|..].
+    - apply elem_of_list_here.
+    - apply elem_of_list_further. done.
+  Qed.
+
   Global Instance fmap_sublist: Proper (sublist ==> sublist) (fmap f).
   Proof. induction 1; simpl; econstructor; eauto. Qed.
   Global Instance fmap_submseteq: Proper (submseteq ==> submseteq) (fmap f).
-- 
GitLab


From d96ebd4ccf1ff624aca6ab37c73a37cca18807a3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 7 Jul 2020 15:44:41 +0200
Subject: [PATCH 2/3] derive NoDup_fmap_2 from the stronger version

---
 theories/list.v | 23 ++++++++++-------------
 1 file changed, 10 insertions(+), 13 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index e4fd5efc..06a5255b 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3483,19 +3483,6 @@ Section fmap.
     naive_solver eauto using elem_of_list_fmap_1, elem_of_list_fmap_2_inj.
   Qed.
 
-  Lemma NoDup_fmap_1 l : NoDup (f <$> l) → NoDup l.
-  Proof.
-    induction l; simpl; inversion_clear 1; constructor; auto.
-    rewrite elem_of_list_fmap in *. naive_solver.
-  Qed.
-  Lemma NoDup_fmap_2 `{!Inj (=) (=) f} l : NoDup l → NoDup (f <$> l).
-  Proof.
-    induction 1; simpl; constructor; trivial. rewrite elem_of_list_fmap.
-    intros [y [Hxy ?]]. apply (inj f) in Hxy. by subst.
-  Qed.
-  Lemma NoDup_fmap `{!Inj (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
-  Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
-
   (** A version of [NoDup_fmap_2] that does not require [f] to be injective for
       *all* inputs. *)
   Lemma NoDup_fmap_2_strong l :
@@ -3513,6 +3500,16 @@ Section fmap.
     - apply elem_of_list_further. done.
   Qed.
 
+  Lemma NoDup_fmap_1 l : NoDup (f <$> l) → NoDup l.
+  Proof.
+    induction l; simpl; inversion_clear 1; constructor; auto.
+    rewrite elem_of_list_fmap in *. naive_solver.
+  Qed.
+  Lemma NoDup_fmap_2 `{!Inj (=) (=) f} l : NoDup l → NoDup (f <$> l).
+  Proof. apply NoDup_fmap_2_strong. intros ?? _ _. apply (inj f). Qed.
+  Lemma NoDup_fmap `{!Inj (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
+  Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
+
   Global Instance fmap_sublist: Proper (sublist ==> sublist) (fmap f).
   Proof. induction 1; simpl; econstructor; eauto. Qed.
   Global Instance fmap_submseteq: Proper (submseteq ==> submseteq) (fmap f).
-- 
GitLab


From fa2a86066951f9977d966af6d27832deeb28497f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 15 Jul 2020 18:38:11 +0200
Subject: [PATCH 3/3] shorter proof by Robbert

---
 theories/list.v | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index 06a5255b..ed104007 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3490,14 +3490,11 @@ Section fmap.
     NoDup l →
     NoDup (f <$> l).
   Proof.
-    intros Hinj.
-    induction 1 as [|???? IH]; simpl; constructor; cycle 1.
-    { apply IH. clear- Hinj.
-      intros x' y Hx' Hy. apply Hinj; apply elem_of_list_further; done. }
-    rewrite elem_of_list_fmap. intros [y [Hxy ?]].
-    apply Hinj in Hxy; [by subst|..].
-    - apply elem_of_list_here.
-    - apply elem_of_list_further. done.
+    intros Hinj. induction 1 as [|x l ?? IH]; simpl; constructor.
+    - intros [y [Hxy ?]]%elem_of_list_fmap.
+      apply Hinj in Hxy; [by subst|by constructor..].
+    - apply IH. clear- Hinj.
+      intros x' y Hx' Hy. apply Hinj; by constructor.
   Qed.
 
   Lemma NoDup_fmap_1 l : NoDup (f <$> l) → NoDup l.
-- 
GitLab