## Stream: new members

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

#### 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


#### Mario Carneiro (Jul 02 2020 at 21:10):

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

#### Mario Carneiro (Jul 02 2020 at 21:10):

quot.lift is pretty much always better

#### Mario Carneiro (Jul 02 2020 at 21:11):

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

#### Mario Carneiro (Jul 02 2020 at 21:34):

Ah, never mind the quot.rec is necessary

#### Mario Carneiro (Jul 02 2020 at 21:34):

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

#### Yury G. Kudryashov (Jul 02 2020 at 21:41):

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

#### 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


#### 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

#### 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


#### 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.

#### Yury G. Kudryashov (Jul 02 2020 at 22:26):

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

#### 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


lol

#### Mario Carneiro (Jul 02 2020 at 22:40):

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

#### 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!)

#### Kyle Miller (Jul 02 2020 at 22:41):

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

#### 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 })


#### Mario Carneiro (Jul 02 2020 at 22:47):

You can do better: \lam _, rfl

#### 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