typeclass problems

Stream: general

[Kenny Lau]

This loop is breaking everything

[class_instances] (25) ?x_99 : out_param (field ?x_97) := @field_extension.to_field ?x_101 ?x_102 ?x_103 ?x_104
[class_instances] (26) ?x_104 : @field_extension ?x_101 ?x_102 ?x_103 := @algebraic_field_extension.to_field_extension ?x_105 ?x_106 ?x_107 ?x_108
[class_instances] (27) ?x_108 : @algebraic_field_extension ?x_105 ?x_106 ?x_107 := @algebraic_closure.to_algebraic_field_extension ?x_109 ?x_110 ?x_111 ?x_112

[Kenny Lau]

class alg_closed_field (α : Type*) extends field α :=
(alg_closed : ∀ f : polynomial α, f.deg > 1 → ∃ x, f.eval α α x = 0)

class field_extension (α : out_param $ Type*) (β : Type*)
  [out_param $ field α] extends field β :=
(f : α → β) [hom : is_ring_hom f]

instance field_extension.to_is_ring_hom (α : Type*) (β : Type*)
  [field α] [field_extension α β] : is_ring_hom (field_extension.f β) :=
field_extension.hom β

instance field_extension.to_algebra (α : Type*) (β : Type*)
  [field α] [field_extension α β] : algebra α β :=
{ f := field_extension.f β }

class algebraic_field_extension (α : out_param $ Type*) (β : Type*)
  [out_param $ field α] extends field_extension α β :=
(algebraic : ∀ x : β, ∃ f : polynomial α, f.eval α β x = 0)

set_option old_structure_cmd true

class algebraic_closure (α : out_param $ Type*) (β : Type*)
  [out_param $ field α] extends alg_closed_field β, algebraic_field_extension α β

set_option old_structure_cmd false

[Kenny Lau]

I'm not very good at dealing with typeclasses

[Kenny Lau]

somehow the same setting with ring instead of field doesn't cause this problem:

class algebra (R : out_param Type*) (A : Type*)
  [out_param $ comm_ring R] extends comm_ring A :=
(f : R → A) [hom : is_ring_hom f]

This doesn't cause any loops

[Kenny Lau]

solution:

class is_alg_closed_field (α : Type*) [field α] : Prop :=
(alg_closed : ∀ f : polynomial α, f.deg > 1 → ∃ x, f.eval α α x = 0)

class field_extension (α : out_param $ Type*) (β : Type*)
  [out_param $ field α] extends field β :=
(f : α → β) [hom : is_ring_hom f]

instance field_extension.to_is_ring_hom (α : Type*) (β : Type*)
  [field α] [field_extension α β] : is_ring_hom (field_extension.f β) :=
field_extension.hom β

instance field_extension.to_algebra (α : Type*) (β : Type*)
  [field α] [field_extension α β] : algebra α β :=
{ f := field_extension.f β }

class is_algebraic_field_extension (α : out_param $ Type*) (β : Type*)
  [out_param $ field α] [field_extension α β] : Prop :=
(algebraic : ∀ x : β, ∃ f : polynomial α, f.eval α β x = 0)

class is_algebraic_closure (α : out_param $ Type*) (β : Type*)
  [field α] [field_extension α β]
  extends is_alg_closed_field β, is_algebraic_field_extension α β : Prop

[Kenny Lau]

TLDR: change algebraic_field_extension (not Prop) to is_algebraic_field_extension (Prop) etc

[Kenny Lau]

update: it is not true that the algebra causes no problem

[Mario Carneiro]

out_param (field ?x_97)

not the first time I've seen this today

[Kenny Lau]

but module seems to be doing fine

[Mario Carneiro]

What caused this typeclass search? You never want to find arbitrary fields

[Kenny Lau]

what stops ring.to_module and class module ... [ring _] from forming a loop?

[Kenny Lau]

What caused this typeclass search? You never want to find arbitrary fields

I have something involving rings and no fields at all. The searcher wants to know that it has addition. Somehow it got to fields, and then it started the loop

[Mario Carneiro]

I don't mean just field ?, but also ring ? and other such things

[Mario Carneiro]

the bad sign is a class on a metavar

[Kenny Lau]

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_zero α := @pi.has_zero ?x_1 ?x_2 ?x_3
failed is_def_eq
[class_instances] (0) ?x_0 : has_zero α := cardinal.has_zero
failed is_def_eq
[class_instances] (0) ?x_0 : has_zero α := @finsupp.has_zero ?x_4 ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : has_zero α := @multiset.has_zero ?x_7
failed is_def_eq
[class_instances] (0) ?x_0 : has_zero α := unsigned.has_zero
failed is_def_eq
[class_instances] (0) ?x_0 : has_zero α := @fin.has_zero ?x_8
failed is_def_eq
[class_instances] (0) ?x_0 : has_zero α := int.has_zero
failed is_def_eq
[class_instances] (0) ?x_0 : has_zero α := nat.has_zero
failed is_def_eq
[class_instances] (0) ?x_0 : has_zero α := @no_zero_divisors.to_has_zero ?x_9 ?x_10
[class_instances] (1) ?x_10 : no_zero_divisors α := @domain.to_no_zero_divisors ?x_11 ?x_12
[class_instances] (2) ?x_12 : domain α := @linear_nonneg_ring.to_domain ?x_13 ?x_14
[class_instances] (2) ?x_12 : domain α := @to_domain ?x_13 ?x_14
[class_instances] (3) ?x_14 : linear_ordered_ring α := @linear_nonneg_ring.to_linear_ordered_ring ?x_15 ?x_16
[class_instances] (3) ?x_14 : linear_ordered_ring α := @linear_ordered_field.to_linear_ordered_ring ?x_15 ?x_16
[class_instances] (4) ?x_16 : linear_ordered_field α := @discrete_linear_ordered_field.to_linear_ordered_field ?x_17 ?x_18
[class_instances] (3) ?x_14 : linear_ordered_ring α := @linear_ordered_comm_ring.to_linear_ordered_ring ?x_15 ?x_16
[class_instances] (4) ?x_16 : linear_ordered_comm_ring α := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_17 ?x_18
[class_instances] (5) ?x_18 : decidable_linear_ordered_comm_ring α := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_19 ?x_20 ?x_21 ?x_22
[class_instances] (5) ?x_18 : decidable_linear_ordered_comm_ring α := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_18 : decidable_linear_ordered_comm_ring α := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_19 ?x_20
[class_instances] (2) ?x_12 : domain α := @division_ring.to_domain ?x_13 ?x_14
[class_instances] (3) ?x_14 : division_ring α := @field.to_division_ring ?x_15 ?x_16
[class_instances] (4) ?x_16 : field α := @field_extension.to_field ?x_17 ?x_18 ?x_19 ?x_20
[class_instances] (5) ?x_20 : @field_extension ?x_17 α ?x_19 := @algebraic_field_extension.to_field_extension ?x_21 ?x_22 ?x_23 ?x_24
[class_instances] (6) ?x_24 : @algebraic_field_extension ?x_21 α ?x_23 := @algebraic_closure.to_algebraic_field_extension ?x_25 ?x_26 ?x_27 ?x_28
[class_instances] (7) ?x_27 : field ?x_25 := @field_extension.to_field ?x_29 ?x_30 ?x_31 ?x_32
[class_instances] (8) ?x_32 : @field_extension ?x_29 ?x_30 ?x_31 := @algebraic_field_extension.to_field_extension ?x_33 ?x_34 ?x_35 ?x_36
[class_instances] (9) ?x_36 : @algebraic_field_extension ?x_33 ?x_34 ?x_35 := @algebraic_closure.to_algebraic_field_extension ?x_37 ?x_38 ?x_39 ?x_40
[class_instances] (10) ?x_39 : field ?x_37 := @field_extension.to_field ?x_41 ?x_42 ?x_43 ?x_44

