rewrite inside a function

Stream: Is there code for X?

[Flo (Florent Schaffhauser)]

Hi :wave:

Is there a routine technique to deal with equality between functions in the middle of a proof?

Here is a MWE, where I want to prove that if I divide all members of a list L by a non-zero constant c in a semifield F and then take the sum, it gives me the same result as summing the members of the list and then dividing the result by c... :new_baby:

import Mathlib.Tactic.FieldSimp
import Mathlib.Data.List.BigOperators.Lemmas

def sum_of_list_div {F : Type} [Semifield F]
  (L : List F) (c : F) (hc : c ≠ 0) : (L.map (. / c)).sum = (1 / c) * L.sum
    := by
      have aux : (fun x => x / c) = (fun x => c⁻¹ * x)
        := by
          ext x
          field_simp
      rw [aux, List.sum_map_mul_left]
      simp

Is there a standard way to avoid introducing the aux term here? Or to write a shorter definition of that term, one that would fit on a sole line?

[Alex J. Best]

I would rewrite using div_eq_mul_inv here, which is an existing lemma.
The only difficulty is that you need to use simp_rw as you are rewriting inside a function.
So you can do

      simp_rw [one_div, div_eq_mul_inv, List.sum_map_mul_right, mul_comm]
      simp

or even just

def sum_of_list_div {F : Type} [Semifield F]
  (L : List F) (c : F) (hc : c ≠ 0) : (L.map (. / c)).sum = (1 / c) * L.sum
    := by
      simp [one_div, div_eq_mul_inv, List.sum_map_mul_right, mul_comm]

Bonus: the linter now informs us that hc isn't actually needed for this proof, as 1/ 0= 0 etc so both sides are zero in that case

[Flo (Florent Schaffhauser)]

Thanks Alex, it looks really good and is exactly the kind of thing I was hoping for but could not get myself :smile:

[Flo (Florent Schaffhauser)]

Maybe a follow-up question would be: is simp_rw the standard way to do rewriting inside a function? Or are there other options?

[Anatole Dedecker]

There are other options, but simp_rw is a pretty good one. Depending on the situation you may be able to ust "enter" the function using congr and ext (or the more powerful congrm), but that typically only works if your goal is the equality you want to prove by rewriting. You can always do that in a have statement of course, but it can be a bit cumbersome. Another way is to enter conv mode (do we have some Lean4 documentation on conv?)

[Flo (Florent Schaffhauser)]

Thanks Anatole! Do you mean like https://leanprover-community.github.io/extras/conv.html
https://leanprover.github.io/theorem_proving_in_lean4/conv.html? I have not checked it out yet :sweat_smile:

[Alex J. Best]

Yes, but https://leanprover.github.io/theorem_proving_in_lean4/conv.html is a better place to read about it seeing as we haven't updated the conv docs on the website to lean 4 yet

[Jireh Loreaux]

There's a conv page on the actual mathlib4 docs.

[Jireh Loreaux]

https://leanprover-community.github.io/mathlib4_docs/docs/Conv/Guide.html

[Jireh Loreaux]

And

[Jireh Loreaux]

https://leanprover-community.github.io/mathlib4_docs/docs/Conv/Introduction.html