Zulip Chat Archive

Stream: new members

Topic: Escaping fin hell (again)


view this post on Zulip Eric Wieser (Nov 27 2020 at 23:10):

I had a really hard time with this proof:

/-- Given a permutation of [0, n-1] , create a permutation of `[0, n]` that
    moves `n` into position `i` and leaves the rest untouched-/
def equiv.perm.snoc {n : } (e : equiv.perm (fin n)) (i : fin n.succ) :
  equiv.perm (fin n.succ) :=
{ to_fun := λ x, if h : x = fin.last n then i else fin.succ_above i (e ((fin.last n).pred_above x h)),
  inv_fun := λ x, if h : x = i then fin.last n else fin.succ_above (fin.last n) (e.symm $ i.pred_above x h),
  left_inv := λ x, by {
    by_cases hnl : fin.last n = x,
    { simp only,
      split_ifs with h1 h2 h3,
      { exact hnl, },
      { have h := h1,
        push_neg at h,
        rw [dif_pos hnl.symm] at h,
        exact false.elim (h rfl)},
      { have h := h1,
        push_neg at h,
        rw [dif_pos hnl.symm] at h,
        exact false.elim (h rfl)}, },
    { simp only,
      split_ifs with h1,
      { have h := h1,
        push_neg at h,
        rw [dif_neg (ne.symm hnl)] at h,
        exact false.elim (fin.succ_above_ne _ _ h), },
      { exact false.elim (hnl h.symm), },
      { simp, }, }, },
  right_inv := λ x, sorry }

The dites were very hard to simplify, and I had to close a lot of trivial contradictions I'd rather just vanished.

Am I missing a tactic here?

( I expect I can do right_inv, but I'd rather wait to see if there's a trick I missed!)

view this post on Zulip Yakov Pechersky (Nov 28 2020 at 23:49):

@Eric Wieser

import data.equiv.fin

/-- Given a permutation `e` of [0, n-1] , create a permutation of `[0, n]` that
    moves `n` into position `i`, and shifts `e x > i` up one. -/
def equiv.perm.snoc {n : } (e : equiv.perm (fin n)) (i : fin (n + 1)) :
  equiv.perm (fin (n + 1)) :=
{ to_fun := λ x, if h : x = fin.last n then i else fin.succ_above i (e ((fin.last n).pred_above x h)),
  inv_fun := λ x, if h : x = i then fin.last n else fin.succ_above (fin.last n) (e.symm $ i.pred_above x h),
  left_inv := λ x, by {
    rcases eq_or_lt_of_le x.le_last with rfl|hnl,
    { simp only [dif_pos] },
    { have : x  fin.last n := ne_of_lt hnl,
      simp only [this, fin.pred_above_succ_above, equiv.symm_apply_apply, dif_neg,
                 not_false_iff, fin.succ_above_pred_above, fin.succ_above_ne]} },
  right_inv := λ x, sorry }

view this post on Zulip Yakov Pechersky (Nov 28 2020 at 23:50):

I didn't touch your data defns, but there's probably a neater way of defining that.

view this post on Zulip Yakov Pechersky (Nov 29 2020 at 00:18):

import data.equiv.fin

@[simp] lemma fin.pred_last {n : } :
  fin.pred (fin.last (n + 1)) (ne_of_gt fin.last_pos) = fin.last n := rfl

lemma fin.pred_above_of_last {n : } {k : fin (n + 2)} (h : fin.last (n + 1)  k) :
  fin.pred_above k (fin.last (n + 1)) h = fin.last n :=
by rw [fin.pred_above, dif_neg (not_lt_of_le k.le_last), fin.pred_last]

lemma fin.pred_above_last {n : } {k : fin (n + 1)} (h : k < fin.last n) :
  fin.pred_above (fin.last n) k (ne_of_lt h) = k.cast_lt h :=
by { rw [fin.pred_above, dif_pos h], refl }

/-- Given a permutation `e` of [0, n-1] , create a permutation of `[0, n]` that
    moves `n` into position `i`, and shifts `e x > i` up one. -/
def equiv.perm.snoc {n : } (e : equiv.perm (fin n)) (i : fin (n + 1)) :
  equiv.perm (fin (n + 1)) :=
{ to_fun := λ x, if h : x = fin.last n then i else fin.succ_above i (e ((fin.last n).pred_above x h)),
  inv_fun := λ x, if h : x = i then fin.last n else fin.succ_above (fin.last n) (e.symm $ i.pred_above x h),
  left_inv := λ x, by {
    by_cases H : x = fin.last n,
    { simp only [H, dif_pos] },
    { simp only [H, fin.pred_above_succ_above, equiv.symm_apply_apply, dif_neg,
                 not_false_iff, fin.succ_above_pred_above, fin.succ_above_ne]} },
  right_inv := λ x, by {
    by_cases H : x = i,
    { simp only [H, dif_pos] },
    { -- this could be a lemma too, but I was advised against it
      have nel :  (k : fin n), k.cast_succ  fin.last n := λ k, ne_of_lt k.cast_succ_lt_last,
      simp only [H, nel, dif_neg, not_false_iff, fin.succ_above_last,
                 fin.pred_above_last (fin.cast_succ_lt_last _), fin.cast_lt_cast_succ,
                 equiv.apply_symm_apply, fin.succ_above_pred_above] } } }

view this post on Zulip Yakov Pechersky (Nov 29 2020 at 00:18):

