Zulip Chat Archive

Stream: Is there code for X?

Topic: Product of a reversed list is inverse of product of inverses


view this post on Zulip Eric Wieser (Oct 22 2020 at 08:58):

I'm pretty sure this lemma is true modulo typos: (proven)

@[to_additive]
lemma prod_reverse (α : Type*) [group α]  :  (l : list α), l.reverse.prod = (l.map (λ x, x⁻¹)).prod⁻¹
| [] := by simp
| (x :: xs) := by simp [prod_reverse xs]

Does this exist anywhere?

view this post on Zulip Eric Wieser (Oct 22 2020 at 11:33):

#4738

view this post on Zulip Eric Wieser (Oct 22 2020 at 14:28):

That PR adds

lemma prod_inv_reverse :  (L : list α), L.prod⁻¹ = (L.map (λ x, x⁻¹)).reverse.prod

However, I've realized I still want the original in this thread,

lemma what :  (L : list α), l.reverse.prod = (l.map (λ x, x⁻¹)).prod⁻¹

What should this second lemma be called?

view this post on Zulip Reid Barton (Oct 22 2020 at 14:30):

I think prod_reverse is a fine name

view this post on Zulip Reid Barton (Oct 22 2020 at 14:31):

Is there another right hand side that a lemma of that name could have?

view this post on Zulip Eric Wieser (Oct 22 2020 at 14:41):

prod_reverse could be for a version with comm_group that says l.prod = l.reverse.prod

view this post on Zulip Reid Barton (Oct 22 2020 at 14:41):

prod_reverse_noncomm?

view this post on Zulip Reid Barton (Oct 22 2020 at 14:42):

or it could also be prod_reverse_eq_inv_prod_inv or something

view this post on Zulip Eric Wieser (Oct 22 2020 at 14:42):

For my what lemma, you mean?

view this post on Zulip Reid Barton (Oct 22 2020 at 14:42):

Yes

view this post on Zulip Eric Wieser (Oct 22 2020 at 14:43):

prod_reverse_noncomm seems reasonable, and I could add prod_reverse in the same PR

view this post on Zulip Adam Topaz (Oct 22 2020 at 14:56):

What about prod_inv (for a name). cf. docs#mul_inv

view this post on Zulip Adam Topaz (Oct 22 2020 at 14:57):

Or list_mul_inv if there's a concern about name conflicts when the list namespace is open.

view this post on Zulip Adam Topaz (Oct 22 2020 at 14:59):

Wait, I thought there was a version of mul_invfor noncommutative groups.

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:00):

Oh, it's called docs#mul_inv_rev

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:01):

So I think prod_inv_reverse should be called prod_inv_rev.

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:03):

Is there an analogue of what for a product of two elements?

view this post on Zulip Johan Commelin (Oct 22 2020 at 15:05):

In Leiden it would be called socks_and_shoes

view this post on Zulip Johan Commelin (Oct 22 2020 at 15:06):

Because, well, if you first put on your socks, and then your shoes, you should remove them in the reverse order.

view this post on Zulip Eric Wieser (Oct 22 2020 at 15:06):

So I think prod_inv_reverse should be called prod_inv_rev.

I went for reverse so it contained the function name - but I made sure to include mul_inv_rev in the docstring

view this post on Zulip Eric Wieser (Oct 22 2020 at 15:06):

Is there an analogue of what for a product of two elements?

No, which surprised me - we don't seem to have (a⁻¹ * b⁻¹)⁻¹ = b * a or the reverse

view this post on Zulip Johan Commelin (Oct 22 2020 at 15:07):

So in the first year algebra course the lemma (x * y) \inv = y \inv * x \inv has this funny name :smile:

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:07):

Eric Wieser said:

Is there an analogue of what for a product of two elements?

No, which surprised me - we don't seem to have (a⁻¹ * b⁻¹)⁻¹ = b * a

I think by simp would solve this.

view this post on Zulip Eric Wieser (Oct 22 2020 at 15:08):

Yes, it would

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:08):

because of the mul_inv_rev and inv_inv lemmas

view this post on Zulip Eric Wieser (Oct 22 2020 at 15:08):

But perhaps a lemma is still useful so it can be referred to by name?

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:08):

Maybe, but surely it shouldn't be a simp lemma.

view this post on Zulip Eric Wieser (Oct 22 2020 at 15:09):

Oh for sure it shouldn't be simp

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:09):

I'm just thinking of how I would actually use it in a proof, and I would always solve such things by simp, so I'm not sure I would ever actually use a lemma which says (a⁻¹ * b⁻¹)⁻¹ = b * a.

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:11):

