Zulip Chat Archive

Stream: new members

Topic: iterating over subscripts & generalizing products


view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:24):

So if I want to prove a statement like (a₁ * a₂ * ... * a_n)⁻¹ = a_n⁻¹ *...*a₂⁻¹ *a₁⁻¹, how would I write it out?

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:25):

check out docs#finset.prod

view this post on Zulip Aniruddh Agarwal (Jun 24 2020 at 20:26):

Jalex beat me to it :P

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:26):

it has many useful lemmas :)

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:27):

you can win the race next time if you use the linkifier

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:30):

ah this won't work, finset.prod is about commutative multiplication

view this post on Zulip Alex J. Best (Jun 24 2020 at 20:32):

docs#inv_prod ?

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:33):

that looks like the theorem alena asked about

view this post on Zulip Aniruddh Agarwal (Jun 24 2020 at 20:34):

docs#list.prod

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:34):

Yeah I'm trying to prove it

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:35):

list.prod takes care of the product, but I still don't get how to iterate over subscripts. Is there some list constructor for that?

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:36):

(list.map a (list.range n)), where (a : ℕ → G) and G is your group. I don't think we have something like python list comprehensions, if that's what you're asking

view this post on Zulip Yakov Pechersky (Jun 24 2020 at 20:38):

example {a b c d : } : (a * b * c * d)⁻¹ = d⁻¹ * c⁻¹ * b⁻¹ * a⁻¹ :=
by { simp [mul_inv', mul_assoc] }

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:38):

I don't know exactly how to phrase my question haha sorry, though I do think what you gave me is what I'm looking for

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:39):

I'm trying to solve it for all n so it's an induction type proof

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:39):

Gonna have to tinker with the list.map thing

view this post on Zulip Yakov Pechersky (Jun 24 2020 at 20:40):

Do you have an example of the place you need to do it at in a #mwe?

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:41):

Like the proof itself? It's just an exercise, I'm trying to go through Dummit and Foote and prove basic stuff

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:42):

I think this is mathematically the right statement

import tactic

variables (G : Type*) [group G] (n : ) (a :   G)

example :
(list.map a (list.range n)).prod⁻¹ = (list.map (λ x, (a x)⁻¹) (list.range n).reverse).prod :=
begin
  sorry
end

view this post on Zulip Yakov Pechersky (Jun 24 2020 at 20:42):

From what I've learned on this channel is that statements about general a_1, ... a_i, ..., a_n aren't very Lean friendly

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:43):

Oof okay, good to know

view this post on Zulip Yakov Pechersky (Jun 24 2020 at 20:43):

I could be totally wrong though.

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:44):

i think working with a list is slightly harder than working with a finset, but i think working with lists in lean is not much more awkward than working with lists in haskell

view this post on Zulip Alex J. Best (Jun 24 2020 at 20:44):

Its probably best when doing problems like this to use a list L and do induction on L instead of indices directly.

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:45):

Oh no this one is gonna be really tedious

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:45):

@Alex J. Best so like, append elements?

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:46):

I don't really know how that would look

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:46):

I think Alex is suggesting that the statement you want to prove is literally docs#inv_prod

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:48):

Ahh okay I see

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:48):

here's the statement, for anyone that doesn't follow the link

lemma inv_prod {G : Type*} [group G] (l : list G) :
(l.prod)⁻¹ = (list.map (λ x , x⁻¹) l.reverse).prod

view this post on Zulip Alex J. Best (Jun 24 2020 at 20:48):

So yeah the lemma is in mathlib, but you should totally try and prove it still!
Yes, lists are defined as an inductive type, so the empty list is a list, and if L is a list and a is an element, then a :: L is also a list, this notation means append a to the start of L, so a :: [b,c] is [a, b, c], or this is a :: b :: c :: [].
Because its an inductive type doing the induction on lists of different lengths works well, just call induction L to split into these two cases the empty list and a :: L for some a  and L.

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:50):

In this case would it be a good idea to start with an a :: [] appended already since the statement doesn't really mean anything on an empty list? Or is that a perfectly valid thing to do?

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:51):

list.prod is defined for the empty list

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:51):

and your theorem is true for it

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:51):

Okay yeah fair

view this post on Zulip Alex J. Best (Jun 24 2020 at 20:51):

Well the advantage of the empty list is that a lot of statements are trivial for that, compared to a :: [], [].prod =1 for example.
BTW the setup for induction would be like this:

lemma inv_prod {α : Type*} [group α] (L : list α) : L.prod⁻¹ = (L.reverse.map (λ x, x⁻¹)).prod :=
begin
  induction L,
  { sorry },
  { sorry },
end

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:52):

Gotcha, thank you!

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:55):

If you want to start from a black box and work backwards, simp can do all the bits, and squeeze_simp will tell you what simp found

import tactic

lemma inv_prod {G : Type*} [group G] (l : list G) :
(list.prod l)⁻¹ = (list.map (λ x, x⁻¹) l.reverse).prod :=
begin
  induction l with hd tl h,
  squeeze_simp,
  squeeze_simp [h],
end

view this post on Zulip Yakov Pechersky (Jun 24 2020 at 20:55):

fin version seems more natural to me

import tactic
import algebra.big_operators
import data.fintype.card

open_locale big_operators

variables (G : Type*) [comm_group G] (n : ) (a : fin n.succ  G)

example :
( i, (a i))⁻¹ =  i, (a i)⁻¹ :=
begin
  induction n with k hk,
  simp,
  simp [fin.prod_univ_succ, mul_inv],
end

view this post on Zulip Yakov Pechersky (Jun 24 2020 at 20:57):

It doesn't have the reversal going on, though

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:57):

you're proving an easier lemma

view this post on Zulip Yakov Pechersky (Jun 24 2020 at 20:58):

Yeah, using comm

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:58):

you're taking an unordered product of elements of a commutative group

view this post on Zulip Yakov Pechersky (Jun 24 2020 at 20:58):

And Prod requires comm_monoid

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:59):

right, that's why we were not using the big operator stuff

view this post on Zulip Yakov Pechersky (Jun 24 2020 at 20:59):

Gotcha

view this post on Zulip Jalex Stark (Jun 24 2020 at 20:59):

it might not be hard to define big operators over lists, but afaik nobody has done it

view this post on Zulip Bryan Gin-ge Chen (Jun 24 2020 at 21:06):

Patrick is fond of recommending the paper on Coq's big operator library: https://hal.inria.fr/inria-00331193/PDF/main.pdf

view this post on Zulip Jalex Stark (Jun 24 2020 at 21:44):

This works for doing list.prod through notation (though there's an embarrassingly simple sorry)

import tactic

localized "notation `∏` binders ` in ` l `, ` r:(scoped:67 f, (list.map f l).prod) := r" in big_list_prod

variables (G : Type*) [comm_group G] (n : ) (a :   G)

open list
open_locale big_list_prod

@[simp]
lemma range_zero : range 0 = nil := rfl

@[simp]
lemma range_succ (n : ) : range n.succ = n :: range n := sorry

example (n : ) :
 i in range n, (a i)⁻¹ = ( i in (range n).reverse, a i)⁻¹ :=
begin
  induction n with d hd,
  { simp },
  simp [hd],
end

Last updated: May 15 2021 at 02:11 UTC