Feel free to PR.

view this post on Zulip Yakov Pechersky (Nov 29 2020 at 00:20):

The crucial part for left_inv was knowing that fin.succ_above_ne is a lemma, but it's not a simp one because it provides an ne statement.

view this post on Zulip Eric Wieser (Nov 29 2020 at 08:16):

Thanks!

view this post on Zulip Eric Wieser (Nov 29 2020 at 08:17):

I've realized I should probably replace fin.last n with a generic j argument

view this post on Zulip Eric Wieser (Nov 29 2020 at 08:17):

And also that I no longer need this for the proof I was working on...

view this post on Zulip Yakov Pechersky (Nov 29 2020 at 08:58):

Do you still need the "split sum over univ into disjoint sets given involutive function etc"?

view this post on Zulip Eric Wieser (Nov 29 2020 at 09:43):

I found that exists already, mostly

view this post on Zulip Eric Wieser (Nov 29 2020 at 09:44):

It turns out that in asking for the Y in my XY problem, I found an X' that used Y in mathlib that was already most of the way towards the X I wanted

view this post on Zulip Eric Wieser (Nov 29 2020 at 16:00):

I think the possibly mathlib-suitable version is:

/-- Given a permutation of [0, n-1] , create a permutation of `[0, n]` that
    inserts `i` in the input and `j` in the output, and maps one to the other. -/
def equiv.perm.insert_fin {n : } (e : equiv.perm (fin n)) (i j : fin n.succ):
  equiv.perm (fin n.succ) :=
{ to_fun := λ x, if h : x = i then j else fin.succ_above j (e (i.pred_above x h)),
  inv_fun := λ x, if h : x = j then i else fin.succ_above i (e.symm $ j.pred_above x h),
  left_inv := λ x, if h : x = i then by simp [h] else by simp [h, fin.succ_above_ne],
  right_inv := λ x, if h : x = j then by simp [h] else by simp [h, fin.succ_above_ne] }

view this post on Zulip Eric Wieser (Nov 29 2020 at 16:22):

Or perhaps these:

/-- Given a permutation of [0, n-1] , create a permutation of `[0, n]` that
    leaves a hole around `i`. -/
def equiv.perm.fin_succ_above {n : } (e : equiv.perm (fin n)) (i : fin n.succ) :
  equiv.perm (fin n.succ) :=
{ to_fun := λ x, if h : x = i then i else fin.succ_above i (e $ i.pred_above x h),
  inv_fun := λ x, if h : x = i then i else fin.succ_above i (e.symm $ i.pred_above x h),
  left_inv := λ x, if h : x = i then by simp [h] else by simp [h, fin.succ_above_ne],
  right_inv := λ x, if h : x = i then by simp [h] else by simp [h, fin.succ_above_ne] }

/-- Given a permutation of `[0, n]` that leaves `i` unchanged, create a permutation of `[0, n - 1]` that
ignores `i`. -/
def equiv.perm.fin_pred_above {n : } (e : equiv.perm (fin n.succ)) (i : fin n.succ) (h : e i = i) :
  equiv.perm (fin n) :=
{ to_fun := λ x, i.pred_above (e $ i.succ_above x)
    (λ h', i.succ_above_ne x $ e.injective $ h'.trans h.symm),
  inv_fun := λ x, i.pred_above (e.symm $ i.succ_above x)
    (λ h', i.succ_above_ne x $ e.symm.injective $ h'.trans (e.apply_eq_iff_eq_symm_apply.mp h)),
  left_inv := λ x, by simp [h],
  right_inv := λ x, by simp [h] }

view this post on Zulip Mario Carneiro (Nov 29 2020 at 17:07):

hm, I would prefer to see this factored a bit to go via option (fin n)

view this post on Zulip Mario Carneiro (Nov 29 2020 at 17:08):

That is, there is an equiv fin (n+1) ~= option (fin n) that sends i to none and is otherwise monotone

view this post on Zulip Mario Carneiro (Nov 29 2020 at 17:09):

and then from an equiv option A ~= option B you can construct A ~= B (I think we have this already)

view this post on Zulip Eric Wieser (Nov 29 2020 at 17:31):

So something like

example {α β : Type*} : (α  β)  (option α  option β) := functor.map_equiv option

/-- An equivalence that leaves a hole around `i`, into which `none` is mapped -/
def equiv.option_equiv_fin_succ_above {n : } (i : fin n.succ) :
  option (fin n)  fin n.succ :=
{ to_fun := λ x, x.cases_on' i (fin.succ_above i),
  inv_fun := λ x, if h : x = i then none else some (i.pred_above x h),
  left_inv := λ x, by { cases x, simp, simp [fin.succ_above_ne], },
  right_inv := λ x, if h : x = i then by simp [h] else by simp [h, fin.succ_above_ne] }

-- the definition higher in the thread
example {n : } (e : equiv.perm (fin n)) (i : fin n.succ) : equiv.perm (fin n.succ) :=
(equiv.option_equiv_fin_succ_above i).perm_congr (functor.map_equiv option e)

view this post on Zulip Eric Wieser (Nov 29 2020 at 17:46):

What should that definition be called? fin.succ_above_option? Reverse it and use fin.pred_above_option?

view this post on Zulip Eric Wieser (Nov 29 2020 at 18:30):

Opened #5145 so that this doesn't get forgotten


Last updated: May 10 2021 at 17:39 UTC