Maximum Class-Instance Resolution Depth Reached

Stream: general

[Ken Lee]

This appeared when I tried to use quotient.mk. What does this mean and how can I fix this?

[Scott Morrison]

Sometimes it just means you need to increase the bound. Other times it means that something has gone haywire, and instances have been defined that cause the class resolution mechanism (which isn't very clever) to enter a loop.

[Johan Commelin]

@Ken Lee In what context where you using quotients?

[Scott Morrison]

Try set_option class.instance_max_depth 50.

[Johan Commelin]

A bunch of algebra? Or a simple equivalence relation?

[Ken Lee]

I was trying to define orbits under a group action.

[Ken Lee]

Try set_option class.instance_max_depth 50.

This hasn't worked

[Johan Commelin]

Try 100

[Johan Commelin]

If that fails, it means something else is wrong.

[Johan Commelin]

Also... orbits are already in mathlib. (Of course that doesn't forbid you from defining your own. But just so you know.)

[Ken Lee]

Try 100

I tried 500. It still doesn't work.

[Johan Commelin]

Ok, then we need more context to figure out what went wrong.

[Chris Hughes]

Did you make thesetoid an instance?

[Ken Lee]

Also... orbits are already in mathlib. (Of course that doesn't forbid you from defining your own. But just so you know.)

I know haha was just seeing if I can define it in Lean

[Ken Lee]

Did you make thesetoid an instance?

Yes @Chris Hughes

[Ken Lee]

Ok, then we need more context to figure out what went wrong.

Should I post the entire code? I haven't written much

[Chris Hughes]

Yes. It might be that the instance depends on an argument that can't be inferred by type class resolution.

[Ken Lee]

import algebra.group

universes u0 u1 u2

open function

#print setoid
#print congr
theorem congr_alt {X : Type u0} {Y : Type u1} {f₁ f₂ : X → Y} {x₁ x₂ : X} :
x₁ = x₂ → f₁ = f₂ → f₁ x₁ = f₂ x₂ := λ x1_eq_x2 f1_eq_f2, congr f1_eq_f2 x1_eq_x2

structure action (G : Type u0) [group G] (X : Type u1) :=
(action : G → (X → X))
(map_one : action 1 = id)
(map_mul : ∀ f g : G, action (f * g) = action f ∘ action g)

infix ` action `:1000 := action

instance action.setoid {G : Type u0} [group G] {X : Type u1} (GX : G action X)
: setoid X := {
  r := λ x y : X, ∃ g : G, GX.action g x = y,
  iseqv := ⟨
    -- Refl
    λ x : X, ⟨1, GX.map_one.symm ▸ rfl⟩,
    -- Symm
    λ (x y : X) ⟨g,gx_eq_y⟩, ⟨g⁻¹,
      calc GX.action g⁻¹ y
            = GX.action g⁻¹ (GX.action g x) : gx_eq_y.symm ▸ rfl
      ... = (GX.action g⁻¹ ∘ GX.action g) x : rfl
      ... = GX.action (g⁻¹ * g) x : congr_alt rfl $ (GX.map_mul _ _).symm
      ... = GX.action 1 x : congr_alt rfl $ inv_mul_self g ▸ rfl
      ... = x : GX.map_one.symm ▸ rfl
      ⟩
    ,
    -- Trans
    λ (x y z : X) ⟨g,gx_eq_y⟩ ⟨h, hy_eq_z⟩, ⟨h * g,
            calc GX.action (h * g) x
                    = (GX.action h ∘ GX.action g) x : congr_alt rfl $ GX.map_mul _ _
            ... = GX.action h y : gx_eq_y ▸ rfl
            ... = z : hy_eq_z
        ⟩
  ⟩,
}

def orbits {G : Type u0} [group G] {X: Type u1} (GX : G action X) :=
quotient (action.setoid GX)

set_option class.instance_max_depth 100

def orbit {G : Type u0} [group G] {X: Type u1} (GX : G action X) (x : X)
: orbits GX := ⟦x⟧

[Ken Lee]

Yes. It might be that the instance depends on an argument that can't be inferred by type class resolution.

May I ask, what is type class resolution?

[Kenny Lau]

def orbit {G : Type u0} [group G] {X: Type u1} (GX : G action X) (x : X)
: orbits GX :=
quotient.mk' x

works fine

[Chris Hughes]

It's the process that fill in the arguments in square brackets.

[Kenny Lau]

oh don't forget to import data.quot

[Chris Hughes]

So the problem was that type class inference didn't know which group action you meant. This information can however be inferred from the expected type (which type class resolution doesn't use). quotient.mk' puts the setoid argument in {} brackets instead of [] brackets, so it uses a different procedure to infer the argument, which does use the expected type.

[Kenny Lau]

btw have you looked at the file group_theory.group_action?

[Kenny Lau]

(deleted)

[Ken Lee]

So the problem was that type class inference didn't know which group action you meant. This information can however be inferred from the expected type (which type class resolution doesn't use). quotient.mk' puts the setoid argument in {} brackets instead of [] brackets, so it uses a different procedure to infer the argument, which does use the expected type.

Aha thanks for the explanation

[Ken Lee]

btw have you looked at the file group_theory.group_action?

No i have not. Why do you ask? @Kenny Lau

[Kenny Lau]

because group action is already defined there

[Ken Lee]

because group action is already defined there

Yes I know. But I wanted to exercise my Lean skills!

[Kenny Lau]

ok so a difference is that in the official file, the group action is a class

[Kenny Lau]

while you made it a structure

[Ken Lee]

I forget the difference between the two. Should I have defined it as a class instead? (if so, why?)

[Kenny Lau]

I put your file in a washing machine

[Kenny Lau]

import algebra.group

universes u0 u1 u2

class has_scalar (G : Type u0) (X : Type u1) :=
(smul : G → X → X)

infixr ` • `:73 := has_scalar.smul

class action (G : Type u0) [group G] (X : Type u1) extends has_scalar G X :=
(one_smul : ∀ x : X, (1 : G) • x = x)
(mul_smul : ∀ f g : G, ∀ x : X, (f * g) • x = f • (g • x))
export action (one_smul mul_smul)

infix ` action `:1000 := action

instance action.setoid (G : Type u0) [group G] (X : Type u1) [G action X] : setoid X :=
{ r := λ x y : X, ∃ g : G, g • x = y,
  iseqv := ⟨
    -- Refl
    λ x : X, ⟨1, by rw one_smul⟩,
    -- Symm
    λ (x y : X) ⟨g, gx_eq_y⟩, ⟨g⁻¹, by rw [← gx_eq_y, ← mul_smul, inv_mul_self, one_smul]⟩,
    -- Trans
    λ (x y z : X) ⟨g,gx_eq_y⟩ ⟨h, hy_eq_z⟩, ⟨h * g, by rw [mul_smul, gx_eq_y, hy_eq_z]⟩⟩ }

def orbits (G : Type u0) [group G] (X: Type u1) [G action X] :=
quotient (action.setoid G X)

def orbit (G : Type u0) [group G] (X: Type u1) [G action X] (x : X) : orbits G X :=
⟦x⟧

[Kenny Lau]

@Chris Hughes should it be a class or a structure?

[Kenny Lau]

@Ken Lee was there a particular reason why you avoided rw?

[Ken Lee]

Ah this is nice, so we can write g(x) = y effectively.

[Chris Hughes]

But this is bad if you want a group to act on a set in lots of different ways.

[Kenny Lau]

yeah but then why does the official file use class?

[Chris Hughes]

Because we haven't had that problem yet. I'm not sure of the best solution.

[Chris Hughes]

There is a mathlib issue about this.

[Ken Lee]

Doesn't structure reflect better what we do in usual maths, "a group action is a tuple ..."? The actually action itself is important to keep, no?

[Ken Lee]

Ken Lee was there a particular reason why you avoided rw?

I dunno because I like term mode? @Kenny Lau

[Ken Lee]

I put your file in a washing machine

So in the shrunken version of my file, types can only have at most one action on them?

[Chris Hughes]

At most one action from the same group. Or at least it will be a pain to have multiple actions from the same group.

[Johan Commelin]

But we can use type wrappers to solve this problem.

[Chris Hughes]

I'm not sure this will always be a good solution. What if it's an action of the reals on the reals? There's a lot of stuff to transfer from reals onto wrapped reals. And then I can't do action1 x y + action2 x y, because the wrappers will be different.

[Kenny Lau]

let's think about group cohomology @Johan Commelin

[Kenny Lau]

do we have two actions from the same group on the same module?

[Johan Commelin]

Not in the generic case, right?

[Kenny Lau]

I mean do we have examples of those

[Johan Commelin]

Probably yes, I can't immediately think of any.

[Kevin Buzzard]

Tate twists

[Kenny Lau]

According to Wiki the m-th Tate twist of V is V tensor Q_p(-1) m times

[Johan Commelin]

If we want examples of this, I think we shouldn't look so far away. For any group (typically non-abelian), there is the action of G on itself by left multiplication and by conjugation. So there we have two actions.

[Johan Commelin]

Of course this example is (somewhat) moot in the case of group cohomology, because you typically want the coefficients to be abelian.

[Kevin Buzzard]

I have an MSc student who is going to work on group cohomology in Lean this coming year.