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