failed to synthesize HMul

Stream: new members

[Moritz R]

i reduced my problem to the following (mathematical nonsense) #mwe:
I don't get why i cant use the multiplication symbol in Q.mul_def1 and why typeclass inference fails in Q.mul_def2

import Mathlib

opaque A : Type

--trivial Quotient: ≈ is =
instance A.Setoid : Setoid A :=
  {
    r := fun a b : A => a = b
    iseqv :=
      {
        refl := by aesop
        symm := by aesop
        trans := by aesop
      }
  }

theorem A.Setoid_Iff (a b : A) : a ≈ b ↔ a = b := by rfl

instance A.Mul : Mul A :=
  {
    mul := fun (a _ : A) => a
  }

instance Q : Type := Quotient A.Setoid

instance Q.Mul : Mul Q :=
  {
    mul := fun (a _ : Q) => a
  }

def Q.rfl_theorem {a : A}: (Quotient.mk A.Setoid a) = (Quotient.mk A.Setoid a) := rfl --works

theorem Q.mul_def1 {a b : A}: (Quotient.mk A.Setoid a) * (Quotient.mk A.Setoid b) = (Quotient.mk A.Setoid a) := sorry --failed to synthesize HMul, why?

theorem Q.mul_def2 {a b : A} : ⟦a⟧ * ⟦b⟧ = ⟦a⟧ := sorry --typeclass instance problem is stuck

theorem Q.mul_def3 {a b : Q} : a * b = a := rfl --works

instance Q.Semigroup : Semigroup Q :=
  {
    mul_assoc := by
      intro a b c
      induction a using Quotient.ind with
      | _ a =>
        induction b using Quotient.ind with
        | _ b =>
          induction c using Quotient.ind with
          | _ c => simp [Q.mul_def2]

  }

[Kenny Lau]

your declaration labels are kind of messy (Q is def not instance, and Q.rfl_theorem is theorem not def)

[Kenny Lau]

and the answer to your question is that Lean sees Quotient.mk A.Setoid a and has no way to figure out that you meant to make an element of Q

[Kenny Lau]

when you define Q : Type := Quotient A.Setoid, Lean will automatically unfold Q to Quotient A.Setoid, but never the other way round!

[Kenny Lau]

you can solve this by defining a special constructor from A to Q

[Kenny Lau]

import Mathlib

opaque A : Type

--trivial Quotient: ≈ is =
instance A.Setoid : Setoid A where
  r a b := a = b
  iseqv :=
  { refl _ := rfl
    symm := Eq.symm
    trans := Eq.trans }

theorem A.Setoid_Iff (a b : A) : a ≈ b ↔ a = b := by rfl

instance A.Mul : Mul A where
  mul a _ := a

def Q : Type := Quotient A.Setoid

instance Q.Mul : Mul Q where
  mul a _ := a

def Q.ofA (a : A) : Q := Quotient.mk A.Setoid a

@[elab_as_elim] def Q.ofA_induction {motive : Q → Sort*} (ofA : ∀ a, motive (Q.ofA a)) (q : Q) :
    motive q :=
  Quotient.rec ofA (fun _ _ r ↦ Eq.recOn r rfl) q

theorem Q.mul_def {a b : A} : Q.ofA a * Q.ofA b = Q.ofA a := rfl

instance Q.Semigroup : Semigroup Q where
  mul_assoc a b c := by
    induction a using Q.ofA_induction
    induction b using Q.ofA_induction
    induction c using Q.ofA_induction
    rfl

[Aaron Liu]

Kenny Lau said:

when you define Q : Type := Quotient A.Setoid, Lean will automatically unfold Q to Quotient A.Setoid, but never the other way round!

Since it's a def and not an abbrev, it's also only unfolded sometimes (and typeclass is not one of those times), I think if you make it an abbrev then instances on Q will apply to its unfolding

[Moritz R]

How can i get this to work? Aren't there any theorems stated with this notation in mathlib?