[Kenny Lau]

loop the last 3 lines

[Mario Carneiro]

field_extension.to_field

[Mario Carneiro]

kill it

[Kenny Lau]

class field_extension (α : out_param $ Type*) (β : Type*)
  [out_param $ field α] extends field β :=
(f : α → β) [hom : is_ring_hom f]

[Kenny Lau]

class algebra (R : out_param Type*) (A : Type*)
  [out_param $ comm_ring R] extends comm_ring A :=
(f : R → A) [hom : is_ring_hom f]

[Kenny Lau]

class module (α : out_param $ Type u) (β : Type v) [out_param $ ring α]
  extends has_scalar α β, add_comm_group β :=
(smul_add : ∀r (x y : β), r • (x + y) = r • x + r • y)
(add_smul : ∀r s (x : β), (r + s) • x = r • x + s • x)
(mul_smul : ∀r s (x : β), (r * s) • x = r • s • x)
(one_smul : ∀x : β, (1 : α) • x = x)

[Kenny Lau]

(not that algebra is not causing problem)

[Kenny Lau]

why does module have no problem

[Kenny Lau]

@Mario Carneiro what should I replace it with?

[Kenny Lau]

I see

[Kenny Lau]

class subring (α : Type*) [comm_ring α] (S : set α) : Prop :=
(add_mem : ∀ {x y}, x ∈ S → y ∈ S → x + y ∈ S)
(neg_mem : ∀ {x}, x ∈ S → -x ∈ S)
(mul_mem : ∀ {x y}, x ∈ S → y ∈ S → x * y ∈ S)
(one_mem : (1:α) ∈ S)

open subring

instance subring.to_comm_ring (α : Type*) [comm_ring α] (S : set α) [subring α S] : comm_ring S :=
{ add            := λ ⟨x, hx⟩ ⟨y, hy⟩, ⟨x + y, add_mem hx hy⟩,
  add_assoc      := λ ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩, subtype.eq $ add_assoc x y z,
  zero           := ⟨0, eq.subst (add_neg_self (1:α)) $ add_mem (one_mem S) $ neg_mem $ one_mem S⟩,
  zero_add       := λ ⟨x, hx⟩, subtype.eq $ zero_add x,
  add_zero       := λ ⟨x, hx⟩, subtype.eq $ add_zero x,
  neg            := λ ⟨x, hx⟩, ⟨-x, neg_mem hx⟩,
  add_left_neg   := λ ⟨x, hx⟩, subtype.eq $ add_left_neg x,
  add_comm       := λ ⟨x, hx⟩ ⟨y, hy⟩, subtype.eq $ add_comm x y,
  mul            := λ ⟨x, hx⟩ ⟨y, hy⟩, ⟨x * y, mul_mem hx hy⟩,
  mul_assoc      := λ ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩, subtype.eq $ mul_assoc x y z,
  one            := ⟨1, one_mem S⟩,
  one_mul        := λ ⟨x, hx⟩, subtype.eq $ one_mul x,
  mul_one        := λ ⟨x, hx⟩, subtype.eq $ mul_one x,
  left_distrib   := λ ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩, subtype.eq $ left_distrib x y z,
  right_distrib  := λ ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩, subtype.eq $ right_distrib x y z,
  mul_comm       := λ ⟨x, hx⟩ ⟨y, hy⟩, subtype.eq $ mul_comm x y }

[Kenny Lau]

will this instance cause problems?

[Kenny Lau]

if so, what should I replace it with?

[Kenny Lau]

adding by letI := subring.to_comm_ring _ S to every definition and theorem is not very feasible

[Kenny Lau]

and is wasting me a lot of time

[Kenny Lau]

but as soon as I make it an instance, everything crashes

[Kenny Lau]

what is this

[Kenny Lau]

def Hausdorff_abelianization (G : Type*) [t : topological_group G] : Type* :=
@left_cosets (abelianization G) _ (closure {1})
  (by apply_instance)

[Kenny Lau]

[class_instances] (0) ?x_60 : topological_group G := t
failed is_def_eq

[Kenny Lau]

Lean, they are the same

[Kenny Lau]

if subring.to_comm_ring causes problems then why doesn't subtype.group cause problems?

[Kenny Lau]

@Patrick Massot @Sebastian Ullrich @Mario Carneiro it can be avoided by using universes instead of Type*

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/unfolding.20notation.20in.20theorem.20vs.20def.2Finstance/near/128167978

[Kenny Lau]

oh and of course the same trick applies to this case

[Kenny Lau]

there's no loop any more

[Kenny Lau]

once I use Type u instead of Type*

[Kenny Lau]

Lean, they are the same

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/typeclass.20problems/near/128162755

[Kenny Lau]

ditto

[Kenny Lau]

Is this a good instance?

def Hausdorff_abelianization.setoid (G : Type u)
  [topological_group G] : setoid G :=
left_rel (closure (commutator_subgroup G set.univ))

[Mario Carneiro]

A local instance maybe

[Mario Carneiro]

it looks a bit domain specific

[Kenny Lau]

domain specific?

[Mario Carneiro]

is there a reason that should be the canonical equivalence on any top group?

[Kenny Lau]

it's the functor from TopGrp to AbelianHasudorffTopGrp

[Johan Commelin]

Kenny, for every topological group G, there should be at most 1 instance of setoid G.

