# Zulip Chat Archive

## Stream: new members

### Topic: Transpositions of adjacent elements

#### Zhangir Azerbayev (Aug 03 2020 at 13:42):

Every transposition of `fin n`

can be decomposed into transpositions of adjacent elements. @Kevin Buzzard pointed out to me that, in some sense, mathlib already knows this, since `list.perm`

has the constructor

```
| swap : ∀ {α : Type uu} (a a_1 : list α) (l : list α), a_1 :: a :: l ~ a :: a_1 :: l
```

I want to extract from this either

- A lemma that says any
`equiv.swap i j`

with`i j : fin n`

can be decomposed into a product of an odd number of elements of the form`equiv.swap i (i+1)`

, or - An induction principle similar to
`equiv.perm.swap_induction_on`

, which would say something like

```
∀ (i j : fin n), P 1 → (∀ (f : equiv.perm (fin n)) (i : fin n),
P f → P (equiv.swap i (i + 1) * f)) → P (equiv.swap i j)
```

or

```
∀ f : equiv.perm (fin n) , P 1 → (∀ (f : equiv.perm (fin n)) (i : fin n),
P f → P (equiv.swap i (i + 1) * f)) → P f
```

How could one prove this?

#### Kevin Buzzard (Aug 03 2020 at 13:44):

Your definition of swap quoted above looks funny -- a should have type alpha surely

#### Kevin Buzzard (Aug 03 2020 at 13:45):

swap says that [a,b,c,...] is related to [b,a,c,...]. It's part of the definition of a binary relation on lists

#### Kevin Buzzard (Aug 03 2020 at 13:46):

I don't think the questions you're asking typecheck

#### Kevin Buzzard (Aug 03 2020 at 13:47):

Oh sorry are there two swaps here?

#### Kevin Buzzard (Aug 03 2020 at 13:49):

You can prove 1, assuming I've understood it correctly, directly by writing it as an explicit product of something like 2(j-i-1)+1 adjacent swaps

#### Zhangir Azerbayev (Aug 03 2020 at 13:51):

The definition I wrote is wrong, it's actually

```
| swap : Π (x y : α) (l : list α), perm (y::x::l) (x::y::l)
```

