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

Stream: new members

[Kyle Miller]

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]

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

[Mario Carneiro]

quot.lift is pretty much always better

[Mario Carneiro]

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

[Mario Carneiro]

Ah, never mind the quot.rec is necessary

[Mario Carneiro]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

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]

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]

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]

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]

See also src#equiv.subtype_quotient_equiv_quotient_subtype

[Yury G. Kudryashov]

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

[Kyle Miller]

@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

[Mario Carneiro]

lol

[Mario Carneiro]

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

[Kyle Miller]

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]

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

[Kyle Miller]

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]

You can do better: \lam _, rfl

[Kyle Miller]

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