[Kenny Lau]

I see

[Kenny Lau]

ok this isn't canonical then

[Johan Commelin]

So you should probably not make this an instance. But possibly define AbHausTopGrp, and make it an instance of that...

[Kenny Lau]

I'm glad I didn't switch the first two words of the name of the category... :D

[Johan Commelin]

I don't get what would be wrong with that? ... Am I overly naive, and missing a joke?

[Kenny Lau]

it sounds similar to a rude word in german

[Johan Commelin]

Ach so, ich muss noch viel Deutsch üben. Und ich kenn kein unhöfliche Worten.

[Kenny Lau]

"Hau ab" means "piss off"

[Johan Commelin]

Wunderbar

[Kenny Lau]

2018-06-17-2.png

[Kenny Lau]

when I turn trace.class_instances on, there's nothing peculiar, except the has_sizeof thing getting pretty long

[Kenny Lau]

that option is not really helpful in my experience

[Kenny Lau]

@Mario Carneiro

[Kenny Lau]

oh and the depth of the class instance search never went to 6

[Kenny Lau]

and I don't think cogroup.base_change_left is the problem, after looking at the trace

[Kenny Lau]

it's here: https://github.com/kckennylau/local-langlands-abelian/blob/master/src/torus.lean#L136

[Simon Hudon]

Why does it need an instance of has_sizeof?

[Kenny Lau]

no idea

[Kenny Lau]

to build a structure, I think?

[Kenny Lau]

Please help me, my deadline is in like 12 hours

[Simon Hudon]

Your screenshot is not telling me much. If you comment one field declaration at a time, when does it stop failing?

[Kenny Lau]

as soon as I remove the last field

[Kenny Lau]

@Simon Hudon is there other information I can provide?

[Simon Hudon]

I think your project needs mathlib

[Simon Hudon]

I'm building it on my machine to have a closer look

[Kenny Lau]

thank you very much

[Kenny Lau]

yes, it does require mathlib

[Simon Hudon]

