## Stream: new members

### Topic: Sending perm $option α to perm α #### Eric Wieser (Jan 03 2021 at 11:13): I'm struggling a little with this definition, as I don'thave much experience with the API for option: import algebra.module import data.equiv.fin import control.equiv_functor import group_theory.perm.basic open equiv section variables {α : Type*} [decidable_eq α] [fintype α] (σ : perm$ option α )

def un_option_aux (x : α) : α :=
match _, rfl : ∀ (x' : option α), x' = σ (some x) → _ with
| some y, _ := y
| none, h := option.get $show (σ none).is_some, from sorry -- hand-wave: we know that none does not map from none, and σ is injective end /-- take a permutation σ : perm (option α), and produce a permutation σ' of α where some (σ' x) = if σ (some x) is none then σ none else σ (some x) or some (σ' x) = σ none -/ def un_option : perm α := { to_fun := un_option_aux σ, inv_fun := un_option_aux σ⁻¹, left_inv := λ x, by sorry, -- awful _match expressions right_inv := λ x, by sorry, } end  #### Yakov Pechersky (Jan 03 2021 at 11:19): How do you know that \si fixes none?? #### Eric Wieser (Jan 03 2021 at 11:20): Either it does fix none, in which case the mapping is obvious, or it doesn't fix none, in which case σ (some x).is_none implies (σ none).is_some - that's what I mean by the "or" in my docstring #### Eric Wieser (Jan 03 2021 at 11:26): Perhaps a clearer statement avoiding match: def un_option_aux' (x : α) : α := if h : (σ (some x)).is_some then option.get h else option.get$ show (σ none).is_some, from
begin
rw option.is_some_iff_exists,
rw option.not_is_some_iff_eq_none at h,
sorry,
end


#### Yakov Pechersky (Jan 03 2021 at 11:36):

I have this so far:

@[simp] def option.pbind_with {α β : Type*} :
Π (x : option α), (x = none → option β) → (Π (a : α), a ∈ x → option β) → option β
| none     g _ := g rfl
| (some a) _ f := f a rfl

def un_option_aux (x : α) : option α :=
(σ (some x)).pbind_with (λ _, σ none) (λ _ _, σ (some x))


#### Yakov Pechersky (Jan 03 2021 at 11:36):

The hypotheses aren't needed, I just had this pbind_with lying around

#### Eric Wieser (Jan 03 2021 at 11:36):

That looks a lot tidier thatn what I have:

def un_option_aux' (x : α) : α :=
if h : (σ (some x)).is_some
then option.get h
else option.get $show (σ none).is_some, from begin rw option.not_is_some_iff_eq_none at h, rw ←option.ne_none_iff_is_some, intro hn, rw ←hn at h, simpa using σ.injective h, end  #### Yakov Pechersky (Jan 03 2021 at 11:41): @[simp] def option.pbind_with {α β : Type*} : Π (x : option α), (x = none → option β) → (Π (a : α), a ∈ x → option β) → option β | none g _ := g rfl | (some a) _ f := f a rfl @[simp] lemma option.pbind_with_eq_some_of_const_some {α : Type*} (x : option α) (y : option α) (a : α) : option.pbind_with x (λ _, y) (λ _ _, x) = some a ↔ x = some a ∨ (y = some a ∧ x = none) := by cases x; simp def un_option_aux (x : α) : option α := (σ (some x)).pbind_with (λ _, σ none) (λ _ _, σ (some x)) lemma un_option_aux_eq_some (x : α) : ∃ y, un_option_aux σ x = some y := begin simp [un_option_aux], end  #### Eric Wieser (Jan 03 2021 at 11:41): That's not going to be constructive though #### Eric Wieser (Jan 03 2021 at 11:42): Oh, maybe it is since you can pass that to option.get #### Yakov Pechersky (Jan 03 2021 at 11:43): exactly #### Yakov Pechersky (Jan 03 2021 at 11:43): I'm just giving you a lemma that proves that you always get something some out of un_option_aux #### Eric Wieser (Jan 03 2021 at 11:44): My definition above seems to work, but proving left_inv is awful #### Yakov Pechersky (Jan 03 2021 at 11:48): @[simp] def option.pbind_with {α β : Type*} : Π (x : option α), (x = none → option β) → (Π (a : α), a ∈ x → option β) → option β | none g _ := g rfl | (some a) _ f := f a rfl @[simp] lemma option.pbind_with_eq_some_of_const_some {α : Type*} (x : option α) (y : option α) (a : α) : option.pbind_with x (λ _, y) (λ _ _, x) = some a ↔ x = some a ∨ (y = some a ∧ x = none) := by cases x; simp def un_option_aux (x : α) : option α := (σ (some x)).pbind_with (λ _, σ none) (λ _ _, σ (some x)) lemma un_option_aux_eq_some (x : α) : ∃ y, un_option_aux σ x = some y := begin cases hs : σ (some x) with z; cases hs' : σ none with w, { rw ←hs' at hs, simpa using hs }, { use w, simpa [un_option_aux, hs'] using or.inr hs }, { use z, simpa [un_option_aux, hs'] using hs, }, { use z, simpa [un_option_aux, hs'] using or.inl hs } end  #### Eric Wieser (Jan 03 2021 at 12:03): Alright, I have a proof of the equiv now too: import algebra.module import data.equiv.fin import control.equiv_functor import group_theory.perm.basic open equiv section variables {α : Type*} [decidable_eq α] [fintype α] (σ : perm$ option α )

def un_option_aux (x : α) : α :=
if h : (σ (some x)).is_some
then option.get h
else option.get $show (σ none).is_some, from begin rw option.not_is_some_iff_eq_none at h, rw ←option.ne_none_iff_is_some, intro hn, rw ←hn at h, simpa using σ.injective h, end lemma un_option_aux_inv (x : α) : un_option_aux σ⁻¹ (un_option_aux σ x) = x := begin dsimp only [un_option_aux], by_cases h : ∀ x, (σ (some x)).is_some, { simp [h] }, rw not_forall at h, obtain ⟨nx, h⟩ := h, by_cases hx : x = nx, { subst hx, simp [h], rw [option.not_is_some_iff_eq_none, ←perm.eq_inv_iff_eq] at h, simp [←h], }, rw option.not_is_some_iff_eq_none at h, have : ↥(σ (some x)).is_some, { rw ←option.ne_none_iff_is_some, intro hn, rw ←hn at h, exact hx (option.some_injective _ (σ.injective h)).symm }, simp [this], end end  Now just a case of golfing it (and deciding whether a case-matching approach makes more sense than if #### Yakov Pechersky (Jan 03 2021 at 12:19): open equiv section variables {α : Type*} [decidable_eq α] [fintype α] (σ : perm$ option α )

@[simp] def option.pbind_with {α β : Type*} :
Π (x : option α), (x = none → option β) → (Π (a : α), a ∈ x → option β) → option β
| none     g _ := g rfl
| (some a) _ f := f a rfl

@[simp] lemma option.pbind_with_eq_some_of_const_some {α : Type*}
(x : option α) (y : option α) (a : α) :
option.pbind_with x (λ _, y) (λ _ _, x) = some a ↔ x = some a ∨ (y = some a ∧ x = none) :=
by cases x; simp

def un_option_aux (x : α) : option α :=
(σ (some x)).pbind_with (λ _, σ none) (λ _ _, σ (some x))

lemma un_option_aux_eq_some (x : α) : ∃ y, un_option_aux σ x = some y :=
begin
cases hs : σ (some x) with z;
cases hs' : σ none with w,
{ rw ←hs' at hs,
simpa using hs },
{ use w,
simpa [un_option_aux, hs'] using or.inr hs },
{ use z,
simpa [un_option_aux, hs'] using hs, },
{ use z,
simpa [un_option_aux, hs'] using or.inl hs }
end

lemma un_option_aux_is_some (x : α) : (un_option_aux σ x).is_some :=
option.is_some_iff_exists.mpr (un_option_aux_eq_some σ x)

def un_option' (x : α) : α :=
option.get (un_option_aux_is_some σ x)

lemma un_option'_iff (x y : α) :
un_option' σ x = y ↔ un_option_aux σ x = some y :=
begin
split,
{ rintro rfl,
simp [un_option'] },
{ intro h,
rw [un_option', ←option.some_inj, option.some_get, h] },
end

def un_option : perm α :=
{ to_fun := un_option' σ,
inv_fun := un_option' σ.symm,
left_inv := λ x, by {
obtain ⟨z, hz⟩ := un_option_aux_eq_some σ x,
simp [(un_option'_iff _ _ _).mpr hz, un_option'_iff, un_option_aux],
simp [un_option_aux] at hz,
rcases hz with hz | ⟨hz, hz'⟩,
{ simp [←hz] },
{ simp [←hz, ←hz'] } },
right_inv := λ x, by {
obtain ⟨z, hz⟩ := un_option_aux_eq_some σ.symm x,
simp [(un_option'_iff _ _ _).mpr hz, un_option'_iff, un_option_aux],
simp [un_option_aux] at hz,
rcases hz with hz | ⟨hz, hz'⟩,
{ simp [←hz] },
{ simp [←hz, ←hz'] } },
}


#### Yakov Pechersky (Jan 03 2021 at 12:20):

some non-terminal simps, but they can prolly get golfed easily

#### Yakov Pechersky (Jan 03 2021 at 12:20):

My strategy here is to get away as soon as possible from juggling is_some predicates

#### Eric Wieser (Jan 03 2021 at 12:32):

Yeah, the pile of different ways to express is_some makes this very painful

#### Eric Wieser (Jan 03 2021 at 12:32):

Is there any precedent for the pbind_with name?

#### Yakov Pechersky (Jan 03 2021 at 12:34):

I have a pbind defined in #5442, I didn't PR the more general pbind_with

#### Yakov Pechersky (Jan 03 2021 at 12:35):

There's a general issue of whether all functors/monads should have auto-generated pmap for their map and pbind for their bind. That's why I've held off with the pbind_with. But your case isn't the first time I've come across having to deal with "meaningful" nones, I've had the same.

#### Eric Wieser (Jan 03 2021 at 12:49):

Edited my version above, was able to get rid of most of the is_some mess

#### Eric Wieser (Jan 03 2021 at 14:55):

Cleaned up in #5593. I'll leave that WIP until I get the correspondance to fin n.succ in there

#### Floris van Doorn (Jan 03 2021 at 23:11):

This is a notoriously tricky proof. I'm surprised we don't have it in mathlib yet (I expected we would have the injectivity of (λ x, x + 1 : cardinal → cardinal), which would use/give remove_none)

#### Eric Wieser (Jan 03 2021 at 23:18):

I take it then that you also couldn't find this in mathlib? Is equiv.remove_none a reasonable name in your opinion?

#### Eric Wieser (Jan 03 2021 at 23:21):

I guess elim / skip / ignore / tie / coalesce might all be alternatives for remove in the name

#### Floris van Doorn (Jan 03 2021 at 23:33):

I'm quite sure it's not in mathlib, indeed.
I don't think there is a "good" name, so I think this one is fine. Other possibilities are equiv.cancel_none or equiv.option_inj[ective] or something.

How hard would it be to go from your formulation to α ≃ β → { x : α // x ≠ x₀ } ≃ { y : β // y ≠ y₀ } (assuming something like decidable_eq or decidable_pred (= x₀) if you want to do it constructively).
I don't know if you will also want that version at some point (it might be easier to go from the version I suggest to the version you have for option, using something like docs#equiv.option_is_some_equiv).

#### Floris van Doorn (Jan 03 2021 at 23:34):

If we make a file equiv/option, should we move the appropriate results from equiv/basic into that file?

#### Yakov Pechersky (Jan 04 2021 at 06:17):

We can, do you want to do this in this PR or separate?

#### Yakov Pechersky (Jan 04 2021 at 06:18):

Relatedly, should the simp-normal form for equiv.refl α : perm α be equiv.refl α or 1?

Last updated: May 14 2021 at 22:15 UTC