restating BigOperator as over indexed list

Stream: Is there code for X?

[Ralf Stephan]

Is there a lemma for this or similar? If not, where to look for parts of proof?

import Mathlib
set_option autoImplicit false
open Nat BigOperators Finset

example (S : Finset ℕ) (L : List ℕ) (hL : L = S.toList) (f : ℕ → ℕ)
  : ∏ i ∈ S, f i = ∏ i ∈ range S.card, f L[i]! := by sorry

[Yakov Pechersky]

I think you should first prove the lemma that relates the prod over fin L.length to L.prod f. Then use that in the proof with range L.length. Then use that here, after you subst hL and turn S.card to S.toList.length to L.length.

[Ralf Stephan]

I'm beginning to believe that this requires induction. Some pieces seem to be missing in Mathlib. So far:

import Mathlib
set_option autoImplicit false
open Nat BigOperators Finset

example (S : Finset ℕ) (L : List ℕ) (hL : L = S.toList) (f : ℕ → ℕ)
  : ∏ i ∈ S, f i = ∏ i ∈ range S.card, f L[i]! := by
  have h₃ : ∏ i : Fin L.length, f L[i]! = (L.map f).prod := by
    rw [hL, prod_to_list S f]
    sorry
  rw [←prod_to_list S f, ←length_toList, ←hL, ←h₃]
  rw [prod_range fun i => f L[i]!]
  rfl

[Yaël Dillies]

You should use Finset.card_congr (soon to be called `card_bij

[Ralf Stephan]

I don't see an advantage of it (feel free to move to New Members).

[Yakov Pechersky]

Following my plan

import Mathlib
set_option autoImplicit false
open Nat BigOperators Finset

lemma foo {α G : Type*} [CommMonoid G] (l : List α) (f : α → G) :
    ∏ (i : Fin l.length), f l[i] = (l.map f).prod := by
  simp

@[simp]
lemma getbang_natCast_eq_get {α : Type*} [Inhabited α] (l : List α) (i : Fin l.length) :
    l[(i : ℕ)]! = l[i] := by
  exact getElem!_pos l (↑i) (Fin.val_lt_of_le i (le_refl l.length)) -- by exact?

lemma bar {α G : Type*} [Inhabited α] [CommMonoid G] (l : List α) (f : α → G) :
    ∏ i ∈ range l.length, f l[i]! = (l.map f).prod := by
  rw [← foo, prod_range, prod_congr rfl]
  simp

example (S : Finset ℕ) (L : List ℕ) (hL : L = S.toList) (f : ℕ → ℕ) :
    ∏ i ∈ S, f i = ∏ i ∈ range S.card, f L[i]! := by
  subst hL
  simp_rw [← Finset.length_toList]
  simp

[Ralf Stephan]

Rewriting with calc, but I don't see how to close foo.

import Mathlib
set_option autoImplicit false
open Nat BigOperators Finset

lemma foo {α G : Type*} [CommMonoid G] (l : List α) (f : α → G) :
    (l.map f).prod = ∏ (i : Fin l.length), f l[i]  := by
  simp only [Fin.getElem_fin, List.getElem_eq_get, Fin.eta]
  --apply? didn't find any relevant lemmas
  sorry

lemma getbang_natCast_eq_get {α : Type*} [Inhabited α] (l : List α) (i : Fin l.length) :
    l[(i : ℕ)]! = l[i] := by
  exact getElem!_pos l (↑i) (Fin.val_lt_of_le i (le_refl l.length))

example {α G : Type*} [CommMonoid G] [Inhabited α] (L : List α) (f : α → G) (S : Finset α) (hL : L = S.toList) :
    ∏ i ∈ S, f i = ∏ i ∈ range S.card, f L[i]! :=
  calc
    ∏ i ∈ S, f i = (List.map f S.toList).prod := by rw [prod_to_list]
    _ = (L.map f).prod := by rw [hL]
    _ = ∏ (i : Fin L.length), f L[i] := by rw [foo]
    _ = ∏ (i : Fin L.length), f L[(i : ℕ)]! := by simp_rw [getbang_natCast_eq_get]
    _ = ∏ i ∈ range L.length, f L[i]! := by simp_rw [prod_range]
    _ = ∏ i ∈ range S.card, f L[i]! := by rw [hL, ← length_toList]

[Ruben Van de Velde]

import Mathlib
set_option autoImplicit false
open Nat BigOperators Finset

lemma foo {α G : Type*} [CommMonoid G] (l : List α) (f : α → G) :
    (l.map f).prod = ∏ (i : Fin l.length), f l[i]  := by
  simp only [Fin.getElem_fin, List.getElem_eq_get, Fin.eta]
  induction l with
  | nil => simp
  | cons head tail ih =>
    simp
    rw [ih]
    exact Eq.symm (Fin.prod_univ_succ fun i => f ((head :: tail).get i)) -- apply?

[Ralf Stephan]

Completely over my head, but thanks!

[Ralf Stephan]

Final question, should the complete lemma go in mathlib (maybe Algebra.BigOperators.Intervals)?

[Yakov Pechersky]

In live-lean, foo is proved by simp directly.

[Yakov Pechersky]

I think in both cases of your foo and your example. the LHS is simpler. And I think that a lemma that has a a = b.toList hypothesis is rarely going to be directly applicable, because anyone that has that hypothesis could/should subst it right away.

[Yakov Pechersky]

How did you end up in a toList situation to begin with?

[Ralf Stephan]

The lemma is Lemma 0.9 on this page. You can see that the index k is needed later to prove that the nth prime >= n+2 which is needed for the inequality 0.10.

I think you're right that this is not sufficiently useful, as I found now Fin.prod_univ_get' which is close enough, and I'll try again to base everything on that. But it was good to see which mechanics are needed for such conversions.