Is it possible you did not commit the latest version of leanpkg.toml? (I don't need it, I can fix it but in general, that makes things smoother for people trying your project)

[Kenny Lau]

oh I didn't really set it up

[Simon Hudon]

Ah ok. Just to be sure, do you use Lean 3.4.1 and the latest mathlib?

[Kenny Lau]

yes

[Kenny Lau]

ok not exactly the latest

[Kenny Lau]

i'm on mathlib commit fe590ca272a41bb321a13be505964e78cad1e731

[Kenny Lau]

third from latest

[Simon Hudon]

In this expression (tensor_a F split.S T) you get into trouble because split.S is a set but a type is expected. If you replace it with subtype split.S, type is required to have a comm_ring instance which you only have for T

[Kenny Lau]

:o

[Kenny Lau]

thanks

[Kenny Lau]

do you have a fix?

[Simon Hudon]

No, it really depends on what you're trying to do. If you actually want subtype split.S, you'd need to add [comm_ring (subtype split.S)] to the local instances which would get hairy because split is a field. Maybe replacing split.S with T would suit your purpose, in which case, the fit is perfect because you already have a comm_ring T instance

[Kenny Lau]

I can't just change my deifnition like that?

[Simon Hudon]

Which one?

[Kenny Lau]

replacing split.S with T?

[Simon Hudon]

That might work. I haven't tried it but that would fix that particular problem

[Kenny Lau]

I mean, it would be a wrong definition

[Simon Hudon]

What would be the right definition?

[Kenny Lau]

split.S as it is

[Simon Hudon]

That would be nonsense: that's not type correct.

[Simon Hudon]

Unless your tensor_a definition is wrong and it should take a set there, not a type

[Kenny Lau]

I'm coercing a set to a type

[Kenny Lau]

it's done automatically

[Kenny Lau]

I do it every time

[Simon Hudon]

Right but that type is then expected to be a commutative ring. I'm not sure how that can be proved automatically

[Kenny Lau]

I have a working version above it, one can trace class instance

[Kenny Lau]

I think it will go through subfield -> field -> comm_ring

[Simon Hudon]

How do you prove that it's a subfield?

[Kenny Lau]

instance finite_Galois_intermediate_extension.to_subfield

[Kenny Lau]

L132 of field_extensions.lean

[Kenny Lau]

right, I just realized, there should be no problem, because there's a working version right above it!

[Simon Hudon]

Which line?

[Kenny Lau]

The #check one

[Kenny Lau]

L139

[Kenny Lau]

oops

[Kenny Lau]

L123

[Kenny Lau]

https://github.com/kckennylau/local-langlands-abelian/blob/master/src/torus.lean#L123

[Kenny Lau]

#check λ (F : Type u) [field F]
  (AC : Type v) [field AC] [is_alg_closed_field AC]
  [field_extension F AC] [is_algebraic_closure F AC]
  (T : Type w) [comm_ring T] [algebra F T] [cogroup F T]
(split : finite_Galois_intermediate_extension F AC)
(rank : ℕ),
@cogroup_iso split.S _ (tensor_a F split.S T)
  (tensor_a.comm_ring _ _ _)
  (base_change_left F split.S T)
  (GL₁ⁿ split.S rank) _ _
  (cogroup.base_change_left F split.S T)
  (GL₁ⁿ.cogroup _ _)

[Simon Hudon]

If I change that check into a def:

def foo := λ (F : Type u) [field F]
  (AC : Type v) [field AC] [is_alg_closed_field AC]
  [field_extension F AC] [is_algebraic_closure F AC]
  (T : Type w) [comm_ring T] [algebra F T] [cogroup F T]
(split : finite_Galois_intermediate_extension F AC)
(rank : ℕ),
@cogroup_iso split.S _ (tensor_a F split.S T)
  (tensor_a.comm_ring _ _ _)
  (base_change_left F split.S T)
  (GL₁ⁿ split.S rank) _ _
  (cogroup.base_change_left F split.S T)
  (GL₁ⁿ.cogroup _ _)

[Simon Hudon]

I get I lot of errors

[Kenny Lau]

curious

[Simon Hudon]

Screen-Shot-2018-06-17-at-7.57.01-PM.png

[Simon Hudon]

I think you're asking a lot of type class inference

[Kenny Lau]

heh...

[Kenny Lau]

how about I move them before the colon

[Kenny Lau]

def foo (F : Type u) [field F]
  (AC : Type v) [field AC] [is_alg_closed_field AC]
  [field_extension F AC] [is_algebraic_closure F AC]
  (T : Type w) [comm_ring T] [algebra F T] [cogroup F T]
(split : finite_Galois_intermediate_extension F AC)
(rank : ℕ) :=
@cogroup_iso split.S _ (tensor_a F split.S T)
  (tensor_a.comm_ring _ _ _)
  (base_change_left F split.S T)
  (GL₁ⁿ split.S rank) _ _
  (cogroup.base_change_left F split.S T)
  (GL₁ⁿ.cogroup _ _)

[Kenny Lau]

no errors!

[Kenny Lau]

also I looked at the trace as I said before

[Simon Hudon]

You're right, I didn't do it well

[Kenny Lau]

there is no issue with the typeclass inferences

[Kenny Lau]

and the max depth is 5

[Kenny Lau]

there should not be any error

[Simon Hudon]

Try:

structure torus (F : Type u) [field F]
  (AC : Type v) [field AC] [is_alg_closed_field AC]
  [field_extension F AC] [is_algebraic_closure F AC]
  (T : Type w) [comm_ring T] [algebra F T] [cogroup F T] :=
(split : finite_Galois_intermediate_extension F AC)
(rank : ℕ)
(splits : foo F AC T split rank)

[Kenny Lau]

what the actual

[Kenny Lau]

@Mario Carneiro you need to see this

[Kenny Lau]

@Simon Hudon what do you think

[Simon Hudon]

I'm not actually sure why the other one wouldn't work. In general, there's nothing wrong with breaking down your definitions into smaller pieces though

[Kenny Lau]

I see

[Kenny Lau]

@Simon Hudon how should I break this loop?

[Kenny Lau]

[class_instances] (5) ?x_31 : field AC := _inst_6
failed is_def_eq
[class_instances] (5) ?x_31 : field AC := @subfield.to_field ?x_34 ?x_35 ?x_36 ?x_37
failed is_def_eq
[class_instances] (5) ?x_31 : field AC := @topological_field.to_field ?x_38 ?x_39
[class_instances] (5) ?x_31 : field AC := @linear_ordered_field.to_field ?x_34 ?x_35
[class_instances] (6) ?x_35 : linear_ordered_field AC := @discrete_linear_ordered_field.to_linear_ordered_field ?x_36 ?x_37
[class_instances] (7) ?x_37 : discrete_linear_ordered_field AC := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (5) ?x_31 : field AC := @discrete_field.to_field ?x_34 ?x_35
[class_instances] (6) ?x_35 : discrete_field AC := rat.field_rat
failed is_def_eq
[class_instances] (6) ?x_35 : discrete_field AC := @discrete_linear_ordered_field.to_discrete_field ?x_36 ?x_37
[class_instances] (7) ?x_37 : discrete_linear_ordered_field AC := rat.discrete_linear_ordered_field
failed is_def_eq
[class_instances] (5) ?x_30 : field ?x_28 := @subfield.to_field ?x_34 ?x_35 ?x_36 ?x_37
[class_instances] (6) ?x_35 : field ?x_34 := _inst_7
[class_instances] (6) ?x_37 : @subfield AC _inst_7 ?x_36 := @finite_Galois_intermediate_extension.to_subfield ?x_38 ?x_39 ?x_40 ?x_41 ?x_42 ?x_43 ?x_44 ?x_45
[class_instances] (7) ?x_39 : field ?x_38 := _inst_7
[class_instances] (7) ?x_41 : field AC := _inst_7
[class_instances] (7) ?x_42 : @is_alg_closed_field AC _inst_7 := _inst_8
[class_instances] (7) ?x_43 : @field_extension AC AC _inst_7 _inst_7 := _inst_9
failed is_def_eq
[class_instances] (7) ?x_43 : @field_extension AC AC _inst_7 _inst_7 := @is_intermediate_field.to_field_extension' ?x_46 ?x_47 ?x_48 ?x_49 ?x_50 ?x_51 ?x_52
failed is_def_eq
[class_instances] (7) ?x_43 : @field_extension AC AC _inst_7 _inst_7 := @is_intermediate_field.to_field_extension ?x_53 ?x_54 ?x_55 ?x_56 ?x_57 ?x_58 ?x_59
failed is_def_eq
[class_instances] (7) ?x_42 : @is_alg_closed_field AC _inst_7 := @is_algebraic_closure.to_is_alg_closed_field ?x_46 ?x_47 ?x_48 ?x_49 ?x_50 ?x_51
[class_instances] (8) ?x_48 : field ?x_46 := _inst_7
[class_instances] (8) ?x_49 : field AC := _inst_7
[class_instances] (8) ?x_50 : @field_extension AC AC _inst_7 _inst_7 := _inst_9
failed is_def_eq
[class_instances] (8) ?x_50 : @field_extension AC AC _inst_7 _inst_7 := @is_intermediate_field.to_field_extension' ?x_52 ?x_53 ?x_54 ?x_55 ?x_56 ?x_57 ?x_58
failed is_def_eq
[class_instances] (8) ?x_50 : @field_extension AC AC _inst_7 _inst_7 := @is_intermediate_field.to_field_extension ?x_59 ?x_60 ?x_61 ?x_62 ?x_63 ?x_64 ?x_65
failed is_def_eq

[Simon Hudon]

There seems to be a circular dependency between your instances. You should try to guarantee that something decreases (syntactically) whenever you apply an instance. For example, instance [decidable_eq a] : decidable_eq (list a) := ... is such an instance. It is about list a and all the instances it relies on involve simpler expressions.

[Kenny Lau]

sorry but could you explain what you mean by decreasing?

[Simon Hudon]

If you compare a and list a (one is a type in an assumed instance, the other, in the head of the instance) list a is a more complex expression than a. That means that if I look for an instance of decidable_eq (list a) and I apply the above instance, I'm decreasing the size of my problem so I'm getting closer to a solution. If every instance decreases the size of the problem, you can't search forever. (just like with structural recursion)

[Kenny Lau]

hmm... but there are times at which I would need to infer simpler instances from complex instances?

[Simon Hudon]

like field from discrete_linear_ordered_field?

[Kenny Lau]

sure

[Kenny Lau]

or sometimes I need to infer a single instance from like 10 instances

[Kenny Lau]

do you have general workarounds?

[Simon Hudon]

A single instance from 10 instances is not a problem as long as each instance is smaller than the initial one

[Kenny Lau]

hmm I still don't know how to judge whether two instances are smaller

[Simon Hudon]

In the case of discrete_linear_ordered_field, does it not extend field?

[Kenny Lau]

I mean, your examples are quite obvious

[Kenny Lau]

yes it does

[Kenny Lau]

I think

[Simon Hudon]

That should be enough, no? You don't need an instance on top of that

[Kenny Lau]

this is a bad instance then?

instance subring.to_comm_ring (α : Type u) [comm_ring α] (S : set α) [subring α S] : comm_ring S :=

[Simon Hudon]

You can compare by counting the number of symbols and operators in each types.

[Kenny Lau]

that instance doesn't seem to be causing much problem though

[Kenny Lau]

I guess it's because it requires subring

[Kenny Lau]

This seems to be the problem:

instance finite_Galois_intermediate_extension.to_subfield
  (F : Type u) [field F]
  (AC : Type v) [field AC] [is_alg_closed_field AC]
  [field_extension F AC] [is_algebraic_closure F AC]
  (E : finite_Galois_intermediate_extension F AC) :
  subfield _ E.S :=
by apply_instance

[Simon Hudon]

subring is actually what I find problematic in it

[Kenny Lau]

because I have an instance from subfield to field

[Kenny Lau]

subring is actually what I find problematic in it

how so?

[Simon Hudon]

there are invisible operators: comm_ring S is actually comm_ring (subtype S) which is more complex than comm_ring a. However subring a (subtype S) is more complex than comm_ring (subtype S)

[Kenny Lau]

nah it's subring a S

[Kenny Lau]

there is no coercion there

[Simon Hudon]

It might actually fly then

[Simon Hudon]

Lean is actually more tolerant than what I'm used to and I'm not sure if that's a good thing or if it's just handing you enough rope to hang yourself with

[Kenny Lau]

this should be the problem

[Kenny Lau]

[class_instances] (5) ?x_30 : field ?x_28 := @subfield.to_field ?x_34 ?x_35 ?x_36 ?x_37
[class_instances] (6) ?x_35 : field ?x_34 := _inst_7
[class_instances] (6) ?x_37 : @subfield AC _inst_7 ?x_36 := @finite_Galois_intermediate_extension.to_subfield ?x_38 ?x_39 ?x_40 ?x_41 ?x_42 ?x_43 ?x_44 ?x_45
[class_instances] (7) ?x_39 : field ?x_38 := _inst_7
[class_instances] (7) ?x_41 : field AC := _inst_7
[class_instances] (7) ?x_42 : @is_alg_closed_field AC _inst_7 := _inst_8

[Kenny Lau]

right, subfield.to_field is the problem

[Simon Hudon]

You can try commenting one instance at a time until the problem disappears

[Simon Hudon]

cool

[Kenny Lau]

that isn't how it works

[Kenny Lau]

if I comment one instance out, a million lines of code will break

[Kenny Lau]

@Simon Hudon a million things depend on subfield.to_field though...

[Kenny Lau]

this is a huge abyss

[Simon Hudon]

does subfield extend field?

[Kenny Lau]

no

[Simon Hudon]

Why not?

[Kenny Lau]

just as is_subgroup does not extend group

[Kenny Lau]

and as I say this sentence

[Kenny Lau]

why doesn't that cause problems?

[Simon Hudon]

I'm not intimate enough with the algebraic hierarchy to know

[Kenny Lau]

#check @subtype.group
/-
subtype.group : Π {α : Type u_1} [_inst_1 : group α] {s : set α} [_inst_2 : is_subgroup s], group ↥s
-/

[Simon Hudon]

Actually, because there's no coercion, that's not that big of a deal. A different instance must be worse

[Kenny Lau]

hmm

[Kenny Lau]

this is a huge mess

[Simon Hudon]

Yeah, that's a problem with this way of doing type classes. You can't understand each instance in isolation

[Kenny Lau]

I think depth first search is not very good

[Kevin Buzzard]

Kenny remember as a last resort you can just override the type class system and give it the instances yourself. I used to do this all the time when I got stuck on (much easier) stuff.

[Alex J. Best]

I just made the PR #1822 where I did something bad and broke multiplication, but I'm not sure how to fix it. I'm not sure how to minify it but you can look at line 154 in https://github.com/leanprover-community/mathlib/blob/6764734114a5e07eddc0409e485eb0bab6aea161/src/ring_theory/dedekind_finite.lean#L154 compared to 115 where somehow the intervening instance instance dedekind_finite_of_noetherian [is_noetherian_ring R] : dedekind_finite R := breaks monoid.has_mul.

[Kevin Buzzard]

You should ask permission to make new branches on leanprover-community; that way I could use cache-olean to make checking out your issue less of a hassle.

[Alex J. Best]

I hereby ask for permission! Sorry, I also just added a new better version, but the question /relevant part is still the same.

[Kevin Buzzard]

Here's the instance trace. I think you might have created a loop. For example I see

[class_instances] (17) ?x_59 : field G := real.field
failed is_def_eq
[class_instances] (17) ?x_59 : field G := rat.field
failed is_def_eq
...
[class_instances] (17) ?x_59 : field G := real.field
failed is_def_eq
[class_instances] (17) ?x_59 : field G := rat.field
failed is_def_eq
...
[class_instances] (20) ?x_124 : field G := real.field
failed is_def_eq
[class_instances] (20) ?x_124 : field G := rat.field
failed is_def_eq
...
[class_instances] (18) ?x_65 : field G := real.field
failed is_def_eq
[class_instances] (18) ?x_65 : field G := rat.field
failed is_def_eq
...
[class_instances] (19) ?x_67 : field G := real.field
failed is_def_eq
[class_instances] (19) ?x_67 : field G := rat.field
failed is_def_eq
...
[class_instances] (19) ?x_67 : field G := real.field
failed is_def_eq
[class_instances] (19) ?x_67 : field G := rat.field
failed is_def_eq
...
[class_instances] (19) ?x_67 : field G := real.field
failed is_def_eq
[class_instances] (19) ?x_67 : field G := rat.field
failed is_def_eq
...

but actually that just looks weird (to me), usually the numbers just creep up by one.

[Kevin Buzzard]

[class_instances] (3) ?x_11 : ring G := @dedekind_finite.to_ring ?x_12 ?x_13
[class_instances] (4) ?x_13 : dedekind_finite G := @ @_root_.dedekind_finite_of_noetherian ?x_17 ?x_18 ?x_19
[class_instances] (5) ?x_18 : ring G := @dedekind_finite.to_ring ?x_20 ?x_21
[class_instances] (6) ?x_21 : dedekind_finite G := @ @_root_.dedekind_finite_of_noetherian ?x_25 ?x_26 ?x_27
...

I think that's your problem.

[Kevin Buzzard]

To prove G is a ring it suffices to prove it's Dedekind finite, to prove it's Dedekind finite it suffices to prove it's a Noetherian ring and...oh.. also a ring! And to check that it's a ring, it suffices to prove it's Dedekind finite, and off we go again.

[Kevin Buzzard]

You wrote

variables (R : Type*)

class dedekind_finite extends ring R :=
( inv_comm : ∀ a b : R, a * b = 1 → b * a = 1 )

and I am wondering whether this should be

class dedekind_finite (R : Type*) [ring R] :=
( inv_comm : ∀ a b : R, a * b = 1 → b * a = 1 )

but unfortunately I am guessing here. I don't really understand how these things work -- I don't really understand the difference between the two in practice.

[Kevin Buzzard]

The thing I know for sure is that I am quoting the last (3), the last (4), the last (5)...in the instance trace, which means for sure that things are spiralling out of control.

[Kevin Buzzard]

OK so I can't guarantee that my fix is what you should be doing, but it does seem to fix the problem. You have to add the extra ring instances

variables (x y : Π i, f i) (i : I) [∀ i, ring (f i)]

on line 27 but then the monoid error goes away. (I also have an error in dedekind_finite_of_noetherian but that was before I started fiddling and it might be because I just cut and pasted the file instead of forking your clone)

[Kevin Buzzard]

I hereby ask for permission! Sorry, I also just added a new better version, but the question /relevant part is still the same.

@Simon Hudon -- who can add people to the "can push to mathlib non-master branch" list? Is it you? Alex is alexjbest on github

[Simon Hudon]

The invite is in the mail. @Alex J. Best let me know if you encounter any issues

[Alex J. Best]

Thanks @Kevin Buzzard and @Johan Commelin for the very helpful comments! It looks like it works well with classes taking ring as a parameter instead of extending (I should have copied the way is_noetherian_ring is set up, rather than integral_domain!) I'll do some more tidy up and push it (unfortunately I can't see a way to change the PR branch but for the next one I should be able to push to mathlib instead (ty @Simon Hudon ))

