Zulip Chat Archive

Stream: new members

Topic: Sending `perm $ option α` to `perm α`


view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jan 03 2021 at 11:19):

How do you know that \si fixes none??

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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))

view this post on Zulip Yakov Pechersky (Jan 03 2021 at 11:36):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 03 2021 at 11:41):

That's not going to be constructive though

view this post on Zulip Eric Wieser (Jan 03 2021 at 11:42):

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

view this post on Zulip Yakov Pechersky (Jan 03 2021 at 11:43):

exactly

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 03 2021 at 11:44):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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'] } },
  }

view this post on Zulip Yakov Pechersky (Jan 03 2021 at 12:20):

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

view this post on Zulip Yakov Pechersky (Jan 03 2021 at 12:20):

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

view this post on Zulip Eric Wieser (Jan 03 2021 at 12:32):

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

view this post on Zulip Eric Wieser (Jan 03 2021 at 12:32):

Is there any precedent for the pbind_with name?

view this post on Zulip Yakov Pechersky (Jan 03 2021 at 12:34):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Jan 03 2021 at 12:49):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Jan 03 2021 at 23:21):

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

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Jan 04 2021 at 06:17):

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

view this post on Zulip 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