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

#4738

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

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?

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

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

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

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