How to work on base representations and lists?

Stream: general

[Ryan Lahfa]

I'm trying to work out with integers base representations using data.nat.digits and here is a MWE where I am completely stuck:

import data.nat.digits


lemma mwe
  (b n: ℕ):
  list.sum ((nat.digits b n).map_with_index (λ i a, a * b ^ i))
  = n :=
  begin
    conv {
      to_rhs,
      rw ← nat.of_digits_digits b n,
    },
    rw nat.of_digits_eq_foldr b,
    -- how to carry on?
    sorry
  end

I have the feeling the list API is not really enough and unsure if I should switch to something like finset and use only finset in my code but as the base repr API provides me only with list, I'm not sure.

I guess what should I do is to develop adhoc lemmas to show that foldr and the map_with_index coincide in the way I want using induction or something like this.

[Jannis Limperg]

Seems like there is indeed a map_with_index-shaped hole in the mathlib API -- quick grep didn't find anything. For this particular application, you need the lemma that map_with_index is equal to a foldr; after that you should be able to use foldr fusion to get rid of the sum. The map_with_index lemma would probably go into data/list/indexes.lean.

[Eric Wieser]

Does rw map_with_index make progress? Or is docs#list.map_with_index not defined conveniently?

Edit now the link is there: Looks like it's not. Maybe it should be redefined in terms of foldr?

[Jannis Limperg]

This applies to a lot of the list functions. Could be that the direct recursive formulation is more efficient than the foldr one.

[Eric Wieser]

I think it's simpler than that - map_with_index is defined before foldr (and both are in lean core)

[Yakov Pechersky]

I would make a lemma that says that l.map_with_index f can be expressed as a l.enum.map (uncurry f) or something

[Yakov Pechersky]

And then you'll be in the clear, because enum and map have way more lemmas.

[Yakov Pechersky]

For example, the relevant one here could be docs#list.enum_eq_zip_range

[Yakov Pechersky]

And I expect there might be an inductive step here.

[Ryan Lahfa]

Jannis Limperg said:

Seems like there is indeed a map_with_index-shaped hole in the mathlib API -- quick grep didn't find anything. For this particular application, you need the lemma that map_with_index is equal to a foldr; after that you should be able to use foldr fusion to get rid of the sum. The map_with_index lemma would probably go into data/list/indexes.lean.

Would that be something like:

lemma list.sum_map_with_index_eq_foldr {α β: Type*} (as: list α) (f: ℕ → α → β):
  (as.map_with_index f).sum = as.foldr (something here) := sorry

?

[Ryan Lahfa]

example {α β: Type*}
  (f : ℕ → α → β)
  (x : ℕ × α) :
  function.uncurry (λ (i : ℕ) (a : α), f (i + 1) a) x =
    (function.uncurry f ∘ prod.map (has_add.add 1) id) x :=
begin
   simp, -- why is it simplified to a single arg function on the lhs?
end

Curious case, I encountered while trying the path @Yakov Pechersky suggested ; and what would be a standard way to move forward?

[Yakov Pechersky]

example {α β: Type*}
  (f : ℕ → α → β)
  (x : ℕ × α) :
  function.uncurry (λ (i : ℕ) (a : α), f (i + 1) a) x =
    (function.uncurry f ∘ prod.map (has_add.add 1) id) x :=
begin
  cases x,
  simp [add_comm]
end

[Ryan Lahfa]

Okay, indeed, that was simple, thanks !

[Ryan Lahfa]

While I'm on the subject, is this,

lemma list.map_with_index_core_eq_map_with_index {α β: Type*}
  (f: ℕ → α → β) (as: list α) (n: ℕ):
  list.map_with_index_core f n as = list.map_with_index (λ i a, f (n + i) a) as
  :=
begin
  sorry,
end

something that is "in the library" or follows quitely easily from the library or should be proved?

[Yakov Pechersky]

