Zulip Chat Archive

Stream: new members

Topic: using quotient.map2


Yakov Pechersky (Feb 10 2022 at 09:18):

In this example, why do I have to reprove the property of my function lifted into the quotient? I would have thought that map2_mk is able to retrieve it from the function itself. The lemma docs#quotient.map₂_mk is tagged @[simp] where it is defined.

import algebra.order.group
import algebra.order.with_zero

variables {S : Type*} [comm_semigroup S]

lemma cancel_left {a b c : S} (h : a * b = a * c) : b = c := sorry

variables (S)
-- we twist the multiplication to simplify refl and symm proofs
-- the definition is equivalent to `(a, a') ≈ (b, b') <-> a * b' = a' * b` due to the commutativity assumption
def mul_pair_setoid : setoid (S × S) :=
{ r := λ p q, p.1 * q.2 = q.1 * p.2,
  iseqv := begin
    refine λ _, rfl, λ _ _, eq.symm, _⟩,
    intros p q r h h',
    have := congr_arg ((*) p.snd) h',
    rw [mul_left_comm, mul_assoc, h, mul_comm _ q.snd, mul_comm _ q.snd, mul_left_comm,
        mul_assoc] at this,
    rw [cancel_left this, mul_comm],
  end }

variables {S}

local attribute [instance] mul_pair_setoid

@[simp] lemma mul_pair_equiv_iff (p q : S × S) : p  q  p.1 * q.2 = q.1 * p.2 := iff.rfl

lemma mul_pair_left_eq (p : S × S) (x : S) : (x * p.1, x * p.2) = p :=
by simp only [quotient.eq, mul_pair_equiv_iff, mul_assoc, mul_comm, mul_left_comm]

namespace mul_pair_quotient

local notation `G` := quotient (mul_pair_setoid S)

def mul : G  G  G :=
quotient.map₂ (λ (p q : S × S), (p.1 * q.1, p.2 * q.2)) begin
  rintro a, a' c, c' hac b, b' d, d' hbd,
  simp only [mul_pair_equiv_iff, quotient.eq] at hac hbd ,
  rw [mul_left_comm, mul_assoc, mul_assoc, mul_assoc, hbd, mul_comm c', hac],
  simp [mul_left_comm, mul_assoc, mul_comm]
end

instance : has_mul G := mul

-- why do I have to provide the proof again?
@[simp] lemma mk_mul :  (p q : S × S), p * q = (p.1 * q.1, p.2 * q.2) :=
quotient.map₂_mk _ begin
  rintro a, a' c, c' hac b, b' d, d' hbd,
  simp only [mul_pair_equiv_iff, quotient.eq] at hac hbd ,
  rw [mul_left_comm, mul_assoc, mul_assoc, mul_assoc, hbd, mul_comm c', hac],
  simp [mul_left_comm, mul_assoc, mul_comm]
end

end mul_pair_quotient

Eric Wieser (Feb 10 2022 at 09:34):

This works:

@[simp] lemma mk_mul :  (p q : S × S), p * q = (p.1 * q.1, p.2 * q.2) :=
begin
  change ( p q, mul p q = _),
  refine quotient.map₂_mk _ _,
end

Yakov Pechersky (Feb 10 2022 at 09:35):

All of those are "term-like" tactics, so why doesn't just the refine step work?

Eric Wieser (Feb 10 2022 at 09:37):

This also works:

@[simp] lemma mk_mul :  (p q : S × S), p * q = (p.1 * q.1, p.2 * q.2) :=
begin
  dunfold has_mul.mul,
  refine quotient.map₂_mk _ _,
end

Eric Wieser (Feb 10 2022 at 09:37):

The elaborator can't infer the implicit arguments correctly for you unless you unfold things in the right order for it, it seems

Yakov Pechersky (Feb 10 2022 at 09:38):

Thanks. This is helpful for the API I am building, but I still don't grok what's "wrong"

Eric Wieser (Feb 10 2022 at 09:38):

(as an aside, note that (λ (p q : S × S), (p.1 * q.1, p.2 * q.2)) is just (*))

Alex J. Best (Feb 10 2022 at 09:39):

And if you really want term mode:

@[simp] lemma mk_mul' :  (p q : S × S), p * q = (p.1 * q.1, p.2 * q.2) :=
assume p q,
show mul p q = _, from quotient.map₂_mk _ _ p q

Yakov Pechersky (Feb 10 2022 at 09:40):

Term mode or tactic mode, I don't understand why show _, from _ is necessary for the unification(?) to occur

Eric Wieser (Feb 10 2022 at 09:42):

My guess is that it unfolds things in the wrong order

Eric Wieser (Feb 10 2022 at 09:42):

Here's a version without show:

@[simp] lemma mk_mul :  (p q : S × S), p * q = (p.1 * q.1, p.2 * q.2) :=
(quotient.map₂_mk _ _ :  p q : S × S, mul p q = _)

Last updated: Dec 20 2023 at 11:08 UTC