Transpositions of adjacent elements

Stream: new members

[Zhangir Azerbayev]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Oh sorry are there two swaps here?

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Reid Barton]

The only real problem is the {α : Type uu} part, right?

[Mario Carneiro]

no, the a and a_1 binders have the wrong type

[Mario Carneiro]

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

[Reid Barton]

oh neat

[Mario Carneiro]

Oh, the bug is in doc_gen

[Mario Carneiro]

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]

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]

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

[Kevin Buzzard]

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]

Relatedly, why is equiv.swap_apply_of_ne_of_ne not a simp lemma?

[Scott Morrison]

src#equiv.swap_apply_of_ne_of_ne

[Scott Morrison]

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

[Scott Morrison]

Presumably because it seems unlikely the side conditions will be discharged by simp, so we wouldn't gain much.

[Scott Morrison]

simp is not much good at proving inequalities.

[Yakov Pechersky]

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]

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.