socks_and_shoes or underwear_and_pants?

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:16):

It's a little silly that simp doesn't solve the following

import algebra

variables (G : Type*) [group G] (L : list G)

example : L.map (λ x, x⁻¹⁻¹) = L := sorry -- by simp doesn't solve this.

view this post on Zulip Yakov Pechersky (Oct 22 2020 at 15:17):

import algebra

variables (G : Type*) [group G] (L : list G)

example : L.map (λ x, x⁻¹⁻¹) = L := by ext; simp

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:18):

Sure, but I would like to be able to make prod_inv_reverse into a simp lemma, and be able to solve what with by simp.

view this post on Zulip Mario Carneiro (Oct 22 2020 at 15:23):

there should be a map_id' lemma that helps simp solve statements like that

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:23):

import algebra

variables (G : Type*) [group G] (L : list G)

@[simp] lemma foo : (λ (x : G), x⁻¹⁻¹) = id := by {ext, simp}

@[simp] lemma bar {α} : (λ x : α, x) = id := rfl

example : L.map (λ x, x⁻¹⁻¹) = L := by simp

view this post on Zulip Mario Carneiro (Oct 22 2020 at 15:24):

I don't think bar can work as a simp lemma itself, it would cause too many other problems

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:24):

import algebra

variables (G : Type*) [group G] (L : list G)

example : L.map (λ x, x⁻¹⁻¹) = L := by tidy

view this post on Zulip Mario Carneiro (Oct 22 2020 at 15:25):

map_id' just says L.map (\lam x, x) = L

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:25):

Oh okay.

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:26):

Is there a tactic that's weaker than tidy which only does ext and simp?

view this post on Zulip Mario Carneiro (Oct 22 2020 at 15:26):

ext; simp

view this post on Zulip Adam Topaz (Oct 22 2020 at 15:26):

What happens if you have to introduce more ext after a simp?

view this post on Zulip Mario Carneiro (Oct 22 2020 at 15:27):

ext; simp; ext

view this post on Zulip Mario Carneiro (Oct 22 2020 at 15:27):

actually I don't find it that often

view this post on Zulip Mario Carneiro (Oct 22 2020 at 15:28):

you can try using something like simp [ext_iff] but YMMV

view this post on Zulip Eric Wieser (Oct 22 2020 at 15:31):

#4744 helps a little with example : L.map (λ x, x⁻¹⁻¹) = L := by simp. At any rate, it suffices to solve what by simp

view this post on Zulip Eric Wieser (Oct 23 2020 at 13:53):

Turns out docs#list.prod_reverse already exists!

view this post on Zulip Yakov Pechersky (Oct 23 2020 at 13:57):

I think what's missing from that file, or from the general theory of permutations (which is somewhat scattered across mathlib across different areas of interest), is that a pairwise swap is a product of adjacent swaps.

view this post on Zulip Eric Wieser (Oct 23 2020 at 13:58):

That's what I had originally set out to prove, and need this lemma for

view this post on Zulip Kevin Buzzard (Oct 23 2020 at 14:09):

@Mario Carneiro is the master at this sort of thing -- if it's there he'll know where it is :-) (because he will have put it there!)

view this post on Zulip Mario Carneiro (Oct 23 2020 at 14:10):

I haven't done that one, but it sounds like it would fall out of the work needed for the alternating group

view this post on Zulip Mario Carneiro (Oct 23 2020 at 14:13):

plus there is the question of how to phrase "adjacent" in appropriately general way

view this post on Zulip Mario Carneiro (Oct 23 2020 at 14:22):

Maybe this?

import group_theory.perm.sign

open_locale classical
open equiv

theorem foo {α} (R : α  α  Prop) {x y : α} (hr : relation.refl_trans_gen R x y) :
   l : list (perm α), swap x y = l.prod   p  l,  a b, R a b  p = swap a b :=
_

view this post on Zulip Eric Wieser (Oct 23 2020 at 14:23):

I think we already have that

view this post on Zulip Eric Wieser (Oct 23 2020 at 14:23):

It's the _adjacent_ swap theorem we don't have

view this post on Zulip Mario Carneiro (Oct 23 2020 at 14:23):

That's what that is

view this post on Zulip Eric Wieser (Oct 23 2020 at 14:24):

Whoops, I missed R a b there. Is docs#relation.refl_trans_gen the magic there?

view this post on Zulip Mario Carneiro (Oct 23 2020 at 14:24):