theorem Q.mul_def2 {a b : A} : ⟦a⟧ * ⟦b⟧ = ⟦a⟧ := sorry

[Kenny Lau]

@Moritz R no, every time you define a special quotient in mathlib, you'll see that there are immediately special constructors

[Kenny Lau]

you can also of course define special notations

[Moritz R]

so the bracket notation is only for the output, not for the input?

[Kenny Lau]

import Mathlib

opaque A : Type

--trivial Quotient: ≈ is =
instance A.Setoid : Setoid A where
  r a b := a = b
  iseqv :=
  { refl _ := rfl
    symm := Eq.symm
    trans := Eq.trans }

theorem A.Setoid_Iff (a b : A) : a ≈ b ↔ a = b := by rfl

instance A.Mul : Mul A where
  mul a _ := a

def Q : Type := Quotient A.Setoid

instance Q.Mul : Mul Q where
  mul a _ := a

def Q.ofA (a : A) : Q := Quotient.mk A.Setoid a

@[elab_as_elim] def Q.ofA_induction {motive : Q → Sort*} (ofA : ∀ a, motive (Q.ofA a)) (q : Q) :
    motive q :=
  Quotient.rec ofA (fun _ _ r ↦ Eq.recOn r rfl) q

theorem Q.mul_def {a b : A} : Q.ofA a * Q.ofA b = Q.ofA a := rfl

notation "⟦" a:arg "⟧Q" => Q.ofA a

theorem Q.mul_def2 {a b : A} : ⟦a⟧Q * ⟦b⟧Q = ⟦a⟧Q := sorry

instance Q.Semigroup : Semigroup Q where
  mul_assoc a b c := by
    induction a using Q.ofA_induction
    induction b using Q.ofA_induction
    induction c using Q.ofA_induction
    rfl

[Kenny Lau]

@Moritz R actually the bracket notation works if you make Q an abbrev

[Kenny Lau]

import Mathlib

opaque A : Type

--trivial Quotient: ≈ is =
instance A.Setoid : Setoid A where
  r a b := a = b
  iseqv :=
  { refl _ := rfl
    symm := Eq.symm
    trans := Eq.trans }

theorem A.Setoid_Iff (a b : A) : a ≈ b ↔ a = b := by rfl

instance A.Mul : Mul A where
  mul a _ := a

abbrev Q : Type := Quotient A.Setoid

instance Q.Mul : Mul Q where
  mul a _ := a

theorem Q.mul_def2 {a b : A} : (⟦a⟧ * ⟦b⟧ : Q) = ⟦a⟧ := sorry

instance Q.Semigroup : Semigroup Q where
  mul_assoc a b c := by
    induction a using Quotient.inductionOn
    induction b using Quotient.inductionOn
    induction c using Quotient.inductionOn
    rw [Q.mul_def2, Q.mul_def2, Q.mul_def2, Q.mul_def2]

[Moritz R]

yes, but i probably don't want to use an abbrev

[Kenny Lau]

yes, so you'll need a custom constructor

[Kenny Lau]

I also don't advise using abbrev

[Moritz R]

so do people in mathlib not care about the brackets in the input, since they will hopefully not have to look at representatives too much?

[Kenny Lau]

I don't know why you keep asking the same question. You can use a custom constructor from A to Q.

[Moritz R]

or are they defining notation for every Quotient they do

[Kenny Lau]

That will be representatives

[Kenny Lau]

yes, you should always define special constructors

[Kenny Lau]

this is part of the API that goes with every new definition

[Moritz R]

Moritz R schrieb:

or are they defining notation for every Quotient they do

is defining the bracket notation with the custom constructor done for every quotient in mathlib?

[Moritz R]

(not asking if its possible, but if its typical)

[Kenny Lau]

every quotient that is not an abbrev, yes. but they don't necessarily use the bracket notation

[Kenny Lau]

for example, Multiset is a quotient of List, and they defined special constructors for Multiset instead of just taking representative

[Kenny Lau]

