# Zulip Chat Archive

## Stream: Is there code for X?

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

#### 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?

#### Eric Wieser (Oct 22 2020 at 11:33):

#### 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?

#### Reid Barton (Oct 22 2020 at 14:30):

I think `prod_reverse`

is a fine name

#### Reid Barton (Oct 22 2020 at 14:31):

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

#### 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`

#### Reid Barton (Oct 22 2020 at 14:41):

`prod_reverse_noncomm`

?

#### Reid Barton (Oct 22 2020 at 14:42):

or it could also be `prod_reverse_eq_inv_prod_inv`

or something

#### Eric Wieser (Oct 22 2020 at 14:42):

For my `what`

lemma, you mean?

#### Reid Barton (Oct 22 2020 at 14:42):

Yes

#### Eric Wieser (Oct 22 2020 at 14:43):

`prod_reverse_noncomm`

seems reasonable, and I could add `prod_reverse`

in the same PR

#### Adam Topaz (Oct 22 2020 at 14:56):

What about `prod_inv`

(for a name). cf. docs#mul_inv

#### 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.

#### Adam Topaz (Oct 22 2020 at 14:59):

Wait, I thought there was a version of `mul_inv`

for noncommutative groups.

#### Adam Topaz (Oct 22 2020 at 15:00):

Oh, it's called docs#mul_inv_rev

#### Adam Topaz (Oct 22 2020 at 15:01):

So I think `prod_inv_reverse`

should be called `prod_inv_rev`

.

#### Adam Topaz (Oct 22 2020 at 15:03):

Is there an analogue of `what`

for a product of two elements?

#### Johan Commelin (Oct 22 2020 at 15:05):

In Leiden it would be called `socks_and_shoes`

#### 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.

#### 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

#### 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

#### 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:

#### 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.

#### Eric Wieser (Oct 22 2020 at 15:08):

Yes, it would

#### Adam Topaz (Oct 22 2020 at 15:08):

because of the `mul_inv_rev`

and `inv_inv`

lemmas

#### Eric Wieser (Oct 22 2020 at 15:08):

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

#### Adam Topaz (Oct 22 2020 at 15:08):

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

#### Eric Wieser (Oct 22 2020 at 15:09):

Oh for sure it shouldn't be `simp`

#### 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`

.

#### Adam Topaz (Oct 22 2020 at 15:11):

`socks_and_shoes`

or `underwear_and_pants`

?

#### 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.
```

#### 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
```

#### 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`

.

#### Mario Carneiro (Oct 22 2020 at 15:23):

there should be a `map_id'`

lemma that helps simp solve statements like that

#### 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
```

#### 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

#### 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
```

#### Mario Carneiro (Oct 22 2020 at 15:25):

`map_id'`

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

#### Adam Topaz (Oct 22 2020 at 15:25):

Oh okay.

#### Adam Topaz (Oct 22 2020 at 15:26):

Is there a tactic that's weaker than `tidy`

which only does `ext`

and `simp`

?

#### Mario Carneiro (Oct 22 2020 at 15:26):

`ext; simp`

#### Adam Topaz (Oct 22 2020 at 15:26):

What happens if you have to introduce more `ext`

after a `simp`

?

#### Mario Carneiro (Oct 22 2020 at 15:27):

`ext; simp; ext`

#### Mario Carneiro (Oct 22 2020 at 15:27):

actually I don't find it that often

#### Mario Carneiro (Oct 22 2020 at 15:28):

you can try using something like `simp [ext_iff]`

but YMMV

#### 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`

#### Eric Wieser (Oct 23 2020 at 13:53):

Turns out docs#list.prod_reverse already exists!

#### 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.

#### Eric Wieser (Oct 23 2020 at 13:58):

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

#### 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!)

#### 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

#### Mario Carneiro (Oct 23 2020 at 14:13):

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

#### 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 :=
_
```

#### Eric Wieser (Oct 23 2020 at 14:23):

I think we already have that

#### Eric Wieser (Oct 23 2020 at 14:23):

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

#### Mario Carneiro (Oct 23 2020 at 14:23):

That's what that is

#### Eric Wieser (Oct 23 2020 at 14:24):

Whoops, I missed `R a b`

there. Is docs#relation.refl_trans_gen the magic there?

#### 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

#### Mario Carneiro (Oct 23 2020 at 14:25):

Actually I guess it could use `eqv_gen`

, since `swap`

is commutative

#### 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)`

#### Mario Carneiro (Oct 23 2020 at 14:30):

that's just a special case

#### Mario Carneiro (Oct 23 2020 at 14:31):

It's an existential even then because of `refl_trans_gen`

which is a prop

#### 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

#### Mario Carneiro (Oct 23 2020 at 14:49):

You also need to know the length of the sequence

#### 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

#### 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
```

#### Eric Wieser (Oct 23 2020 at 15:00):

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

#### Mario Carneiro (Oct 23 2020 at 15:01):

it should be in `equiv.basic`

#### Eric Wieser (Oct 23 2020 at 15:02):

Or should `equiv.swap`

be renamed to `equiv.perm.swap`

?

#### Mario Carneiro (Oct 23 2020 at 15:04):

maybe? It is an equiv though

#### Eric Wieser (Oct 23 2020 at 15:05):

Well, so are all perms

#### 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