To get the result for adjacent swaps you have to supply \lam x y, x = y + 1 as R and then prove that refl_trans_gen R holds for any two nats/fins or what have you

view this post on Zulip Mario Carneiro (Oct 23 2020 at 14:25):

Actually I guess it could use eqv_gen, since swap is commutative

view this post on Zulip Eric Wieser (Oct 23 2020 at 14:27):

I suppose you could make that actually compute the list with (next : α → α) (hr : relation.refl_trans_gen (fun x y, next x = y) x y)

view this post on Zulip Mario Carneiro (Oct 23 2020 at 14:30):

that's just a special case

view this post on Zulip Mario Carneiro (Oct 23 2020 at 14:31):

It's an existential even then because of refl_trans_gen which is a prop

view this post on Zulip Eric Wieser (Oct 23 2020 at 14:33):

I'm not sure I agree with that - I was able to computably obtain the list in #4379 for when α is nat, and I think all I needed was next and a transitive relation

view this post on Zulip Mario Carneiro (Oct 23 2020 at 14:49):

You also need to know the length of the sequence

view this post on Zulip Mario Carneiro (Oct 23 2020 at 14:50):

which is possible on nat and similar things but amounts to the enum class that @Anne Baanen proposed in the other thread

view this post on Zulip Mario Carneiro (Oct 23 2020 at 14:52):

import group_theory.perm.sign

namespace list
section group
variables {α : Type*} [group α]

/-- This is the `list.prod` version of `mul_inv_rev` -/
@[to_additive "This is the `list.sum` version of `add_neg_rev`"]
lemma prod_inv_reverse :  (L : list α), L.prod⁻¹ = (L.map (λ x, x⁻¹)).reverse.prod
| [] := by simp
| (x :: xs) := by simp [prod_inv_reverse xs]

end group
end list

open equiv

theorem foo {α} [decidable_eq α] (R : α  α  Prop) {x y : α} (hr : eqv_gen R x y) :
   l : list (perm α), swap x y = l.prod   p  l,  a b, R a b  p = swap a b :=
begin
  have Hrefl :  x,  l : list (perm α),
    swap x x = l.prod   p  l,  a b, R a b  p = swap a b :=
    λ x, ⟨[], by simp [swap_self]; refl, by rintro _ ⟨⟩⟩,
  induction hr,
  case rel : x y hr {
    refine ⟨[swap x y], by simp, _⟩,
    simp only [forall_eq, list.mem_singleton],
    exact _, _, hr, rfl },
  case refl : x { apply Hrefl },
  case symm : x y hr IH {
    obtain l, e, H := IH,
    refine ⟨(l.map (λ x, x⁻¹)).reverse, _, λ p h, _⟩,
    { rw [ list.prod_inv_reverse,  e, swap_inv, swap_comm] },
    { simp at h,
      obtain p, hp, rfl := h,
      obtain a, b, hr, rfl := H _ hp,
      exact a, b, hr, by simp } },
  case trans : x y z hr₁ hr₂ IH₁ IH₂ {
    obtain ⟨⟨l₁, e₁, H₁⟩, l₂, e₂, H₂⟩⟩ := IH₁, IH₂⟩,
    by_cases zy : z = y, { subst z, exact l₁, e₁, H₁ },
    by_cases zx : z = x, { subst z, apply Hrefl },
    refine l₁ ++ l₂ ++ l₁, _, λ p h, _⟩,
    { rw swap_comm at e₁ e₂,
      rw [list.prod_append, list.prod_append,  e₁,  e₂, perm.swap_mul_swap_mul_swap zy zx] },
    { simp [or.right_comm] at h, exact h.elim (H₁ _) (H₂ _) } }
end

view this post on Zulip Eric Wieser (Oct 23 2020 at 15:00):

I was looking for docs#equiv.perm.swap_mul_swap_mul_swap...

view this post on Zulip Mario Carneiro (Oct 23 2020 at 15:01):

it should be in equiv.basic

view this post on Zulip Eric Wieser (Oct 23 2020 at 15:02):

Or should equiv.swap be renamed to equiv.perm.swap?

view this post on Zulip Mario Carneiro (Oct 23 2020 at 15:04):

maybe? It is an equiv though

view this post on Zulip Eric Wieser (Oct 23 2020 at 15:05):

Well, so are all perms

view this post on Zulip Eric Wieser (Oct 23 2020 at 15:06):

And it's defined as def swap (a b : α) : perm α


Last updated: May 17 2021 at 15:13 UTC