import Mathlib.Data.Multiset.Basic

#check (37 ::ₘ 3 ::ₘ 0 : Multiset ℕ)

[Kenny Lau]

@Moritz R so you'll see that Multiset is defined to be Quotient (List.isSetoid α), and right below it is the special constructor Multiset.ofList.

[Kenny Lau]

this is all part of the multiset API.

[Moritz R]

In this version with a special constructor, why does my simp at the end fail? And what does it probably have to do with your ofA_induction:

import Mathlib

opaque A : Type

--trivial Quotient: ≈ is =
instance A.Setoid : Setoid A :=
  {
    r := fun a b : A => a = b
    iseqv :=
      {
        refl := by aesop
        symm := by aesop
        trans := by aesop
      }
  }

theorem A.Setoid_Iff (a b : A) : a ≈ b ↔ a = b := by rfl

instance A.Mul : Mul A :=
  {
    mul := fun (a _ : A) => a
  }

instance Q : Type := Quotient A.Setoid

instance Q.Mul : Mul Q :=
  {
    mul := fun (a _ : Q) => a
  }

def Q.mk (a : A) : Q := Quotient.mk A.Setoid a

def Q.rfl_theorem {a : A}: (Quotient.mk A.Setoid a) = (Quotient.mk A.Setoid a) := rfl --works

theorem Q.mul_def1 {a b : A}: (Q.mk a) * (Q.mk b) = (Q.mk a) := by rfl

instance Q.Semigroup : Semigroup Q :=
  {
    mul_assoc := by
      intro a b c
      induction a using Quotient.ind with
      | _ a =>
        induction b using Quotient.ind with
        | _ b =>
          induction c using Quotient.ind with
          | _ c => simp [Q.mul_def1]

  }

[Aaron Liu]

You need a custom induction that uses the custom constructor

[Kenny Lau]

@Moritz R because you copied the part of my code with the constructor and forgot to copy the part of my code with the special induction too

[Kenny Lau]

did you read my codes?

[Moritz R]

i didn't forget your special induction, but i had no idea how you came up with it, and why so i left it out.
I think now, it is because in the output i have Elements of type Quotient A.Setoid, but my simp theorem is using elements of type Q and simp doesn't unfold the Q definition when trying to apply the lemma?

[Kenny Lau]

@Moritz R the special induction is part of the API. you basically rephrase induction, but using your custom constructor instead

[Kenny Lau]

because if you just use the built in induction, then you get Quotient.mk a, which Lean cannot unfold to become Q.ofA a

[Moritz R]

Thanks, i think i understand now!

[Kenny Lau]

you basically need to think in terms of unfolding

[Kenny Lau]

def X := Y means X unfolds to Y, and never the other way round

[Moritz R]

But what is part of the "standard mathlib api" wasn't really clear for me, im still a beginner

[Kenny Lau]

the API is the set of auxiliary definitions and theorems you need, to properly use the new definition

[Kenny Lau]

in other words, just having a mathematically correct definition is not enough, you need to be able to use it

[Kenny Lau]

if i construct a mathematically correct square root function sqrt on the reals, but do not prove that sqrt (x * x) = x, then this sqrt function is useless

[Moritz R]

in the long term we should automate this process for Quotients, no? It seems automatic enough here

[Kenny Lau]

it's good practice to build API yourself, because most likely you won't have a quotient by equality.

[Moritz R]

But building a custom constructor and rephrasing the induction principle don't depend at all on how the equivalence relation is defined? This is what i meant we could automate away

[Kenny Lau]

well you might want to give it a custom name

[Kenny Lau]

and sometimes the custom constructor actually you want it to be a ring hom

[Moritz R]

Kenny Lau schrieb:

and sometimes the custom constructor actually you want it to be a ring hom

instead of a fun?

[Aaron Liu]

Moritz R said:

in the long term we should automate this process for Quotients, no? It seems automatic enough here

We need a redesign of Quotients

[Kenny Lau]

I disagree