[Oliver Nash]

I've been suffering with some typeclass problems which I've managed to reduce to the following:

import ring_theory.algebra

universes u v

section prio
set_option default_priority 200 -- No problem if priority 199 or lower, evidently because algebra.to_module has priority 200
class foo (R : Type u) (M M'  : Type v)
  [comm_ring R] [add_comm_group M] [add_comm_group M'] [module R M] extends module R M' :=
(f : M →ₗ[R] M')
end prio

set_option class.instance_max_depth 100
set_option trace.class_instances true

instance bar (R : Type u) (A : Type v)
  [comm_ring R] [ring A] [algebra R A] : module R A := infer_instance

[Oliver Nash]

The above will report that maximum class-instance resolution depth has been reached when elaborating bar but it will work if we lower the priority of the instances created by the declaration of foo, as indicated in my comment.

[Oliver Nash]

I do not understand the "Prolog-like search" that is performed as part of typeclass inference well at all but I am surprised because my fuzzy understanding had lead me to believe that changing priorities like this should merely affect performance, rather than the actual results. Evidently I am in error. Can anyone shed any light?

[Kevin Buzzard]

Typeclass loops can cause the max class-instance error and changing priorities can avoid the loops because a solution might be found before the loop is found

[Oliver Nash]

Furthermore, in debugging this, I attempted to read my first "class-instance resolution trace", and I note that my definition foo appears to introduce a looping behaviour, based on the following output from lean foobar.lean 2>&1 | grep foo.to_module:

[Oliver Nash]

[class_instances] (0) ?x_0 : @module R A (@comm_ring.to_ring R _inst_1) (@ring.to_add_comm_group A _inst_2) := @foo.to_module ?x_98 ?x_99 ?x_100 ?x_101 ?x_102 ?x_103 ?x_104 ?x_105
[class_instances] (1) ?x_104 : @module R (free_abelian_group ?x_122) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_122) := @foo.to_module ?x_222 ?x_223 ?x_224 ?x_225 ?x_226 ?x_227
[class_instances] (2) ?x_228 : @module R (free_abelian_group ?x_246) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_246) := @foo.to_module ?x_360 ?x_361 ?x_362 ?x_363 ?x_364 ?x_365
[class_instances] (3) ?x_366 : @module R (free_abelian_group ?x_384) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_384) := @foo.to_module ?x_498 ?x_499 ?x_500 ?x_501 ?x_502 ?x_503
[class_instances] (4) ?x_504 : @module R (free_abelian_group ?x_522) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_522) := @foo.to_module ?x_636 ?x_637 ?x_638 ?x_639 ?x_640 ?x_641
[class_instances] (5) ?x_642 : @module R (free_abelian_group ?x_660) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_660) := @foo.to_module ?x_774 ?x_775 ?x_776 ?x_777 ?x_778 ?x_779
[class_instances] (6) ?x_780 : @module R (free_abelian_group ?x_798) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_798) := @foo.to_module ?x_912 ?x_913 ?x_914 ?x_915 ?x_916 ?x_917
[class_instances] (7) ?x_918 : @module R (free_abelian_group ?x_936) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_936) := @foo.to_module ?x_1050 ?x_1051 ?x_1052 ?x_1053 ?x_1054 ?
[class_instances] (8) ?x_1056 : @module R (free_abelian_group ?x_1074) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_1074) := @foo.to_module ?x_1188 ?x_1189 ?x_1190 ?x_1191 ?x_119
[class_instances] (9) ?x_1194 : @module R (free_abelian_group ?x_1212) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_1212) := @foo.to_module ?x_1326 ?x_1327 ?x_1328 ?x_1329 ?x_133
[class_instances] (10) ?x_1332 : @module R (free_abelian_group ?x_1350) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_1350) := @foo.to_module ?x_1464 ?x_1465 ?x_1466 ?x_1467 ?x_14
[class_instances] (11) ?x_1470 : @module R (free_abelian_group ?x_1488) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_1488) := @foo.to_module ?x_1602 ?x_1603 ?x_1604 ?x_1605 ?x_16
[class_instances] (12) ?x_1608 : @module R (free_abelian_group ?x_1626) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_1626) := @foo.to_module ?x_1740 ?x_1741 ?x_1742 ?x_1743 ?x_17
[class_instances] (13) ?x_1746 : @module R (free_abelian_group ?x_1764) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_1764) := @foo.to_module ?x_1878 ?x_1879 ?x_1880 ?x_1881 ?x_18
[class_instances] (14) ?x_1884 : @module R (free_abelian_group ?x_1902) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_1902) := @foo.to_module ?x_2016 ?x_2017 ?x_2018 ?x_2019 ?x_20
[class_instances] (15) ?x_2022 : @module R (free_abelian_group ?x_2040) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_2040) := @foo.to_module ?x_2154 ?x_2155 ?x_2156 ?x_2157 ?x_21
[class_instances] (16) ?x_2160 : @module R (free_abelian_group ?x_2178) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_2178) := @foo.to_module ?x_2292 ?x_2293 ?x_2294 ?x_2295 ?x_22
[class_instances] (17) ?x_2298 : @module R (free_abelian_group ?x_2316) (@comm_ring.to_ring R _inst_1) (free_abelian_group.add_comm_group ?x_2316) := @foo.to_module ?x_2430 ?x_2431 ?x_2432 ?x_2433 ?x_24
[class_instances] (18) ?x_2436 : @module R (free_abelian_group

[Oliver Nash]

@Kevin Buzzard Thank you, that is consistent with my fuzzy understanding.

[Oliver Nash]

So what is the take-home message here? Is it:

1. I need to be more careful about instance priorities?, or
2. Priorities aside, the definition of foo is faulty / unidiomatic in some way?, or
3. I should give up on extends and just make module R M' a parameter in the definition of foo?, or
4. Something else?

[Oliver Nash]

(deleted)

[Oliver Nash]

My guess is that there is no unconditional answer to the above, and the best one can say is "sometimes option 1, sometimes option 3", depending on the situation.

[Kevin Buzzard]

You're not allowed to make instance loops, that's the take home message I think. I'm certainly not an expert at this stuff but we saw the other day how extending a typeclass as opposed to asking for it can cause trouble sometimes

[Kevin Buzzard]

I think foo.to_module exists because you're extending. I'd love to point you to some docs explaining the basic do's and don'ts in this area but there aren't any and I can't write them

[Oliver Nash]

Thanks. Yes, I believe one of the things that extending does is to create foo.to_module; I too would love to read such docs, but I’ll happily plough ahead for now and wait till they are written (perhaps after Lean 4 arrives).

[Oliver Nash]

I think I more or less understand the no loops prohibition (a tree-like search can't search a general graph) but I need to sharpen my understanding a little. I still have various questions but I'm unblocked so I think I'll just put them aside for now and see how I go when I pick this up, in a few days. Thanks again.

[Mario Carneiro]

The general rule being violated here is that foo has three explicit (type) args, but it has a parent that has only two

[Mario Carneiro]

which means that during instance search M gets invented, leading to the instance loop

[Kevin Buzzard]

What's a parent? Something it extends?

[Kevin Buzzard]

This can be avoided by just using [module R M'] right?

[Mario Carneiro]

yes

[Oliver Nash]

@Mario Carneiro Thank you, that is extremely helpful!

[Daniel Selsam]

Can anyone come up with a simple, mathematically-motivated version of the reduced problem @Oliver Nash introduced in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/typeclass.20problems/near/184185635 ? Specifically, I am looking for any simple example of a "natural" collection of "action-like" instances that cannot be used in Lean3 because they would induce a cycle. Here by cycle I mean literally a cycle where the same exact subgoal repeats, and not just any infinite loop such as in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Cute.20instance.20loop/near/180140798 . Thanks!

[Daniel Selsam]

Fun fact: tangent_space.topological_space would induce a cycle on its own, if only tangent_space and topological_fiber_bundle_core.fiber were not considered opaque inside typeclass resolution. The following loops in current mathlib:

local attribute [reducible] tangent_space topological_fiber_bundle_core.fiber
example {𝕜 E : Type} [nondiscrete_normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] : topological_space E :=
by apply_instance

[Floris van Doorn]

Do you mean something like this?

import ring_theory.algebra
universe variables u v w

instance foo {k : Type u} {A : Type v} {M : Type w}
  [comm_ring k] [ring A] [add_comm_group M] [algebra k A] [module A M] :
  module k M :=
by sorry

set_option trace.class_instances true

attribute [instance, priority 2000] ring.to_add_comm_group
example {k : Type u} {A : Type v} {M : Type w}
  [comm_ring k] [comm_ring A] [ring M] [algebra k A] [algebra A M] :
  module k M :=
by apply_instance

Here type-class inference is trying to find ring ?M but doesn't know that ?M should be A, and therefore goes in an infinite loop.

[Daniel Selsam]

@Floris van Doorn Thank you. I apologize that I was not precise enough in my request, and unfortunately this is not quite what I am looking for. First, this problem seems to be dependent on the order in which the instance subgoals are solved. The [ring A] argument of foo appears in the downstream instance, and it is a separate and easily fixable problem to simply postpone the search for such instances, e.g. by searching for the instances from right-to-left instead of left-to-right (which is what we do in Lean4). It would be great to find a small collection of desirable instances that would loop even under the right-to-left policy. Also, by "mathematically-motivated" I meant instances with real names and meanings, as opposed to (presumably) artificial instances like foo.

[Kevin Buzzard]

foo has a real mathematical meaning. An example of foo is the statement that a complex vector space can be considered as a real vector space (of twice the dimension, in this setting).

[Daniel Selsam]

@Kevin Buzzard Thanks. What would be a good name for this instance then? Also, I suppose this instance is problematic no matter which direction we solve the subgoals in. If we go right-to-left, we immediately cycle. However, it does seems to work when algebra k A is tried before module A M:

import ring_theory.algebra

universe variables u v w

instance foo {k : Type u} {A : Type v} {M : Type w}
  (_ : comm_ring k) (_ : ring A) (_ : add_comm_group M) [algebra k A] [module A M] :
  module k M :=
by sorry

attribute [instance, priority 2000] ring.to_add_comm_group
example {k : Type u} {A : Type v} {M : Type w}
  [comm_ring k] [comm_ring A] [ring M] [algebra k A] [algebra A M] :
  module k M :=
by apply_instance -- works

[Yury G. Kudryashov]

In this particular case a possible solution is to have a tag "don't try this instance if k = A".

[Johan Commelin]

@Daniel Selsam It could be called restrict_scalars

[Daniel Selsam]

Is there a reasonable "sister" instance that would make it loop even if algebra k A were tried first, before module A M?

[Yury G. Kudryashov]

There is instance algebra.id [comm_ring R] : algebra R R.

[Yury G. Kudryashov]

BTW, if we define algebra.trans similarly to restrict_scalars, then algebra.id + algebra.trans will create a loop too.

[Daniel Selsam]

BTW, if we define algebra.trans similarly to restrict_scalars, then algebra.id + algebra.trans will create a loop too.

Could you please post code for the algebra.trans you envision?

[Yury G. Kudryashov]

Look at algebra.comap in ring_theory/algebra.lean. This is what I meant but it has a type tag to avoid loops.

[Yury G. Kudryashov]

I don't know if we would want to have algebra.trans as an instance (without a type tag) if it was possible.

[Yury G. Kudryashov]

instance algebra.trans [comm_ring R] [comm_ring S] [ring A] [algebra R S] [algebra S A] : algebra R A :=
{ smul := λ r x, (algebra_map S r • x : A),
  to_fun := (algebra_map A : S → A) ∘ algebra_map S,
  hom := by apply_instance,
  commutes' := λ r x, algebra.commutes _ _,
  smul_def' := λ _ _, algebra.smul_def _ _ }

[Yury G. Kudryashov]

(untested)

[Yury G. Kudryashov]

(tested, works, needs some defs from ring_theory/algebra.lean)

[Chris Hughes]

algebra.comap is a nightmare. If you prove a theorem using algebra.comap, you won't be able to apply it easily to three rings where the canonical homomorphisms don't commute by definition. For example the $\mathbb{Q}$-algebra structure on $\mathbb{C}$, is not defeq to (coe : ℝ → ℂ) ∘ (coe : ℚ → ℝ). algebra.trans shouldn't be an instance because of these diamonds, and we also shouldn't prove theorems with algebra.trans in the statement. That does lead to ugly statements however.

[Yury G. Kudryashov]

@Chris Hughes Thank you for the explanation.

[Johan Commelin]

I think that Chris raises a very important problem. Without a good way to deal with commutative diagrams, advancing in commutative algebra will be nasty

[Johan Commelin]

Of course we can just add proof obligations. But if it isn't done carefully, it makes everything hard to read and hard to write.

[Johan Commelin]

In an ideal world, you just "bless" a diagram as being commutative, and don't need to mention it again. Some system (not type class inference, but maybe similar) should just solve these issues in the background.

[Johan Commelin]

Finding paths through a graph is something that computers are better at than humans. So this part of proving should certainly not be kicked back into the users lap.

[Daniel Selsam]

@Chris Hughes I am not sure if I understand. Are you saying that even in Lean4, where typeclass resolution will handle cycles and diamonds correctly, algebra.trans would still be a bad instance because the path that typeclass resolution takes through the algebra.trans graph will affect whether some highly desirable definitional equalities hold or not?

According to the comment in algebra.lean, algebra.comap is a workaround for not being able to use algebra.trans. When you say it is a nightmare, are you saying it is a nightmare for the same reason that algebra.trans would be a nightmare? Can you please give an example of an "ugly" statement that avoids both?

Thanks very much.

[Johan Commelin]

As far as I understand, the problem that Chris mentions affects both algebra.comap and algebra.trans. Suppose that A → B → C are ring homs. Then C is an algebra over B, and B over A. By transitivity, C is also an algebra over A. But this fixes a particular (i.e., the transitive one) algebra structure for C over A. In practice, if one wants to apply a lemma, (e.g. to ℚ → ℝ → ℂ) then there is another algebra structure floating around which is not defeq to the transitive one.

[Daniel Selsam]

Thanks.

[Daniel Selsam]

I have not been able to get the restrict_scalars example to loop when it could have succeeded, once I controlled the subgoal ordering more carefully. So, I am still looking for a more compelling example of no-cycle-support being annoying in Lean3, or for a new cycle that you will want to introduce in Lean4.

[Johan Commelin]

https://cloud.commelin.net/s/C8PrCLoxe7995Nk is a picture of a type class graph that algebraic geometers have in their head, and use all the time.

[Johan Commelin]

@Daniel Selsam We currently cannot state this graph yet, because we haven't built enough algebraic geometry yet.

[Johan Commelin]

But all the info in this graph is used implicitly on almost every page of algebraic geometry (after introductory lecture notes)

[Johan Commelin]

So, this is not really a Lean 3 example. But being able to support dependencies like those in this graph would be really cool. As far as I understand, Lean 3 wouldn't be able to do that.

[Daniel Selsam]

Interesting, thank you. What is the difference between the dotted edges, the regular edges, and the dark edges?

[Johan Commelin]

The bold edges seem to "merge" two dependencies

[Johan Commelin]

The dotted edges are considered "trivial" (either because the definition extends the other) or because, well... it's trivial (i.e., doesn't require proof in Hartshorne – one of the main introductory texts in AG).

[Johan Commelin]

I found this graph on the wall of my office, when I arrived here in Freiburg. I think it's from an appendix in a book on AG by Goertz and Wedhorn.

[Johan Commelin]

I left it on the wall :grinning_face_with_smiling_eyes:

[Daniel Selsam]

Thanks.

[Yury G. Kudryashov]

@Daniel Selsam One more typeclass related problem, see #1875 https://github.com/leanprover-community/mathlib/pull/1875#discussion_r366674829 for a context, or below for a minimal example.

noncomputable theory
open_locale classical

variables {α : Type*} {β : Type*}
def indicator [has_zero β] (s : set α) (f : α → β) : α → β := λ x, if x ∈ s then f x else 0

@[instance] axiom is_add_monoid_hom.indicator (β : Type*) [add_monoid β] (s : set α) :
  is_add_monoid_hom (λf:α → β, indicator s f)

lemma indicator_sum [add_comm_monoid β] {ι : Type*} (I : finset ι) (s : set α) (f : ι → α → β) :
  indicator s (I.sum f) = I.sum (λ i, indicator s (f i)) :=
begin
  convert (finset.sum_hom _ _).symm,
  convert is_add_monoid_hom.indicator β s
end

lemma indicator_sum' [add_comm_monoid β] {ι : Type*} (I : finset ι) (s : set α) (f : ι → α → β) :
  indicator s (I.sum f) = I.sum (λ i, indicator s (f i)) :=
(finset.sum_hom _ _).symm

The begin ... end proof works while the last line fails to unify add_monoid (α → β) from add_comm_monoid.to_add_monoid (pi.add_comm_monoid ...) with pi.add_monoid .... I have no idea how hard is to improve the situation here.

[Mario Carneiro]

I think this is missing MWE stuff

[Yury G. Kudryashov]

@Mario Carneiro What do you mean?

[Mario Carneiro]

what are the imports? I'm pretty sure is_add_monoid_hom is not in core

[Mario Carneiro]

ideally this should not have any imports, so it can be a standalone example that ports to lean 4

[Yury G. Kudryashov]

I'll try to post a version with no imports.

[Yury G. Kudryashov]

When I try to create a version with no imports and most def / lemma replaced by constant / axiom, it works... I'll try again tomorrow.

[Yury G. Kudryashov]

Probably this is a bug in pi_instance. It generates strange add_monoid.zero and add_monoid.add. I'll see if I can make it reuse pi.has_zero.