Zulip Chat Archive

Stream: new members

Topic: Transpositions of adjacent elements


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 03 2020 at 13:44):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 03 2020 at 13:46):

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

view this post on Zulip Kevin Buzzard (Aug 03 2020 at 13:47):

Oh sorry are there two swaps here?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 03 2020 at 13:53):

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

view this post on Zulip Mario Carneiro (Aug 03 2020 at 14:10):

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

view this post on Zulip Reid Barton (Aug 03 2020 at 14:16):

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

view this post on Zulip Mario Carneiro (Aug 03 2020 at 14:23):

no, the a and a_1 binders have the wrong type

view this post on Zulip Mario Carneiro (Aug 03 2020 at 14:25):

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

view this post on Zulip Reid Barton (Aug 03 2020 at 14:26):

oh neat

view this post on Zulip Mario Carneiro (Aug 03 2020 at 14:36):

Oh, the bug is in doc_gen

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Aug 03 2020 at 22:38):

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

view this post on Zulip Scott Morrison (Aug 03 2020 at 22:54):

src#equiv.swap_apply_of_ne_of_ne

view this post on Zulip Scott Morrison (Aug 03 2020 at 22:55):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Aug 03 2020 at 22:55):

simp is not much good at proving inequalities.

view this post on Zulip 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

view this post on Zulip 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