Sending `perm $ option α` to `perm α`

Stream: new members

[Eric Wieser]

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]

How do you know that \si fixes none??

[Eric Wieser]

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]

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]

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]

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

[Eric Wieser]

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]

@[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]

That's not going to be constructive though

[Eric Wieser]

Oh, maybe it is since you can pass that to option.get

[Yakov Pechersky]

exactly

[Yakov Pechersky]

I'm just giving you a lemma that proves that you always get something some out of un_option_aux

[Eric Wieser]

My definition above seems to work, but proving left_inv is awful

[Yakov Pechersky]

@[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]

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]

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]

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

[Yakov Pechersky]

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

[Eric Wieser]

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

[Eric Wieser]

Is there any precedent for the pbind_with name?

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

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

[Eric Wieser]

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

[Floris van Doorn]

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]

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]

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

[Floris van Doorn]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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