## Stream: new members

### Topic: Escaping fin hell (again)

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


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

#### 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] } } }  #### Yakov Pechersky (Nov 29 2020 at 00:18): Feel free to PR. #### 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. #### Eric Wieser (Nov 29 2020 at 08:16): Thanks! #### Eric Wieser (Nov 29 2020 at 08:17): I've realized I should probably replace fin.last n with a generic j argument #### Eric Wieser (Nov 29 2020 at 08:17): And also that I no longer need this for the proof I was working on... #### Yakov Pechersky (Nov 29 2020 at 08:58): Do you still need the "split sum over univ into disjoint sets given involutive function etc"? #### Eric Wieser (Nov 29 2020 at 09:43): I found that exists already, mostly #### 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 #### 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] }


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


#### Mario Carneiro (Nov 29 2020 at 17:07):

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

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

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

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


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

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