using quotient.map2

Stream: new members

[Yakov Pechersky]

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]

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]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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

[Alex J. Best]

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]

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

[Eric Wieser]

My guess is that it unfolds things in the wrong order

[Eric Wieser]

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⟧ = _)