Zulip Chat Archive

(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

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] }

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

Alena Gusakov (Jun 24 2020 at 20:39):

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

Alena Gusakov (Jun 24 2020 at 20:39):

Gonna have to tinker with the list.map thing

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?

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

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

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

Alena Gusakov (Jun 24 2020 at 20:43):

Oof okay, good to know

Yakov Pechersky (Jun 24 2020 at 20:43):

I could be totally wrong though.

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

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.

Alena Gusakov (Jun 24 2020 at 20:45):

Oh no this one is gonna be really tedious

Alena Gusakov (Jun 24 2020 at 20:45):

@Alex J. Best so like, append elements?

Alena Gusakov (Jun 24 2020 at 20:46):

I don't really know how that would look

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

Alena Gusakov (Jun 24 2020 at 20:48):

Ahh okay I see

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

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.

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?

Jalex Stark (Jun 24 2020 at 20:51):

list.prod is defined for the empty list

Jalex Stark (Jun 24 2020 at 20:51):

and your theorem is true for it

Alena Gusakov (Jun 24 2020 at 20:51):

Okay yeah fair

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

Alena Gusakov (Jun 24 2020 at 20:52):

Gotcha, thank you!

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

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

Yakov Pechersky (Jun 24 2020 at 20:57):

It doesn't have the reversal going on, though

Jalex Stark (Jun 24 2020 at 20:57):

you're proving an easier lemma

Yakov Pechersky (Jun 24 2020 at 20:58):

Yeah, using comm

Jalex Stark (Jun 24 2020 at 20:58):

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

Yakov Pechersky (Jun 24 2020 at 20:58):

And Prod requires comm_monoid

Jalex Stark (Jun 24 2020 at 20:59):

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

Yakov Pechersky (Jun 24 2020 at 20:59):

Gotcha

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

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

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: Dec 20 2023 at 11:08 UTC