Escaping fin hell (again)

Stream: new members

[Eric Wieser]

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!)

[Yakov Pechersky]

@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 }

[Yakov Pechersky]

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

[Yakov Pechersky]

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] } } }

[Yakov Pechersky]

Feel free to PR.

[Yakov Pechersky]

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.

[Eric Wieser]

Thanks!

[Eric Wieser]

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

[Eric Wieser]

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

[Yakov Pechersky]

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

[Eric Wieser]

I found that exists already, mostly

[Eric Wieser]

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

[Eric Wieser]

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] }

[Eric Wieser]

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] }

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Eric Wieser]

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)

[Eric Wieser]

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

[Eric Wieser]

Opened #5145 so that this doesn't get forgotten