Product of a reversed list is inverse of product of inverses

Stream: Is there code for X?

[Eric Wieser]

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]

#4738

[Eric Wieser]

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]

I think prod_reverse is a fine name

[Reid Barton]

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

[Eric Wieser]

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

[Reid Barton]

prod_reverse_noncomm?

[Reid Barton]

or it could also be prod_reverse_eq_inv_prod_inv or something

[Eric Wieser]

For my what lemma, you mean?

[Reid Barton]

Yes

[Eric Wieser]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

Oh, it's called docs#mul_inv_rev

[Adam Topaz]

So I think prod_inv_reverse should be called prod_inv_rev.

[Adam Topaz]

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

[Johan Commelin]

In Leiden it would be called socks_and_shoes

[Johan Commelin]

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

[Eric Wieser]

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]

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]

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

[Adam Topaz]

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]

Yes, it would

[Adam Topaz]

because of the mul_inv_rev and inv_inv lemmas

[Eric Wieser]

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

[Adam Topaz]

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

[Eric Wieser]

Oh for sure it shouldn't be simp

[Adam Topaz]

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]

socks_and_shoes or underwear_and_pants?

[Adam Topaz]

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]

import algebra

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

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

[Adam Topaz]

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]

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

[Adam Topaz]

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]

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

[Adam Topaz]

import algebra

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

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

[Mario Carneiro]

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

[Adam Topaz]

Oh okay.

[Adam Topaz]

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

[Mario Carneiro]

ext; simp

[Adam Topaz]

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

[Mario Carneiro]

ext; simp; ext

[Mario Carneiro]

actually I don't find it that often

[Mario Carneiro]

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

[Eric Wieser]

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

Turns out docs#list.prod_reverse already exists!

[Yakov Pechersky]

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]

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

[Kevin Buzzard]

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

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

I think we already have that

[Eric Wieser]

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

[Mario Carneiro]

That's what that is

[Eric Wieser]

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

[Mario Carneiro]

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]

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

[Eric Wieser]

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]

that's just a special case

[Mario Carneiro]

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

[Eric Wieser]

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]

You also need to know the length of the sequence

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

it should be in equiv.basic

[Eric Wieser]

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

[Mario Carneiro]

maybe? It is an equiv though

[Eric Wieser]

Well, so are all perms

[Eric Wieser]

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