From ed3c2a9262d7bbdd3f58335bb24248f01020dc30 Mon Sep 17 00:00:00 2001
From: Vincent Siles <vsiles@fb.com>
Date: Thu, 11 Aug 2022 13:09:12 +0200
Subject: [PATCH] [list] squashing MR on top of master

---
 CHANGELOG.md         |  3 +++
 stdpp/list.v         | 24 ++++++++++++++++++------
 stdpp/list_numbers.v |  2 +-
 3 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index da57df1e..a64d01b1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -41,6 +41,9 @@ Coq 8.11 is no longer supported.
   involving bitwise operations. (by Michael Sammler)
 - Add the bind operation `set_bind` for finite sets. (by Dan Frumin and Paolo G.
   Giarrusso)
+- Change `list_fmap_ext` and `list_fmap_equiv_ext` to require equality on the
+  elements of the list, not on all elements of the carrier type. This change
+  makes these lemmas consistent with those for 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/stdpp/list.v b/stdpp/list.v
index d6053261..807dbc5b 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -3895,12 +3895,6 @@ Section fmap.
 
   Lemma list_fmap_compose {C} (g : B → C) l : g ∘ f <$> l = g <$> (f <$> l).
   Proof. induction l; f_equal/=; auto. Qed.
-  Lemma list_fmap_ext (g : A → B) (l1 l2 : list A) :
-    (∀ x, f x = g x) → l1 = l2 → fmap f l1 = fmap g l2.
-  Proof. intros ? <-. induction l1; f_equal/=; auto. Qed.
-  Lemma list_fmap_equiv_ext `{!Equiv B} (g : A → B) l :
-    (∀ x, f x ≡ g x) → f <$> l ≡ g <$> l.
-  Proof. induction l; constructor; auto. Qed.
 
   Global Instance fmap_inj: Inj (=) (=) f → Inj (=@{list A}) (=) (fmap f).
   Proof.
@@ -4084,6 +4078,24 @@ Section fmap.
   Proof. by induction l; f_equal/=. Qed.
 End fmap.
 
+Section ext.
+  Context {A B : Type}.
+  Implicit Types l : list A.
+
+  Lemma list_fmap_ext (f g : A → B) l :
+    (∀ i x, l !! i = Some x → f x = g x) → f <$> l = g <$> l.
+  Proof.
+    intros Hfg. apply list_eq; intros i. rewrite !list_lookup_fmap.
+    destruct (l !! i) eqn:?; f_equal/=; eauto.
+  Qed.
+  Lemma list_fmap_equiv_ext `{!Equiv B} (f g : A → B) l :
+    (∀ i x, l !! i = Some x → f x ≡ g x) → f <$> l ≡ g <$> l.
+  Proof.
+    intros Hl. apply list_equiv_lookup; intros i. rewrite !list_lookup_fmap.
+    destruct (l !! i) eqn:?; simpl; constructor; eauto.
+  Qed.
+End ext.
+
 Lemma list_alter_fmap_mono {A} (f : A → A) (g : A → A) l i :
   Forall (λ x, f (g x) = g (f x)) l → f <$> alter g i l = alter g i (f <$> l).
 Proof. auto using list_alter_fmap. Qed.
diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index 2fbb3de1..b85189c7 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -164,7 +164,7 @@ Section seqZ.
   Proof.
     intros. unfold seqZ. rewrite Z2Nat.inj_add, seq_app, fmap_app by done.
     f_equal. rewrite Nat.add_comm, <-!fmap_add_seq, <-list_fmap_compose.
-    apply list_fmap_ext; [|done]; intros j; simpl.
+    apply list_fmap_ext; intros j n; simpl.
     rewrite Nat2Z.inj_add, Z2Nat.id by done. lia.
   Qed.
 
-- 
GitLab