lemma list.map_with_index_core_eq {α β : Type*} (l : list α) (f : ℕ → α → β) (n : ℕ) :
  l.map_with_index_core f n = l.map_with_index (λ i a, f (i + n) a) :=
begin
  induction l with hd tl hl generalizing f n,
  { simp [list.map_with_index, list.map_with_index_core] },
  { rw [list.map_with_index],
    simp [list.map_with_index_core, hl, add_left_comm, add_assoc, add_comm] }
end

[Yakov Pechersky]

I had to prove this, it wasn't in the library

[Ryan Lahfa]

Thanks a lot @Yakov Pechersky !

[Yakov Pechersky]

Full proof:

import data.nat.digits
import data.list.range

lemma list.map_with_index_core_eq {α β : Type*} (l : list α) (f : ℕ → α → β) (n : ℕ) :
  l.map_with_index_core f n = l.map_with_index (λ i a, f (i + n) a) :=
begin
  induction l with hd tl hl generalizing f n,
  { simp [list.map_with_index, list.map_with_index_core] },
  { rw [list.map_with_index],
    simp [list.map_with_index_core, hl, add_left_comm, add_assoc, add_comm] }
end

@[simp] lemma list.map_uncurry_zip_eq_zip_with {α β γ : Type*}
  (f : α → β → γ) (l : list α) (l' : list β) :
  list.map (function.uncurry f) (l.zip l') = list.zip_with f l l' :=
begin
  induction l with hd tl hl generalizing l',
  { simp },
  { cases l' with hd' tl',
    { simp },
    { simp [hl] } }
end

lemma list.zip_with_map_left {α β γ δ : Type*}
  (f : α → β → γ) (g : δ → α) (l : list δ) (l' : list β) :
  list.zip_with f (l.map g) l' = list.zip_with (f ∘ g) l l' :=
begin
  induction l with hd tl hl generalizing l',
  { simp },
  { cases l' with hd' tl',
    { simp },
    { simp [hl] } }
end

lemma list.zip_with_map_right {α β γ δ : Type*}
  (f : α → β → γ) (l : list α) (g : δ → β) (l' : list δ) :
  list.zip_with f l (l'.map g) = list.zip_with (λ x, f x ∘ g) l l' :=
begin
  induction l with hd tl hl generalizing l',
  { simp },
  { cases l' with hd' tl',
    { simp },
    { simp [hl] } }
end

lemma list.map_with_index_eq_enum_map_uncurry {α β : Type*} (l : list α) (f : ℕ → α → β) :
  l.map_with_index f = l.enum.map (function.uncurry f) :=
begin
  induction l with hd tl hl generalizing f,
  { simp [list.map_with_index, list.map_with_index_core, list.enum_eq_zip_range] },
  { rw [list.map_with_index, list.map_with_index_core, list.map_with_index_core_eq, hl],
    simp [list.enum_eq_zip_range, list.range_succ_eq_map, list.zip_with_map_left] }
end

@[simp] lemma list.sum_zip_with_distrib_left {α β : Type*} (f : α → β → ℕ) (n : ℕ) (l : list α) (l' : list β) :
  (list.zip_with (λ x y, n * f x y) l l').sum = n * (l.zip_with f l').sum :=
begin
  induction l with hd tl hl generalizing f n l',
  { simp },
  { cases l' with hd' tl',
    { simp, },
    { simp [hl, mul_add] } }
end

lemma aux (b : ℕ) (l : list ℕ) :
  (list.zip_with ((λ (i a : ℕ), a * b ^ i) ∘ nat.succ) (list.range l.length) l).sum =
  b * (list.zip_with (λ i a, a * b ^ i) (list.range l.length) l).sum :=
begin
  suffices : list.zip_with (((λ (i a : ℕ), a * b ^ i) ∘ nat.succ)) (list.range l.length) l =
      list.zip_with (λ i a, b * (a * b ^ i)) (list.range l.length) l,
    { simp [this] },
  congr,
  ext,
  simp [pow_succ],
  ring
end

lemma mwe  (b n: ℕ) :
  list.sum ((nat.digits b n).map_with_index (λ i a, a * b ^ i)) = n :=
begin
  conv {
      to_rhs,
      rw ← nat.of_digits_digits b n,
    },
  rw [list.map_with_index_eq_enum_map_uncurry, list.enum_eq_zip_range,
      list.map_uncurry_zip_eq_zip_with, nat.of_digits_eq_foldr b],
  induction b.digits n with hd tl hl,
  { simp },
  { simp [list.range_succ_eq_map, list.zip_with_map_left, aux, hl] }
end

[Yakov Pechersky]

Feel free to PR any of these to mathlib.

[Yakov Pechersky]

The crucial part was to just consider nat.digits b n as some random list. For that, your work to use nat.of_digits_digits and nat.of_digits_eq_foldr was crucial.

[Yakov Pechersky]

Everything else is just juggling the various list operations. And writing a distrib lemma.

[Ryan Lahfa]

Yakov Pechersky said:

Everything else is just juggling the various list operations. And writing a distrib lemma.

Indeed, but the proofs you wrote are a lot nicer than mine which were a bit tedious and slow I guess, thank you for the example, I learnt a lot from this!

[Ryan Lahfa]

Yakov Pechersky said:

Feel free to PR any of these to mathlib.

I will try to open a PR in the next hours with those :)

[Yakov Pechersky]

I think it's really neat that a lot of the proofs are just:

  induction l with hd tl hl generalizing l',
  { simp },
  { cases l' with hd' tl',
    { simp },
    { simp [hl] } }

[Yakov Pechersky]

That means that there are good simp lemmas elsewhere, and that the list operation makes sense.

[Yakov Pechersky]

There can probably be some general list.zip_with congr lemma that expects hypotheses that would prove goals of this type.

[Ryan Lahfa]

Here's a first PR: https://github.com/leanprover-community/mathlib/pull/5963 — @Yakov Pechersky Let me know how do you want to be credited for the proofs :)

[Ryan Lahfa]

And here's the second one: https://github.com/leanprover-community/mathlib/pull/5964

[Ryan Lahfa]

Follow-up question @Yakov Pechersky — how would you simplify the proof of:

@[simp] lemma map_of_map_with_index_eq_map {α β γ: Type*} (g: β → γ) (f: ℕ → α → β) (L: list α):
  list.map g (list.map_with_index f L) = list.map_with_index (λ i a, g (f i a)) L :=
begin
  induction L with hd tl hl generalizing f,
  { simp [list.map_with_index, list.map_with_index_core] },
  {
    rw [list.map_with_index, list.map_with_index,
      list.map_with_index_core, list.map_with_index_core,
      list.map_with_index_core_eq, list.map_with_index_core_eq],
    simp [hl],
  }
end

It seems like I cannot rewrite both sides directly with one application of rw, unsure of a simpler path?

[Ryan Lahfa]

Also I suppose there's no easy way to write down the composition as g \circ f and that would still be a currified function?

[Ryan Lahfa]

Also, more difficult question I guess about casts, I have a cast in front of some map_with_index which I want to be lifted inside the function, it appears to me that norm_cast does not work out of the box, so I supposed there was some coercion theorem missing here, I tried to write down this:

@[norm_cast] lemma cast_map_index_sum {α β γ}
[add_monoid β] [add_monoid γ]
[has_lift_t β γ] (f: ℕ → α → β) (l: list α):
  (↑(list.map_with_index f l).sum) = ((list.map_with_index (λ x, ↑(f x)) l).sum: γ) :=
  begin
   induction l with hd tl hl,
   unfold list.map_with_index,
   unfold list.map_with_index_core,
   rw list.sum_nil,
   rw list.sum_nil,
   sorry,
   sorry,
  end

but unsure if I'm going through the right way, also I do not see how to clear out coe 0 = 0 — surely, a coercion of 0 is still 0?

[Ryan Lahfa]

Here's a MWE of what I'm trying to do:

import data.real.basic
import analysis.special_functions.pow
import data.nat.digits

lemma of_digits_eq_sum_map_with_index (b: ℕ) (L: list ℕ):
  nat.of_digits b L = list.sum (L.map_with_index (λ (i: ℕ) (a: ℕ), a * b ^ i)) := sorry

lemma mwe (b: ℕ) (l: list ℕ): abs ((nat.of_digits b l): ℝ) = abs (list.sum (l.map_with_index (λ i a, ↑a * (b: ℝ) ^ i))) :=
by { rw_mod_cast of_digits_eq_sum_map_with_index, norm_cast }

[Mario Carneiro]

If you just assume has_lift_t β γ, that just means you have a coe from beta to gamma that could do anything

[Mario Carneiro]

lemma list.map_map_with_index_core {α β γ} (f : ℕ → α → β) (g : β → γ) : ∀ (l : list α) n,
  (l.map_with_index_core f n).map g = l.map_with_index_core (λ i a, g (f i a)) n :=
by intros; induction l generalizing n; simp [*, list.map_with_index_core]

lemma list.map_map_with_index {α β γ} (f : ℕ → α → β) (g : β → γ) (l : list α) :
  (l.map_with_index f).map g = l.map_with_index (λ i a, g (f i a)) :=
list.map_map_with_index_core _ _ _ _

lemma of_digits_eq_sum_map_with_index (b: ℕ) (L: list ℕ):
  nat.of_digits b L =
  list.sum (L.map_with_index (λ (i: ℕ) (a: ℕ), a * b ^ i)) := sorry

lemma mwe (b: ℕ) (l: list ℕ): abs ((nat.of_digits b l): ℝ) = abs (list.sum (l.map_with_index (λ i a, ↑a * (b: ℝ) ^ i))) :=
begin
  congr,
  rw_mod_cast of_digits_eq_sum_map_with_index,
  have := list.sum_hom _ (nat.cast_add_monoid_hom ℝ),
  simp at this, rw [← this, list.map_map_with_index]
end

[Ryan Lahfa]

In the continuity of list lemmas that I'm not sure they exist or should exist, I'm looking now at:

lemma list.le_map_with_index {α β} (f g: ℕ → α → β) [canonically_linear_ordered_add_monoid β] (l: list α):
  (∀ (i: ℕ) (i_le: i < l.length), f i (list.nth_le l i i_le) ≤ g i (list.nth_le l i i_le)) → (l.map_with_index f).sum ≤ (l.map_with_index g).sum :=
begin
  intro h_f_le,
  induction l with hd tl hl generalizing f g,
  { simp [list.map_with_index, list.map_with_index_core] },
  { simp [list.map_with_index, list.map_with_index_core],
    rw [list.map_with_index_core_eq, list.map_with_index_core_eq],
    apply add_le_add,
    convert h_f_le 0 _,
    simp,
    convert hl _ _ _,
    intros i hi,
    convert h_f_le (i + 1) _,
    simp [hi],
   },
end

I was able to produce the proof by myself, but I would be interested into feedback regarding whether this is a good statement, and would there be a more natural way to prove it?

[Ryan Lahfa]

And another question also:

lemma mwe (b: ℕ) (l: list ℕ):
  list.sum (l.map_with_index (λ (i a: ℕ), abs ((a: ℝ) * (b: ℝ) ^ i))) = list.sum (l.map_with_index (λ (i a: ℕ), (abs a) * (abs b) ^ i)) :=
  begin
    congr,
    ext,
    simp [is_absolute_value.abv_mul, is_absolute_value.abv_pow],
    norm_cast,
    apply mul_nonneg,
    exact nat.zero_le _,
    apply pow_nonneg,
    exact nat.zero_le _,
  end

Is there a way to avoid proving this by proving equality of functions, it seems like a simple rewrite cannot "enter the function" and assume generic parameters to perform its rewrite?

[Hanting Zhang]

Btw, your mwe is not a true mwe; you're missing imports. Adding import data.real.basic makes the code error-free. (It's not a huge deal but figuring out what imports need to be added is annoying.)

[Ryan Lahfa]

Hanting Zhang said:

Btw, your mwe is not a true mwe; you're missing imports. Adding import data.real.basic makes the code error-free. (It's not a huge deal but figuring out what imports need to be added is annoying.)

Sorry for that, I'll change it

[Mario Carneiro]

simp can enter binders like this

[Mario Carneiro]

The issue here seems to be that you are using a lemma that isn't suitable for simp; with abs_mul it works fine

lemma mwe (b: ℕ) (l: list ℕ):
  list.sum (l.map_with_index (λ (i a: ℕ), abs ((a: ℝ) * (b: ℝ) ^ i))) = list.sum (l.map_with_index (λ (i a: ℕ), (abs a) * (abs b) ^ i)) :=
by simp [abs_mul, abs_pow]

[Ryan Lahfa]

Mario Carneiro said:

The issue here seems to be that you are using a lemma that isn't suitable for simp; with abs_mul it works fine

lemma mwe (b: ℕ) (l: list ℕ):
  list.sum (l.map_with_index (λ (i a: ℕ), abs ((a: ℝ) * (b: ℝ) ^ i))) = list.sum (l.map_with_index (λ (i a: ℕ), (abs a) * (abs b) ^ i)) :=
by simp [abs_mul, abs_pow]

Alright, makes sense

[Ryan Lahfa]

@Mario Carneiro what does it mean for a lemma to be suitable for simp ?
e.g. what makes abs_mul more suitable than abv_mul ?

[Mario Carneiro]

the lhs of abv_mul starts with a variable, so there is no key

[Ryan Lahfa]

Ah alright, indeed, adding explicitly the absolute value makes it work in general context, thanks!

[Mario Carneiro]

the fact that abs_mul is about the constant abs rather than an arbitrary absolute value like thing is what makes the difference

[Ryan Lahfa]

Hello again, I'm stuck on a le lemmas for lists, here's a MWE:

import data.real.cau_seq
import data.real.basic
import analysis.special_functions.pow


lemma list.le_map_with_index {α β} {f g: ℕ → α → β} [canonically_linear_ordered_add_monoid β] {l: list α}:
  (∀ (i: ℕ) (i_le: i < l.length), f i (list.nth_le l i i_le) ≤ g i (list.nth_le l i i_le)) → (l.map_with_index f).sum ≤ (l.map_with_index g).sum := sorry

theorem mwe (b: ℕ) (l: list ℕ) (h_abs: ∀ (a: ℕ), a ∈ l → abs (a: ℝ) ≤ 1):
list.sum (l.map_with_index (λ (i a: ℕ), (abs (a: ℝ)) * ((b: ℝ) ^ i)))
  ≤ list.sum (l.map_with_index (λ (i a: ℕ), (b: ℝ) ^ i)) :=
begin
  sorry,
end

I have an (ugly) proof of the le_map_with_index lemma, but it looks like for some reason (I suppose casts/coercions), I cannot apply it very well to this situation, I can convert from h_abs to the proper required hypothesis easily (and can add it), but a simple apply does not even work with an unification error

[Yakov Pechersky]

I would try to convert map_with_index to zip_with and then write some lemmas about how separable functions of zip_with are the same as some combination of zip_with of mapped lists

[Ryan Lahfa]

Yakov Pechersky said:

I would try to convert map_with_index to zip_with and then write some lemmas about how separable functions of zip_with are the same as some combination of zip_with of mapped lists

Got it, I will try something

[Yakov Pechersky]

Almost there! What's the lemma you would use to solve that le-quality?

import data.real.cau_seq
import data.real.basic
import analysis.special_functions.pow
import data.list.indexes

lemma list.sum_ext_le {α : Type*} [ordered_add_comm_monoid α] {l l' : list α}
  (hl : l.length = l'.length)
  (h : ∀ {i} (hle), l.nth_le i hle ≤ l'.nth_le i (hl ▸ hle)) :
  l.sum ≤ l'.sum :=
begin
  induction l with hd tl IH generalizing l',
  { have : l' = list.nil := by simpa [list.length_eq_zero] using hl.symm,
    simp [this] },
  { cases l' with hd' tl',
    { simpa using hl },
    { simp at hl,
      simp_rw list.sum_cons,
      refine add_le_add _ _,
      { exact h (nat.zero_lt_succ _) },
      { apply IH hl,
        intros i hi,
        exact h (nat.succ_lt_succ hi) } } }
end

open list

@[simp] lemma zip_with_const_left {α β γ : Type*} (f : α → γ) (l : list α) (l' : list β) :
  zip_with (λ a b, f a) l l' = take l'.length (map f l) :=
begin
  induction l with hd tl hl generalizing l',
  { simp },
  { cases l',
    { simp },
    { simp [hl] } }
end

@[simp] lemma zip_with_const_right {α β γ : Type*} (f : β → γ) (l : list α) (l' : list β) :
  zip_with (λ a, f) l l' = take l.length (map f l') :=
begin
  induction l with hd tl hl generalizing l',
  { simp },
  { cases l',
    { simp },
    { simp [hl] } }
end

lemma zip_with_separable {α β γ α' β' : Type*} (f : α → β → γ) (g : α' → α) (h : β' → β)
  (l : list α') (l' : list β') :
  zip_with (λ a b, f (g a) (h b)) l l' = zip_with f (map g l) (map h l') :=
begin
  induction l with hd tl hl generalizing l',
  { simp },
  { cases l',
    { simp },
    { simp [hl] } }
end

theorem mwe (b: ℕ) (l: list ℕ) (h_abs: ∀ (a: ℕ), a ∈ l → abs (a: ℝ) ≤ 1):
list.sum (l.map_with_index (λ (i a: ℕ), (abs (a: ℝ)) * ((b: ℝ) ^ i)))
  ≤ list.sum (l.map_with_index (λ (i a: ℕ), (b: ℝ) ^ i)) :=
begin
  have : (λ (i a : ℕ), abs (a : ℝ) * (b : ℝ) ^ i) = (λ (i a : ℕ), (b : ℝ) ^ i * abs (a : ℝ)),
    { ext, rw mul_comm },
  rw this, clear this,
  simp [map_with_index_eq_enum_map_uncurry, enum_eq_zip_range],
  rw [zip_with_separable],
  have : take l.length = take (map (pow (b : ℝ)) (range l.length)).length,
    { congr' 1, simp },
  rw [this, take_length], clear this,
  refine sum_ext_le (by simp) _,
  intros i hi,
  specialize h_abs (l.nth_le i (by simpa using hi)) (nth_le_mem _ _ _),
  simp,
  sorry -- I don't know the right le lemma here
end

[Yakov Pechersky]

That's on your branch#raito-mapwithindex-list

[Ryan Lahfa]

Wouldn't le_abs_self be the right lemma?

[Ryan Lahfa]

Something like, le_trans + le_abs_self + mul_le_mul_left and some simplification of *1

[Ryan Lahfa]

Hmm, annoyingly it will require to do case work on b pos with zero, unsure if there is a faster way

[Ryan Lahfa]

Thanks a lot though @Yakov Pechersky !

[Yakov Pechersky]

Also, if you notice, your h_abs can be simplified to a \le 1, because of course a \le abs a

[Ryan Lahfa]

Indeed, because those are natural integers

[Yakov Pechersky]

I mean, that's true for anything abs is defined on: docs#le_abs_self

[Ryan Lahfa]

Hmm, then the simplification is not always possible, right?
I mean, a \le 1 does not imply abs a \le 1 in general under the theorem: a \le abs a, or am I too tired? :D

[Ryan Lahfa]

(counterexample: -5 \le 1, though 5 \ge 1 even though -5 \le 5, right?)

[Yakov Pechersky]

I mean, here, you're always coercing from nat. So abs (a : \R) must be (a : \R)

[Yakov Pechersky]

So here is the final proof:

theorem mwe (b: ℕ) (l: list ℕ) (hle : ∀ (a: ℕ), a ∈ l → a ≤ 1):
list.sum (l.map_with_index (λ (i a: ℕ), (abs (a: ℝ)) * ((b: ℝ) ^ i)))
  ≤ list.sum (l.map_with_index (λ (i a: ℕ), (b: ℝ) ^ i)) :=
begin
  have : (λ (i a : ℕ), abs (a : ℝ) * (b : ℝ) ^ i) = (λ (i a : ℕ), (b : ℝ) ^ i * abs (a : ℝ)),
    { ext, rw mul_comm },
  rw this, clear this,
  simp [map_with_index_eq_enum_map_uncurry, enum_eq_zip_range],
  rw [zip_with_separable],
  have : take l.length = take (map (pow (b : ℝ)) (range l.length)).length,
    { congr' 1, simp },
  rw [this, take_length], clear this,
  refine sum_ext_le (by simp) _,
  intros i hi,
  let k : ℕ := l.nth_le i (by simpa using hi),
  suffices : (b : ℝ) ^ i * k ≤ b ^ i * 1,
    { simpa using this },
  refine mul_le_mul (le_refl _) _ (by simp) (by simp),
  simpa using hle k (nth_le_mem _ _ _)
end

[Yakov Pechersky]

As you can see, I changed the h_abs to hle

[Ryan Lahfa]

Yakov Pechersky said:

I mean, here, you're always coercing from nat. So abs (a : \R) must be (a : \R)

Ah! I completely agree, yes

[Yakov Pechersky]

So even in the l.map_with_index lambda, you don't need the abs.

[Ryan Lahfa]

Indeed, but this is only true in this "minimum" example, in general, I'm using arbitrary absolute values on which abs a != a even for nat, so I can only bound them through le_abv_self if I'm not wrong

[Yakov Pechersky]

Again, feel free to PR any of the lemmas. What was crucial here was to prove some general lemmas about sums over lists, or about zip_with. The zip_with_separable allowed us to get it to a form where we can throw away oen of the lists. But it can't be a simp lemma because we have (in your branch, at least) map_uncurry_zip_eq_zip_with as a simp lemma. And Jannis's comment here: https://github.com/leanprover-community/mathlib/pull/5974#discussion_r567509308 indicates that it probably shouldn't be! Additionally, he also came up with zip_with_separable, but in reverse:
https://github.com/leanprover-community/mathlib/pull/5974#discussion_r567508963

[Ryan Lahfa]

Yakov Pechersky said:

Again, feel free to PR any of the lemmas. What was crucial here was to prove some general lemmas about sums over lists, or about zip_with. The zip_with_separable allowed us to get it to a form where we can throw away oen of the lists. But it can't be a simp lemma because we have (in your branch, at least) map_uncurry_zip_eq_zip_with as a simp lemma. And Jannis's comment here: https://github.com/leanprover-community/mathlib/pull/5974#discussion_r567509308 indicates that it probably shouldn't be! Additionally, he also came up with zip_with_separable, but in reverse:
https://github.com/leanprover-community/mathlib/pull/5974#discussion_r567508963

Sure thing! Thanks for the comments and insights, I missed the fact that Jannis reviewed the PR, will address those comments tomorrow hopefully

[Ryan Lahfa]

Therefore, as we removed the simp attribute on map-uncurry lemma, should I add the simp on zip_with_map @Yakov Pechersky @Jannis Limperg ?

[Jannis Limperg]

I'd say yes. It's a bit specialised, but zip_with is not a common symbol so we won't run into performance issues.

[Ryan Lahfa]

Alright, will do the change!

[Ryan Lahfa]

Done :)