# Zulip Chat Archive

## 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" `none`

s, 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