Zulip Chat Archive

Stream: new members

Topic: Showing a function is well-defined (eq.rec)


view this post on Zulip Kyle Miller (Jul 02 2020 at 20:42):

I was trying to show there is a function from {s : multiset α // s.card = n} to the quotient of vector α n by permutations (actually, that there is an equivalence between these types), but I got stuck proving well-definedness due to not knowing how to deal with a eq.rec that appears. Perhaps I'm not defining to_fun correctly -- any suggestions or solutions would be appreciated.

The sorry is in to_fun below:

import data.quot
import data.equiv.basic
import data.vector
import data.set.function
import tactic

open function

def sym (α : Type*) (n : ) := {s : multiset α // s.card = n}

def vector.is_setoid (α : Type*) (n : ) : setoid (vector α n) :=
{ r := λ a b, list.perm a.1 b.1,
  iseqv := by { rcases list.perm.eqv α with hr, hs, ht, tidy, } }

def sym' (α : Type*) (n : ) := quotient (vector.is_setoid α n)

variables (α : Type*) (n : )

def to_fun (s : sym α n) : sym' α n :=
quot.rec (λ l h, quot.mk _ l, h) (begin
  intros a b p,
  ext h,
  have p' := list.perm.length_eq p,
  change b.length = n at h,
  sorry,
end) s.1 s.2

def inv_fun (s' : sym' α n) : sym α n :=
quot.rec (λ s, quot.mk _ s.1, s.2) (begin
  intros a b p,
  cases a, cases b,
  induction s',
  { cases s', induction a_property,
    simp only [eq_rec_constant, subtype.mk_eq_mk, multiset.coe_eq_coe, multiset.quot_mk_to_coe''],
    exact p, },
  refl,
end) s'

lemma left_inv : left_inverse (inv_fun α n) (to_fun α n) :=
by tidy

lemma right_inv : right_inverse (to_fun α n) (inv_fun α n) :=
by tidy

view this post on Zulip Mario Carneiro (Jul 02 2020 at 21:10):

don't use quot.rec if you can avoid it

view this post on Zulip Mario Carneiro (Jul 02 2020 at 21:10):

quot.lift is pretty much always better

view this post on Zulip Mario Carneiro (Jul 02 2020 at 21:11):

also, if it's an equivalence then use quotient instead of quot

view this post on Zulip Mario Carneiro (Jul 02 2020 at 21:34):

Ah, never mind the quot.rec is necessary

view this post on Zulip Mario Carneiro (Jul 02 2020 at 21:34):

See multiset.pmap for an example of how to do this

view this post on Zulip Yury G. Kudryashov (Jul 02 2020 at 21:41):

Do we have some general statement "quotient and subtype commute up to an equivalence"?

view this post on Zulip Mario Carneiro (Jul 02 2020 at 21:41):

def to_fun (s : sym α n) : sym' α n :=
quot.rec (λ l h, quot.mk _ l, h) (begin
  intros a b p,
  ext hb,
  have ha : a.length = n := (list.perm.length_eq p).trans hb,
  have :  {s e h}, @eq.rec (multiset α) a (λ s, s.card = n  sym' α n)
    (λ h, quotient.mk' a, ha) s e h = quotient.mk' a, ha,
  { intros s₂ e _; subst e },
  exact this.trans (quot.sound p),
end) s.1 s.2

view this post on Zulip Mario Carneiro (Jul 02 2020 at 21:43):

When defining a partial function on a quotient it is messy because you have to prove the predicate does not depend on the quotient relation. In both of these examples that's because the predicate depends on a quotient.lift. I don't know if that works in general

view this post on Zulip Mario Carneiro (Jul 02 2020 at 22:03):

def quot.plift {α r} {p : @quot α r  Prop} {β} (f :  a, p (quot.mk _ a)  β)
  (hf :  a b ha hb, r a b  f a ha = f b hb) (a) : p a  β :=
quot.rec f (begin
  intros a b h,
  ext hb,
  have ha : p (quot.mk _ a), {rwa quot.sound h},
  have :  {c e h}, @eq.rec (quot r) (quot.mk _ a) (λ s, p s  β)
    (λ h, f a ha) c e h = f a ha,
  { intros s₂ e _; subst e },
  refine this.trans (hf _ _ _ _ h),
end) a

def to_fun (s : sym α n) : sym' α n :=
@quot.plift _ _ (λ s : multiset α, s.card = n) _
  (λ l h, (quot.mk _ l, h : sym' α n))
  (λ a b ha hb p, quot.sound p) s.1 s.2

view this post on Zulip Kyle Miller (Jul 02 2020 at 22:08):

Thanks, and I appreciate that you answered the follow-up question I was just about to ask, which was whether you thought there could be a version of quot.lift that would let you easily use a property that respected the relation.

view this post on Zulip Yury G. Kudryashov (Jul 02 2020 at 22:25):

See also src#equiv.subtype_quotient_equiv_quotient_subtype

view this post on Zulip Yury G. Kudryashov (Jul 02 2020 at 22:26):

Probably we need a version with {}-implicit setoids.

view this post on Zulip Kyle Miller (Jul 02 2020 at 22:39):

@Yury G. Kudryashov Thanks, that's exactly what I needed.

Style-wise, is this sort of definition OK?

def sym_equiv_sym' (α : Type*) (n : ) : equiv (sym α n) (sym' α n) :=
begin
 apply equiv.subtype_quotient_equiv_quotient_subtype,
 tidy,
end

view this post on Zulip Mario Carneiro (Jul 02 2020 at 22:39):

lol

view this post on Zulip Mario Carneiro (Jul 02 2020 at 22:40):

it should be fine if those are just proofs, although you should tidy up tidy usage

view this post on Zulip Kyle Miller (Jul 02 2020 at 22:40):

Even though I knew it was about subtypes and quotients commuting, I didn't think to look for it :-/ (It's even well-named! thanks mathlib contributors!)

view this post on Zulip Kyle Miller (Jul 02 2020 at 22:41):

Yeah, they're just proofs. I can tidy? it, though.

view this post on Zulip Kyle Miller (Jul 02 2020 at 22:44):

It was worth it. Here's the one-liner:

def sym_equiv_sym' (α : Type*) (n : ) : equiv (sym α n) (sym' α n) :=
equiv.subtype_quotient_equiv_quotient_subtype _ _ (by {intro, refl}) (by { intros _ _, refl })

view this post on Zulip Mario Carneiro (Jul 02 2020 at 22:47):

You can do better: \lam _, rfl

view this post on Zulip Kyle Miller (Jul 02 2020 at 22:49):

Oh, except that refl is pulling in the refl of a particular relation, so there's at least (λ _, by refl).


Last updated: May 13 2021 at 20:13 UTC