The thing I wrote in my question is what shows up on the mathlib docs website (https://leanprover-community.github.io/mathlib_docs/data/list/perm.html#list.is_setoid), which is different from what's in source code.

#### Kevin Buzzard (Aug 03 2020 at 13:52):

Your induction principle might not quite be what you want because i+1 is random if n=i+1

#### Kevin Buzzard (Aug 03 2020 at 13:53):

@Kendall Frey you're not the only one doing permutations of `fin n`

#### Mario Carneiro (Aug 03 2020 at 14:10):

wait, don't tell me this is the next evolution stage of the `a`

bug

#### Reid Barton (Aug 03 2020 at 14:16):

The only real problem is the `{α : Type uu}`

part, right?

#### Mario Carneiro (Aug 03 2020 at 14:23):

no, the `a`

and `a_1`

binders have the wrong type

#### Mario Carneiro (Aug 03 2020 at 14:25):

which, incidentally, means we have found an entirely new kind of pollack inconsistency in lean

#### Reid Barton (Aug 03 2020 at 14:26):

oh neat

#### Mario Carneiro (Aug 03 2020 at 14:36):

Oh, the bug is in `doc_gen`

#### Mario Carneiro (Aug 03 2020 at 14:38):

Here's a standalone version of the bug:

```
import tactic.basic data.list.perm
open tactic
meta def expr.instantiate_pis : list expr → expr → expr
| (e'::es) (expr.pi n bi t e) := expr.instantiate_pis es (e.instantiate_var e')
| _ e := e
meta def mk_const_with_params (d : declaration) : expr :=
let lvls := d.univ_params.map level.param in
expr.const d.to_name lvls
#eval do
d ← get_decl ``list.perm,
t ← infer_type (mk_const_with_params d),
(locs, _) ← mk_local_pis t,
trace (list.map expr.local_type locs), -- [Type uu, list α, list α]
proj_tp ← mk_const ``list.perm.swap >>= infer_type,
t ← pis locs (proj_tp.instantiate_pis locs),
trace t -- ∀ {α : Type uu} (a a_1 : list α) (l : list α), a_1 :: a :: l ~ a :: a_1 :: l
```

#### Mario Carneiro (Aug 03 2020 at 14:40):

It looks like the code has assumed that the first three binders of `list.perm.swap`

have types `[Type uu, list α, list α]`

respectively

#### Mario Carneiro (Aug 03 2020 at 14:41):

in other words, it confused the indices of the inductive family `inductive list.perm {α : Type uu} : list α → list α → Prop`

for parameters

#### Kevin Buzzard (Aug 03 2020 at 18:13):

Back to the original point, Zhangir Chris and I knocked up the following in the live lean coding discord chat:

```
import data.equiv.basic
import group_theory.perm.sign
import tactic
open equiv
lemma zhangir1 (n : ℕ) (i j : fin n) (hij : i ≠ j) : ∃ L : list (perm (fin n)),
L.prod = equiv.swap i j ∧ ∀ l ∈ L, ∃ k : fin n, ∃ h : k.1 + 1 < n,
l = equiv.swap k ⟨k.1 + 1, h⟩ :=
begin
wlog h1 : i < j using [i j, j i],
{ rcases lt_trichotomy i j with h1 | rfl | h3,
{ left, assumption },
{ exfalso, cc },
{ right, assumption }
},
{ cases j with j hj,
cases i with i hi,
change i < j at h1,
clear hij,
revert hj,
refine nat.le_induction _ _ j (show i+1 ≤ j, from h1),
{ intro hj,
let L := [swap (⟨i, hi⟩ : fin n) ⟨i + 1, hj⟩],
use L,
split, simp,
intros l hl,
use i, exact hi,
use hj,
cases hl, exact hl,
cases hl },
{ clear h1 j,
intros j hj h hj',
have hjn : j < n := lt_trans (nat.lt_succ_self j) hj',
rcases h hjn with ⟨L, hL1, hL2⟩,
let M := [swap (⟨j, hjn⟩ : fin n) (⟨j+1, hj'⟩)] ++ L ++ [swap (⟨j, hjn⟩ : fin n) (⟨j+1, hj'⟩)],
use M,
split,
{ rw [list.prod_append, list.prod_append, hL1, list.prod_singleton],
rw swap_comm (fin.mk i _) (fin.mk (j+1) _),
apply perm.swap_mul_swap_mul_swap,
{ apply ne_of_lt, exact hj },
{ apply ne_of_lt, show i < j+1, linarith } },
{ intros l hl,
rw [list.mem_append, list.mem_append, list.mem_singleton] at hl,
rcases hl with ⟨rfl | hl⟩ | rfl,
{ use fin.mk j hjn, use hj' },
{ apply hL2, assumption, },
{ use fin.mk j hjn, use hj' } } } },
{ symmetry' at hij,
rw swap_comm,
exact this hij }
end
variables (α : Type*) [decidable_eq α]
@[elab_as_eliminator] lemma zhangir2 [fintype α] {P : perm α → Prop} (f : perm α) :
P 1 → (∀ f x y, x ≠ y → P f → P (f * swap x y)) → P f :=
begin
intros h1 IH,
let Q : perm α → Prop := λ f, P (f⁻¹),
suffices hQ : ∀ f, Q f,
{ convert hQ f⁻¹,
simp,
},
intro f,
apply perm.swap_induction_on,
{ exact h1 },
intros f x y h hQ,
show P (((swap x y) * f)⁻¹),
rw [mul_inv_rev, swap_inv],
apply IH,
exact h,
exact hQ,
end
```

#### Yakov Pechersky (Aug 03 2020 at 22:38):

Relatedly, why is `equiv.swap_apply_of_ne_of_ne`

not a simp lemma?

#### Scott Morrison (Aug 03 2020 at 22:54):

src#equiv.swap_apply_of_ne_of_ne

#### Scott Morrison (Aug 03 2020 at 22:55):

(Just using the linkifier so I can see what it says.)

#### Scott Morrison (Aug 03 2020 at 22:55):

Presumably because it seems unlikely the side conditions will be discharged by `simp`

, so we wouldn't gain much.

#### Scott Morrison (Aug 03 2020 at 22:55):

`simp`

is not much good at proving inequalities.

#### Yakov Pechersky (Aug 03 2020 at 22:59):

Here's a short example where, if tagged `[simp]`

, it's useful. But it's not that much of a hassle to just invoke it.

```
variables {R : Type*} {m n : ℕ} [field R]
variables (A : matrix (fin (n + 2)) (fin (m + 2)) R)
def swap_row (i j) : matrix (fin (n + 2)) (fin (m + 2)) R :=
A ∘ equiv.swap i j
@[simp] lemma swap_row_def (i j) :
swap_row A i j = A ∘ equiv.swap i j := rfl
lemma swap_row_symmetric (i j) :
swap_row A i j = swap_row A j i :=
begin
ext ix jx,
by_cases hj : (ix = j);
by_cases hi : (ix = i);
simp [hj, hi, equiv.swap_apply_of_ne_of_ne]
end
```

#### Scott Morrison (Aug 03 2020 at 23:10):

I think a general rule of thumb is that if in order to make `simp`

use some particular lemma, you're going to need to jump through hoops providing additional facts to simp so it can apply, then it doesn't merit joining the standard `simp`

set. Maybe another way to say the same thing is that you shouldn't have to "know about" individual `simp`

lemmas to successfully use `simp`

.

Last updated: May 06 2021 at 21:09 UTC