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

1. 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
2. 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

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