more type class inference issues

Stream: general

[Kevin Buzzard]

It seems to me that for classes like ringdefined in core lean or mathlib, you are kind of supposed to use type class inference to make them work.

[Kevin Buzzard]

For example, class is_ring_hom {α : Type u} {β : Type v} [ring α] [ring β] (f : α → β) : Prop := ... is now in mathlib

[Kevin Buzzard]

now I don't actually know how to make type class inference work in all cases, so I spend some of my time working around it.

[Kevin Buzzard]

Here's an example. I have the following structure in my code:

[Kevin Buzzard]

structure presheaf_of_rings (α : Type*) [T : topological_space α] extends presheaf_of_types α :=
(Fring : ∀ {U} (OU : T.is_open U), comm_ring (F OU))
(res_is_ring_morphism : ∀ (U V : set α) (OU : T.is_open U) (OV : T.is_open V) (H : V ⊆ U),
  is_ring_hom (res U V OU OV H))

[Kevin Buzzard]

Yesterday, is_ring_hom was about comm_ring, and I used it in my code via @is_ring_hom _ _ (FPR.Fring HU) (GPR.Fring HU) ..., explicitly giving the proof that something was a comm_ring.

[Kevin Buzzard]

But now it's changed to ring and so either I figure out a way of explicitly turning a comm_ring into a ring

[Kevin Buzzard]

or I ask here about how I should be doing this properly.

[Kevin Buzzard]

In short, Lean / mathlib seems to want me, by default, to prove that things are rings by type class inference.

[Kevin Buzzard]

How do I ensure that every time I access a presheaf_of_rings as defined above, presheaf_of_rings.Fring is added to the type class inference system?

[Kevin Buzzard]

Is there some clever trick involving an instance statement directly after the definition of presheaf_of_rings?

[Kevin Buzzard]

Oh yeah :-)

[Kevin Buzzard]

instance presheaf_of_rings_Fring (α : Type*) [T : topological_space α] {U : set α} (FPR : presheaf_of_rings α) (OU : T.is_open U) : comm_ring (FPR.F OU) :=
FPR.Fring OU

[Kevin Buzzard]

As you were :-)

[Kevin Buzzard]

What does this mean?

[Kevin Buzzard]

structure presheaf_of_rings (α : Type*) [T : topological_space α] extends presheaf_of_types α :=
[Fring : ∀ {U} (OU : T.is_open U), comm_ring (F OU)]
(res_is_ring_morphism : ∀ (U V : set α) (OU : T.is_open U) (OV : T.is_open V) (H : V ⊆ U),
  is_ring_hom (res U V OU OV H))

[Kevin Buzzard]

Is that a thing? It doesn't seem to be a thing.

[Chris Hughes]

comm_ring.to_ring might help

[Chris Hughes]

attribute [instance] presheaf_of_rings.Fring might also help

[Chris Hughes]

Just add that ^ line after the definition of presheaf_of_rings

[Kevin Buzzard]

Oh that's a better way :-) Thanks Chris, I'm glad I asked now.

[Kevin Buzzard]

I specifically wanted to avoid comm_ring.to_ring as I am pretty sure that the whole point of type class inference is that the end user shouldn't have to use such functions.

[Kevin Buzzard]

Actually, is the following a potential problem with the type class system:

[Kevin Buzzard]

My understanding (incomplete) of something Johannes was saying a few days ago to Patrick, was that the reason topological_space is defined as a structure with the class attribute added later, rather than a class directly, was that there were occasions when you might want to consider more than one topological space structure on a given type.

[Kevin Buzzard]

but ring is defined as a class in core lean

[Kevin Buzzard]

so what about the person who wants to prove theorems about putting different ring structures on a type?

[Kevin Buzzard]

Are they forced to abandon the type class system, and then they really would have to learn the names of all the theorems mapping a ring to an additive group etc?

[Kevin Buzzard]

And here's another question: what if the ring instance is in the same structure?

[Kevin Buzzard]

structure presheaf_of_rings_on_basis {X : Type u} [TX : topological_space X]
  {B : set (set X)} (HB : topological_space.is_topological_basis B) extends presheaf_of_types_on_basis HB :=
(Fring : ∀ {U} BU, comm_ring (F BU))
(res_is_ring_morphism : ∀ {U V} (BU : U ∈ B) (BV : V ∈ B) (H : V ⊆ U),
  @is_ring_hom _ _ (@Fring U BU) (Fring BV) (@res U V BU BV H))

[Kevin Buzzard]

Here a presheaf_of_rings_on_basis has Fring saying something is a commutative ring, and then res_is_ring_morphism which immediately wants to use type class inference to deduce that Fring U BU is a ring. Now do I really have to use comm_ring.to_ring?

[Kevin Buzzard]

structure presheaf_of_rings_on_basis {X : Type u} [TX : topological_space X]
  {B : set (set X)} (HB : topological_space.is_topological_basis B) extends presheaf_of_types_on_basis HB :=
(Fring : ∀ {U} (BU : U ∈ B), comm_ring (F BU))
(res_is_ring_morphism : ∀ {U V} (BU : U ∈ B) (BV : V ∈ B) (H : V ⊆ U),
  @is_ring_hom _ _ (@comm_ring.to_ring _ (Fring BU)) (@comm_ring.to_ring _ (Fring BV)) (@res U V BU BV H))

[Kevin Buzzard]

Type class inference is failing me badly here. Sorry for no MWE, hopefully people can see the problem; Lean wants me to use type class inference to prove that commutative rings are rings but I don't know how to make this happen in this situation.

[Mario Carneiro]

that's what the brackets inside the structure are for

[Kevin Buzzard]

?

[Kevin Buzzard]

Oh!

[Kevin Buzzard]

:-)

[Kevin Buzzard]

structure presheaf_of_rings_on_basis {X : Type u} [TX : topological_space X]
  {B : set (set X)} (HB : topological_space.is_topological_basis B) extends presheaf_of_types_on_basis HB :=
[Fring : ∀ {U} (BU : U ∈ B), comm_ring (F BU)]
(res_is_ring_morphism : ∀ {U V} (BU : U ∈ B) (BV : V ∈ B) (H : V ⊆ U),
  is_ring_hom (@res U V BU BV H))

[Kevin Buzzard]

So just to be clear -- the square brackets inside the structure trigger type class inference only within the structure definitions?

[Mario Carneiro]

I think they also mark it as an instance, but you should #print to be sure

[Kevin Buzzard]

I don't think they do

[Kevin Buzzard]

because that was what prompted the question about why the square brackets within the structure definition was even a thing

[Kevin Buzzard]

earlier

[Mario Carneiro]

you shouldn't need @res either

[Kevin Buzzard]

yes, that's gone now

[Kevin Buzzard]

But your change of is_ring_hom from [comm_ring] to [ring] has thrown up one final type class inference issue which I can't solve

[Kevin Buzzard]

possibly because it's not solvable

[Kevin Buzzard]

I think I do need an MWE for this one

[Kevin Buzzard]

Oh no it's Ok, indeed I am now pretty convinced that the square brackets in the structure definition do not insert anything into the type class inference system globally

[Kevin Buzzard]

because my final problem was solved by Chris' instance trick.

[Kevin Buzzard]

Oh this is great. I got stuck on these problems before and blamed it on the type class inference system not being smart enough.

[Kevin Buzzard]

I should have asked for help earlier.

[Kevin Buzzard]

Patrick said the same thing -- I told him to give up on coercions because they weren't smart enough

[Kevin Buzzard]

and he pointed out that whenever he'd got stuck before, you (Mario) had had a trick which got him through.

[Kevin Buzzard]

Here's a weird question. It feels to me like comm_ring.to_ring should not be the kind of function which end users have to worry about, because when the devs made ring a typeclass they are somehow declaring that Lean will automatically take care of inferences of this nature.

[Kevin Buzzard]

Am I right in thinking that an end user should only have to invoke comm_ring.to_ring in exceptional circumstances?

[Kevin Buzzard]

(says the person who just managed to avoid all uses of it when his code broke in lots of places)

[Kevin Buzzard]

(when a comm_ring changed to a ring)

[Kevin Buzzard]

Aah, more generally should an end user never have to explicitly invoke any theorem tagged with the instance attribute?

[Kevin Buzzard]

(unless they are putting more than one structure of a typeclass onto one type, say)

[Chris Hughes]

Sorry to hijack your thread, but I have a typeclass issue of my own

import data.int.modeq

instance Zmod_setoid {n : ℤ} : setoid ℤ :=
{ r := int.modeq n,
  iseqv := ⟨int.modeq.refl, @int.modeq.symm n, @int.modeq.trans n⟩ }

def Zmod (n : ℤ) : Type := quotient (@Zmod_setoid n)

private def add_aux {n : ℤ} (a b : Zmod n) : Zmod n :=
quotient.lift_on₂ a b (λ a b, ⟦a + b⟧) sorry

It cannot infer the setoid instance, probably because it requires an argument. Not sure of a good solution to this.

[Mario Carneiro]

This is a common problem; I think the lift_on recursor does not correctly deliver the expected type to the lambda. The usual solution is to add an ascription at the lambda:

private def add_aux {n : ℤ} (a b : Zmod n) : Zmod n :=
quotient.lift_on₂ a b (λ a b, (⟦a + b⟧ : Zmod n)) sorry

[Chris Hughes]

Still not working I'm getting this message

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ⁇
inferred
  Zmod_setoid n

[Kevin Buzzard]

import data.int.modeq

instance Zmod_setoid {n : ℤ} : setoid ℤ :=
{ r := int.modeq n,
  iseqv := ⟨int.modeq.refl, @int.modeq.symm n, @int.modeq.trans n⟩ }

example : setoid ℤ := by apply_instance -- fails

[Kevin Buzzard]

I'm not sure that I understand how parametrized instances work.

[Kevin Buzzard]

import data.int.modeq

instance Zmod_setoid {n : ℤ} : setoid ℤ :=
{ r := int.modeq n,
  iseqv := ⟨int.modeq.refl, @int.modeq.symm n, @int.modeq.trans n⟩ }

def Zmod (n : ℤ) : Type := quotient (@Zmod_setoid n)

#check (⟦3⟧ : Zmod 5) -- failed to synthesize type class instance for setoid ℤ

[Kevin Buzzard]

I'm even less sure now

[Kevin Buzzard]

#check (⟦(3 : ℤ)⟧ : Zmod 5 gives

[Kevin Buzzard]

⁇ : Zmod 5 for information check result (in green)

[Kevin Buzzard]

and fails to synthesize the instance

[Simon Hudon]

Try:

import data.int.modeq

@[reducible]
def Zmod (n : ℤ) : Type := ℤ

instance Zmod_setoid {n : ℤ} : setoid (Zmod n) :=
{ r := int.modeq n,
  iseqv := ⟨int.modeq.refl, @int.modeq.symm n, @int.modeq.trans n⟩ }

example {n : ℤ} : setoid (Zmod n) := by apply_instance

#check ⟦ (3 : Zmod 5) ⟧

[Simon Hudon]

The problem is that instance inference is only working with ℤ (in your example) to find a setoid instance. It's not enough information to infer the n parameter. Now, I added a synonym for ℤ which provides that information.

[Kevin Buzzard]

import data.int.modeq

@[reducible]
def Z_aux (n : ℤ) : Type := ℤ

instance Zmod_setoid {n : ℤ} : setoid (Z_aux n) :=
{ r := int.modeq n,
  iseqv := ⟨int.modeq.refl, @int.modeq.symm n, @int.modeq.trans n⟩ }

example {n : ℤ} : setoid (Z_aux n) := by apply_instance

def Zmod (n : ℤ) : Type := quotient (@Zmod_setoid n)

#check (⟦ 3 ⟧ : Zmod 5) -- 3 is interpreted as being in Z_aux 5 and this works

private def add_aux {n : ℤ} (a b : Zmod n) : Zmod n :=
quotient.lift_on₂ a b (λ a b, (⟦a + b⟧ : Zmod n)) sorry -- no error yet

[Kevin Buzzard]

As a mathematician I'm a bit uneasy about having a thing which is Z but which is called Zmod n

[Kevin Buzzard]

so I renamed it Z_aux, but your trick is excellent all the same :-)

[Kevin Buzzard]

I was worried the check would fail because Lean wouldn't push 3 into Z_aux 5

[Kevin Buzzard]

setoid is a class and this is in core lean.

[Kevin Buzzard]

I think this means that it's quite hard to have more than one instance of a setoid structure on a given type

[Kevin Buzzard]

Simon's trick shows how to get around this, by making lots of types, one for each structure

[Kevin Buzzard]

it's evil :-)

[Simon Hudon]

In general, if you need more than one instance of a class for a given type, it should make you suspicious

[Mario Carneiro]

it's also a good way to handle the multiple rings problem

[Kevin Buzzard]

yes

[Kevin Buzzard]

I don't think I'd seen it before

[Simon Hudon]

But you can also name the quotient instead of Z:

[Simon Hudon]

instance Zmod_setoid (n : ℤ) : setoid (Zmod n) :=
{ r := int.modeq n,
  iseqv := ⟨int.modeq.refl, @int.modeq.symm n, @int.modeq.trans n⟩ }

def Zmod' (n : ℤ) : Type := quotient (Zmod_setoid n)

#check (⟦ 3 ⟧ : Zmod' 5)

[Simon Hudon]

And if you equip Zmod' 5 with has_one, has_zero and has_add, #check (3 : Zmod' 5) should work

[Kevin Buzzard]

variables (Y : Type) [has_add Y] [has_one Y]
#check (3 : Y)

[Kevin Buzzard]

no need for zero ;-)

[Simon Hudon]

Even better!

[Kevin Buzzard]

sort of...

[Kevin Buzzard]

:-)

[Simon Hudon]

Simon's trick shows how to get around this, by making lots of types, one for each structure

it's evil :-)

I disagree. If you want the structure to be inferred implicitly, the information must be somewhere. The alternative is to have a different + / * operator for each one of those structures: +_mod_5 / *_mod_5. That would be ugly and evil!

[Kevin Buzzard]

If setoid were a structure rather than a class, do you think Chris' code would be OK?

[Kevin Buzzard]

The quotient knows the equivalence relation, and the information distinguishing the quotient types is in the equivalence relation

[Kevin Buzzard]

variables (Y : Type) [has_add Y] [has_one Y]

[Kevin Buzzard]

I think I just defined the positive integers :-)

[Simon Hudon]

Yeah I think that would be good. Maybe rather than making setoid a structure, just make Zmod_setoid into a definition because it is not unique

[Kevin Buzzard]

then you'll lose access to the \[[ notation

[Kevin Buzzard]

this goes back to the thing I was talking about earlier

[Kevin Buzzard]

once setoid is deemed to be a class

[Kevin Buzzard]

then pretty much whenever it's mentioned in a definition or theorem, it's in a square bracket

[Simon Hudon]

I think I just defined the positive integers :-)

That looks like the Church numerals

[Simon Hudon]

Sorry, I kind of jumped in the middle your conversation

[Kevin Buzzard]

so it's a pain to work with if you decide not to use the type class inference system

[Simon Hudon]

Yes, I see now

[Kevin Buzzard]

As Mario points out, it's the same sort of thing as the (hypothetical but not completely impossible) possibility of having more than one ring structure on a type

[Simon Hudon]

Is it ever necessary to have it inferred?

[Kevin Buzzard]

it's just inconvenient not to have it inferred, if Lean wants it to be inferred.

[Kevin Buzzard]

That was what I discovered when I had a commutative ring earlier -- if you use the type class inference system then you also automatically have a ring, an additive group, and a whole bunch of other things

[Kevin Buzzard]

and if you don't then you're stuck making all of these yourself

[Simon Hudon]

What if you skip \[[ and instead rely on coe to convert integers to Zmod and has_one / has_add to use numerals?

[Kevin Buzzard]

I guess the proof of the pudding would be in the eating

[Kevin Buzzard]

I was fine explictly writing my proofs that various types were commutative rings up to a point

[Kevin Buzzard]

and then it got inconvenient and then I figured out how to use type class inference.

[Kevin Buzzard]

Those things aren't quite church numerals

[Kevin Buzzard]

as far as I can see at least

[Kevin Buzzard]

but they do have a similar flavour

[Kevin Buzzard]

def hudon_numeral := Π (Y : Type), (Y → Y → Y) → Y → Y
def one : hudon_numeral := λ Y h_add h_one, h_one
def two : hudon_numeral := λ Y h_add h_one, h_add h_one h_one

[Kevin Buzzard]

etc

[Simon Hudon]

Ah yes I see! 0 is missing and Church encodes succ rather than add

[Chris Hughes]

Any advice about how to deal with this issue?

def Zmod_fintype {n : ℤ} (hn : n ≠ 0) : fintype (Zmod n) :=
fintype.of_equiv _ (equiv_fin hn).symm

I can't make this an instance, because it's only true if n ≠ 0

[Kevin Buzzard]

Why not let n be in pnat (positive integers) instead of Z?

[Chris Hughes]

Probably the best thing. Alternative is to define the equivalence relation differently in the case n = 0, so Zmod 0 is a fintype.

[Chris Hughes]

Then there's also the issue of proving it's a field in the case prime p

[Kenny Lau]

fintype (Zmod $ nat.succ m)

[Chris Hughes]

n is an int currently

[Kevin Buzzard]

I have another type class inference issue and this one is rather frustrating.

[Kevin Buzzard]

I am making a definition, so I really want to stay in term mode.

[Kevin Buzzard]

I wrote down something which should work

[Kevin Buzzard]

and Lean complained that it could not prove that a certain composition of two maps was a ring homomorphism.

[Kevin Buzzard]

So I tried again in tactic mode

[Kevin Buzzard]

(each map is a ring hom, with an instance, and the composite of two ring homs is a ring hom, and this is an instance too, so it should work)

[Kevin Buzzard]

and in tactic mode I have managed to get Lean into a state where the goal is to show that the map is a ring hom (I did this using refine)

[Kevin Buzzard]

and apply_instance fails

[Kevin Buzzard]

but show ([cut and paste the goal])

[Kevin Buzzard]

followed by apply_instance succeeds.

[Kevin Buzzard]

In term mode, the proof should look like this:

[Kevin Buzzard]

to_fun := away.extend_map_of_im_unit ((of_comm_ring (away f) _) ∘ (of_comm_ring R (powers f))) H,

[Kevin Buzzard]

(it's some part of a structure I'm defining)

[Kevin Buzzard]

but away.extend_map_of_im_unit requires that the map (a composite of two ring homs) is a ring hom

[Kevin Buzzard]

So here it feels to me like Lean is not working as well as it could be.

[Kevin Buzzard]

But I don't have any feeling as to why not

[Kevin Buzzard]

If I set pp.all true I can see that the show command is doing something

[Kevin Buzzard]

but unfortunately these are complex maps defined between complex rings

[Kevin Buzzard]

and so I am having trouble figuring out what I have done wrong

[Kevin Buzzard]

and whether it's Lean's fault or mine

[Kevin Buzzard]

Here are the two (rather lengthy) goals.

[Kevin Buzzard]

https://gist.github.com/kbuzzard/a09dc87e290c0497db65c4c702b37c2f

[Kevin Buzzard]

Just to be clear: my problem is that I need to prove something in term mode because it's part of a definition. Type class inference fails me and I don't know why. In tactic mode I can make type class inference succeed.

[Kevin Buzzard]

I could go down the awful route of adding @s and explicitly chasing up the proof, but I would rather let type class inference do its job properly and just add hints.

[Simon Hudon]

if it's a proof (i.e. it's type is a Prop) I think you can use a tactic:

to_fun :=
have local_proof : something, by ...,
definition_using_local_proof,

[Simon Hudon]

To my memory, local_proof gets compiled to an auxiliary definition / lemma and you'll have to_fun := definition_using_local_proof with a reference to that auxiliary definition (which will not be displayed because of proof erasure).

[Kevin Buzzard]

Unfortunately this fails, because my local proof is not a proof of the correct thing.

[Kevin Buzzard]

My local proof is a proof of the second monstrous expression in the gist, which can be proved by type class inference.

[Kevin Buzzard]

I have two maps phi and psi

[Kevin Buzzard]

and I can prove is_ring_hom (phi comp psi) with apply_instance

[Kevin Buzzard]

but when I write foo (phi comp psi)

[Kevin Buzzard]

for some function foo which needs (phi comp psi) to be a ring hom

[Kevin Buzzard]

then type class inference fails

[Kevin Buzzard]

well, this is my understanding of the situation.

[Kevin Buzzard]

I tried to create a MWE but I could not reproduce the problem in a controlled environment

[Simon Hudon]

What do you know about phi comp psi that makes it a is_ring_hom? Could you create:

instance [... some context about (phi comp psi) ...] : is_ring_hom (phi comp psi) := ...

right before the structure you're trying to define?

[Johan Commelin]

phi and psi are both ring homs themselves, if I understand Kevin correctly

[Kevin Buzzard]

Type class inference will make it a ring hom

[Kevin Buzzard]

Here is a very clear explanation of the situation I find myself in:

[Kevin Buzzard]

  to_fun := have XXX : is_ring_hom
    (of_comm_ring (away f) (powers (of_comm_ring R (powers f) g)) ∘ (of_comm_ring R (powers f)) )
    := by apply_instance,
  away.extend_map_of_im_unit
              (of_comm_ring (away f) (powers (of_comm_ring R (powers f) g)) ∘ (of_comm_ring R (powers f)))
              sorry,

[Kevin Buzzard]

(the sorry at the end is just to save you from having to look at another term)

[Kevin Buzzard]

So this definition fails

[Kevin Buzzard]

there's a red squiggle under away

[Kevin Buzzard]

and the error is

[Kevin Buzzard]

failed to synthesize type class instance for
R : Type u,
_inst_1 : comm_ring R,
f g : R,
H : Spec.D' g ⊆ Spec.D' f,
XXX : is_ring_hom (of_comm_ring (away f) (powers (of_comm_ring R (powers f) g)) ∘ of_comm_ring R (powers f))
⊢ is_ring_hom (of_comm_ring (away f) (powers (of_comm_ring R (powers f) g)) ∘ of_comm_ring R (powers f))

[Kevin Buzzard]

Note that the goal looks exactly like XXX

[Kevin Buzzard]

and what is even more frustrating is that the goal and XXX were both created in the same way

[Kevin Buzzard]

by typing the same string twice

[Kevin Buzzard]

namely the string which appears in the goal

[Kevin Buzzard]

however if I set pp.all true

[Kevin Buzzard]

then XXX and the goal expand into the two distinct, but defeq, monsters

[Kevin Buzzard]

and note that XXX was proved by type class inference

[Kevin Buzzard]

What I need to understand to proceed, I think, is that I'd like to understand how Lean can unfold the same string in two different ways in these two situations.

[Kevin Buzzard]

I am scared to use a let to define the function, because I am scared it will cause me problems further down the line

[Kevin Buzzard]

I am trying to prove that a map is a bijection and if I do something screwy when defining the map then I'm worried I won't be able to use it later

[Simon Hudon]

The problem might be in the two terms that are defeq but not identical. Cosmetic differences in the syntax can take the instance inference process in a different direction. Do you think you can make them exactly identical?

[Kevin Buzzard]

this is exactly what I cannot do

[Kevin Buzzard]

because as you can see from my term

[Kevin Buzzard]

I created XXX and the input to away.extend_map_of_im_unit by typing exactly the same string of characters.

[Simon Hudon]

including the @?

[Kevin Buzzard]

aah I see

[Kevin Buzzard]

I can try to be more persuasive

[Simon Hudon]

It will probably not be concise but we can work on that once we know it works

[Kevin Buzzard]

by the way, am I right in thinking that I should not be using let in a defintion of a map?

[Kevin Buzzard]

Many thanks Simon

[Kevin Buzzard]

Explicitly telling Lean what the type of the composition was has solved the problem

[Kevin Buzzard]

Thanks a lot for persevering with this very awkward problem which was completely blocking me.

[Kevin Buzzard]

Many thanks indeed.

[Simon Hudon]

You're very welcome :)

[Simon Hudon]

by the way, am I right in thinking that I should not be using let in a defintion of a map?

I would avoid it especially if you're going to prove stuff about it. Maybe you're asking about the ùmathlibù style though. I haven't seen that mentioned anywhere but facilitating proofs using your definitions is likely to make you popular with the mathlib team.

[Mario Carneiro]

Have you tried using by exact in your definition? There is nothing wrong with using tactics in the definition of a term, although you may need to be more conscientious about junk added to your term by lean (or use by clean)

[Mario Carneiro]

there is not a problem with using let or other techniques in defining a complicated function, although you will probably want to write simp lemmas providing your interface so you don't need to rely on definitional expansion

[Kevin Buzzard]

Gaargh I have another one. Here's a MWE.

[Kevin Buzzard]

import algebra.ring
universes u v w uu

structure is_unique_R_alg_hom {R : Type u} {α : Type v} {β : Type w} [comm_ring R] [comm_ring α] [comm_ring β]
(sα : R → α) (sβ : R → β) (f : α → β) [is_ring_hom sα] [is_ring_hom sβ] [is_ring_hom f] :=
(R_alg_hom : sβ = f ∘ sα)
(is_unique : ∀ g : α → β, is_ring_hom g → sβ = g ∘ sα → g = f)

lemma comp_unique {R : Type u} {α : Type v} {β : Type w} {γ : Type uu}
  [comm_ring R] [comm_ring α] [comm_ring β] [comm_ring γ]
  (sα : R → α) (sβ : R → β) (sγ : R → γ) (f : α → β) (g : β → γ) (h : α → γ)
  [is_ring_hom sα] [is_ring_hom sβ] [is_ring_hom sγ] [is_ring_hom f] [is_ring_hom g] [is_ring_hom h] :
  is_unique_R_alg_hom sα sβ f → is_unique_R_alg_hom sβ sγ g → is_unique_R_alg_hom sα sγ h → g ∘ f = h :=
λ Uf Ug Uh, Uh.is_unique (g ∘ f : α → γ) (by apply_instance) (by simp [Uf.R_alg_hom,Ug.R_alg_hom])

[Kevin Buzzard]

Note the by apply_instance on the last line!

[Kevin Buzzard]

If I replace that with _ then I get

[Kevin Buzzard]

don't know how to synthesize placeholder
context:
R : Type u,
α : Type v,
β : Type w,
γ : Type uu,
_inst_1 : comm_ring R,
_inst_2 : comm_ring α,
_inst_3 : comm_ring β,
_inst_4 : comm_ring γ,
sα : R → α,
sβ : R → β,
sγ : R → γ,
f : α → β,
g : β → γ,
h : α → γ,
_inst_5 : is_ring_hom sα,
_inst_6 : is_ring_hom sβ,
_inst_7 : is_ring_hom sγ,
_inst_8 : is_ring_hom f,
_inst_9 : is_ring_hom g,
_inst_10 : is_ring_hom h,
Uf : is_unique_R_alg_hom sα sβ f,
Ug : is_unique_R_alg_hom sβ sγ g,
Uh : is_unique_R_alg_hom sα sγ h
⊢ is_ring_hom (g ∘ f)

[Kevin Buzzard]

How does type class inference work? Is _ something other than by apply_instance?

[Mario Carneiro]

yes

[Kevin Buzzard]

I guess I just proved that :-)

[Mario Carneiro]

_ only does unification

[Mario Carneiro]

when it is omitted and the binder type is [tc A] it uses typeclass inference

[Patrick Massot]

You need is_unique_R_alg_hom.is_unique to take a square bracket argument

[Mario Carneiro]

by apply_instance does the same thing but manually

[Kevin Buzzard]

So "don't know how to synthesize placeholder" -- what did it try??

[Mario Carneiro]

unification

[Mario Carneiro]

and nothing else

[Kevin Buzzard]

I don't know what unification means

[Kevin Buzzard]

isn't that something to do with finding something of the right type?

[Kevin Buzzard]

Oh

[Kevin Buzzard]

I remember

[Kevin Buzzard]

it means "I will call this ?m_6"

[Kevin Buzzard]

"and sort it out later"

[Kevin Buzzard]

Thanks Patrick:

[Kevin Buzzard]

structure is_unique_R_alg_hom {R : Type u} {α : Type v} {β : Type w} [comm_ring R] [comm_ring α] [comm_ring β]
(sα : R → α) (sβ : R → β) (f : α → β) [is_ring_hom sα] [is_ring_hom sβ] [is_ring_hom f] :=
(R_alg_hom : sβ = f ∘ sα)
(is_unique : Π (g : α → β) [is_ring_hom g], sβ = g ∘ sα → g = f)

lemma comp_unique {R : Type u} {α : Type v} {β : Type w} {γ : Type uu}
  [comm_ring R] [comm_ring α] [comm_ring β] [comm_ring γ]
  (sα : R → α) (sβ : R → β) (sγ : R → γ) (f : α → β) (g : β → γ) (h : α → γ)
  [is_ring_hom sα] [is_ring_hom sβ] [is_ring_hom sγ] [is_ring_hom f] [is_ring_hom g] [is_ring_hom h] :
  is_unique_R_alg_hom sα sβ f → is_unique_R_alg_hom sβ sγ g → is_unique_R_alg_hom sα sγ h → g ∘ f = h :=
λ Uf Ug Uh, Uh.is_unique (g ∘ f : α → γ) (by simp [Uf.R_alg_hom,Ug.R_alg_hom])

[Patrick Massot]

You're welcome

[Kevin Buzzard]

I have abstracted a standard trick :-)

[Kevin Buzzard]

I see, I was not even asking type class inference to do its job here. So this one is my bad.

[Patrick Massot]

Indeed

[Kevin Buzzard]

How do I do this one:

[Kevin Buzzard]

structure foo :=
(bar : ∀ (α : Type) [group α] (a b c : α), Prop)

definition X : foo :=
{bar := λ α Hα a b c, (mul_assoc a b c)}

[Kevin Buzzard]

Can I use type class inference here?

[Kenny Lau]

you need a prop

[Kenny Lau]

that isn't a prop

[Kenny Lau]

structure foo :=
(bar : ∀ (α : Type) [group α] (a b c : α), Prop)

definition X : foo :=
{bar := λ g Hg a b c, by letI := Hg; from mul_assoc a b c}

[Kenny Lau]

invalid type ascription, term has type
  a * b * c = a * (b * c) : Prop
but is expected to have type
  Prop : Type
state:
g : Type,
Hg : group g,
a b c : g,
_inst : group g := Hg
⊢ Prop

[Kevin Buzzard]

I have some type mismatch error, I think I have more than one problem here

[Kenny Lau]

which is?

[Kenny Lau]

structure foo :=
(bar : ∀ (α : Type) [group α] (a b c : α), Prop)

definition X : foo :=
{ bar := λ g Hg a b c, @mul_assoc _
    (@monoid.to_semigroup g $ @group.to_monoid g Hg) a b c }

[Kevin Buzzard]

mul_assoc a b c isn't a prop, it's a proof.

[Kevin Buzzard]

I know I can do it using @, I want to do it using type class inference

[Kevin Buzzard]

I want to understand how to make type class inference work, not to understand how to work around it (which I already know)

[Kevin Buzzard]

structure foo :=
(bar : ∀ (α : Type) [group α] (a : α), 1 * a = a)

definition X : foo :=
{bar := λ α Hα a, group.one_mul a}

[Kevin Buzzard]

failed to synthesize type class instance for
α : Type,
Hα : group α,
a : α
⊢ group α

[Kenny Lau]

then just letI

[Kevin Buzzard]

Where do I put the letI?

[Kevin Buzzard]

I am in the middle of a structure

[Kenny Lau]

by letI := H\a; from group.one_mul a

[Kevin Buzzard]

What if I don't want to go into tactic mode because I am actually defining something?

[Kevin Buzzard]

What exactly are yuo suggesting?

[Kevin Buzzard]

definition X : foo :=
{bar := λ α Hα a, by letI := Hα; from group.one_mul a}

[Kevin Buzzard]

?

[Kenny Lau]

yes

[Kevin Buzzard]

7 errors

[Kevin Buzzard]

including "unknown identifier letI"

[Kevin Buzzard]

But even if we can get this to work

[Kenny Lau]

import anything from mathlib

[Kevin Buzzard]

I would rather just make type class inference work.

[Kenny Lau]

import algebra.group

structure foo :=
(bar : ∀ (α : Type) [group α] (a : α), 1 * a = a)

definition X : foo :=
{bar := λ α Hα a, by letI := Hα; from group.one_mul a}

#print X._proof_1

/-
theorem X._proof_1 : ∀ (α : Type) (Hα : group α) (a : α), 1 * a = a :=
λ (α : Type) (Hα : group α) (a : α), let _inst : group α := Hα in group.one_mul a
-/

[Kevin Buzzard]

?!

[Kenny Lau]

!?

[Kevin Buzzard]

which version of Lean are you using?

[Kevin Buzzard]

aah

[Kevin Buzzard]

I have no import

[Kevin Buzzard]

letI is some mathlib magic I guess

[Kenny Lau]

it is.

[Kenny Lau]

it is Mario's workaround of Leo's changes.

[Kenny Lau]

So it's in mathlib.

[Kevin Buzzard]

Well thank you for your answer, which kind of stinks

[Kevin Buzzard]

Your answer seems to indicate that [group \a] is useless in my structure

[Kevin Buzzard]

i.e. it didn't insert H\a into the type class inference system anyway

[Kevin Buzzard]

but wait a minute, isn't this what Patrick told me to do earlier?

[Kenny Lau]

only typeclasses before the colon are inserted

[Kenny Lau]

that is Leo's changes

[Kevin Buzzard]

I am writing another localization interface by the way

[Kevin Buzzard]

rewriting your universal properties

[Kenny Lau]

heh

[Mario Carneiro]

you don't need to use letI, by exactI is the right solution for this application

[Kenny Lau]

aha

[Kevin Buzzard]

https://github.com/kbuzzard/lean-stacks-project/blob/master/src/localization_UMP.lean

[Kevin Buzzard]

I have finally battled through all my typeclass inference issues.

[Kevin Buzzard]

Kenny, I wrote an even better interface for localization

[Kevin Buzzard]

I put all the stuff which makes up the universal properties into one structure

[Kevin Buzzard]

is_unique_R_alg_hom

[Kevin Buzzard]

Mario, it's not quite mathlib-ready, but one day this should probably be in mathlib in some form if localization is in

[Kevin Buzzard]

because this file makes the localization stuff usable without ever having to touch the quotient type itself

[Kevin Buzzard]

I know because I'm using localization all the time in my schemes work and this work is what led me to the formalisation and the instances in the file I just linked to

[Kevin Buzzard]

There's one more instance of the structure which is commonly used which we still have to fill in

[Mario Carneiro]

Shouldn't comp_unique read something like is_unique_R_alg_hom sα sβ f → is_unique_R_alg_hom sβ sγ g → is_unique_R_alg_hom sα sγ (g ∘ f)?

[Mario Carneiro]

by rw ←HR.symm

what?

[Patrick Massot]

Nice one!

[Patrick Massot]

Kevin, is there is reason why your file doesn't have open classical towards the top? You write classical. quite a lot

[Kevin Buzzard]

Shouldn't comp_unique read something like is_unique_R_alg_hom sα sβ f → is_unique_R_alg_hom sβ sγ g → is_unique_R_alg_hom sα sγ (g ∘ f)?

No. That's not even true in general. The standard use of the universal property to prove that certain maps are isomorphisms is via the following argument: "We are given maps X-> Y and Y -> X. The given map from X to Y is the only map X -> Y with a certain property (e.g. being an R-algebra map). The map given Y -> X is the only map Y -> X with a certain property. Composition of two maps with the property has the property. The identity map X -> X is the only map X -> X with the property. Hence X -> Y -> X is the identity map by comp_unique. Furthermore the identity map Y -> Y is the only map Y -> Y with the property. Hence Y -> X -> Y is also the identity. So X isomorphic to Y".

[Kevin Buzzard]

The reason your suggestion is not true is that there could be plenty of maps from A to C which don't factor through B.

[Kevin Buzzard]

I don't open classical because I typically don't open anything. I am very bad at namespaces in general. A whole bunch of my code is incorrectly sitting in the root namespace. The whole thing needs a clear-up.

[Kevin Buzzard]

by rw ←HR.symm

what?

ha ha. I think it was getting late at that point. This was kind of stupid. I had that composition of f and g was h, but needed to show forall x, f (g x) = h xand I felt that this should just be an application of a standard lemma but I couldn't find it. So I just wrote "lambda x, by rw (proof that f circ g = h)" a few times, but then something was the other way round so I switched it and then something else was the other way around so I had to switch it back

[Kevin Buzzard]

Shouldn't comp_unique read something like is_unique_R_alg_hom sα sβ f → is_unique_R_alg_hom sβ sγ g → is_unique_R_alg_hom sα sγ (g ∘ f)?

Maybe you'll like this one:

[Kevin Buzzard]

theorem unique_R_of_unique_R_of_unique_Rloc {R : Type u} {α : Type v} {β : Type w} {γ : Type uu}
[comm_ring R] [comm_ring α] [comm_ring β] [comm_ring γ]
(sα : R → α) [is_ring_hom sα] (fαβ : α → β) [is_ring_hom fαβ] (fβγ : β → γ) [is_ring_hom fβγ] :
is_unique_R_alg_hom sα (fβγ ∘ fαβ ∘ sα) (fβγ ∘ fαβ)
→ is_unique_R_alg_hom fαβ (fβγ ∘ fαβ) fβγ
→ is_unique_R_alg_hom (fαβ ∘ sα) (fβγ  ∘ fαβ ∘ sα) (fβγ) :=

[Kevin Buzzard]

If there's a unique R-alg hom from alpha to gamma and a unique alpha-alg hom from beta to gamma then there's a unique R-alg hom from beta to gamma (and it's the same map)

[Kevin Buzzard]

(oh, the R-alg hom from alpha to gamma must be the composite of a given map alpha -> beta and our given alpha-alg map from beta to gamma)

[Johan Commelin]

This feels like you want to hit it with Yoneda and reduce it to some basic set-theoretic fact... But that is only instinct

[Johan Commelin]

You're looking at both R-alg-homs and alpha-alg-homs... so maybe it is not that straightforward actually

[Kenny Lau]

don't get him started on alpha

[Johan Commelin]

What do you mean?

[Johan Commelin]

There is alpha's everywhere in his code

[Johan Commelin]

I was actually surprised when I saw that

[Kenny Lau]

don't say "alpha" and any mathematical object in the same sentence in front of kevin buzzard

[Johan Commelin]

But he just did that himself!

[Kenny Lau]

it doesn't matter

[Kevin Buzzard]

Did you notice that when we were doing groups earlier I used alpha to be a group homomorphism just to wind up the CS folk?

[Kevin Buzzard]

alpha : G to H

[Kevin Buzzard]

The reason I am using alpha for a ring

[Kevin Buzzard]

is that the most important ring is called R

[Kevin Buzzard]

and then I needed three more

[Kevin Buzzard]

but I couldn't face S T U

[Kevin Buzzard]

so I thought alpha beta gamma was OK

[Kevin Buzzard]

begin
  intros Hαβ Hβγ,
  constructor,refl,
  intros gβγ Hgβγ H1,
  have Hαγ : fβγ ∘ fαβ = gβγ ∘ fαβ,
    exactI (Hαβ.is_unique (gβγ ∘ fαβ) H1).symm,
  exactI Hβγ.is_unique gβγ Hαγ,
end

[Kevin Buzzard]

That was the proof

[Reid Barton]

Haha, I seriously thought up to now that an "alpha-alg-hom" was a map of rings equipped with some fancy extra additional structure, like $\lambda$-rings or divided power rings or something.

[Kevin Buzzard]

no, it's an alpha-algebra hom :-)

[Kevin Buzzard]

YOU SEE YOU CS PEOPLE

[Kevin Buzzard]

THE MOMENT YOU CALL RINGS ALPHA

[Kevin Buzzard]

WE GET THINGS LIKE THIS HAPPENING

[Johan Commelin]

wow, that was pretty α-male

[Kevin Buzzard]

Here's today's type class inference issue:

[Kevin Buzzard]

theorem canonical_iso_is_canonical_hom {R : Type u} [comm_ring R] {f g : R} (H : Spec.D' g ⊆ Spec.D' f) :
let gbar := of_comm_ring R (powers f) g in
let sα : R → loc (away f) (powers gbar) :=
  of_comm_ring (away f) (powers gbar) ∘ of_comm_ring R (powers f) in
let sγ := (of_comm_ring R (non_zero_on_U (Spec.D' g))) in
let H2 := (canonical_iso H).is_ring_hom in
is_unique_R_alg_hom sγ sα (canonical_iso H).to_fun := sorry

[Kevin Buzzard]

that won't run

[Kevin Buzzard]

but hopefully I can explain the issue

[Kevin Buzzard]

I am trying to prove is_unique_R_alg_hom sγ sα (canonical_iso H).to_fun

[Kevin Buzzard]

but the definition of is_unique_R_alg_hom expects H2 to be deduced from type class inference

[Kevin Buzzard]

and I've only managed to prove it the line before

[Kevin Buzzard]

so I can solve this with @

[Kevin Buzzard]

but given that it would then look like

[Kevin Buzzard]

...erm

[Kevin Buzzard]

even that didn't work

[Kevin Buzzard]

@is_unique_R_alg_hom _ _ _ _ _ _ sγ sα (canonical_iso H).to_fun _ _ H2

[Kevin Buzzard]

actually it did work, I now have an unrelated problem

[Kevin Buzzard]

So can I insert H2 into the type class inference system before I have even started my proof, because I need it to make my term typecheck?

[Kevin Buzzard]

I have got it working with @

[Kevin Buzzard]

theorem canonical_iso_is_canonical_hom {R : Type u} [comm_ring R] {f g : R} (H : Spec.D' g ⊆ Spec.D' f) :
let gbar := of_comm_ring R (powers f) g in
let sα : R → loc (away f) (powers gbar) :=
  of_comm_ring (away f) (powers gbar) ∘ of_comm_ring R (powers f) in
let sγ := (of_comm_ring R (non_zero_on_U (Spec.D' g))) in
let H2 := (canonical_iso H).is_ring_hom in
let H3 : is_ring_hom sα := by apply_instance in
let H4 : is_ring_hom sγ := by apply_instance in
@is_unique_R_alg_hom _ _ _ _ _ _ sγ sα (canonical_iso H).to_fun H4 H3 H2 := sorry

[Kevin Buzzard]

The first three lets are simply there to make the statement look clearer

[Kevin Buzzard]

the last three are there because type class inference asked for them all

[Reid Barton]

Change those last three lets to letI I think

[Kevin Buzzard]

letI doesn't work there

[Kevin Buzzard]

well, it doesn't work for me

[Kevin Buzzard]

It works in a proof

[Reid Barton]

Sorry, I just noticed this was in term mode

[Kevin Buzzard]

but this is before the proof

[Kevin Buzzard]

the issue is that we're before the colon

[Kevin Buzzard]

I think

[Reid Barton]

But I think by letI ...; exact is fine

[Kevin Buzzard]

I have only seen letI after the colon

[Reid Barton]

Though, it does make me vaguely uneasy to put it in the theorem statement.

[Reid Barton]

theorem canonical_iso_is_canonical_hom {R : Type u} [comm_ring R] {f g : R} (H : Spec.D' g ⊆ Spec.D' f) :
let gbar := of_comm_ring R (powers f) g in
let sα : R → loc (away f) (powers gbar) :=
  of_comm_ring (away f) (powers gbar) ∘ of_comm_ring R (powers f) in
let sγ := (of_comm_ring R (non_zero_on_U (Spec.D' g))) in
by letI H2 := (canonical_iso H).is_ring_hom; exact
is_unique_R_alg_hom sγ sα (canonical_iso H).to_fun := sorry

(untested, hopefully I deleted the right amount of stuff)

[Mario Carneiro]

Using letI in theorem types is fine, and by letI ...; exact or by exactI is the recommended way to introduce a typeclass thing from the context in term mode

[Chris Hughes]

Don't use let in the statement of a theorem.

[Kevin Buzzard]

Don't use let in the statement of a theorem.

This is easy to fix -- the let is in some sense for my own sanity.

[Mario Carneiro]

Note that haveI when used in a tactic doesn't actually produce a have term, the result is just like you would get if it were actually inferred by regular tc inference

[Mario Carneiro]

If in doubt, just #print the statement to make sure it doesn't look weird

[Kevin Buzzard]

I can't get the syntax right for this

[Kevin Buzzard]

having tried for 10 seconds

[Kevin Buzzard]

I need to insert three hypotheses into the type class inference box

[Kevin Buzzard]

and I don't understand the syntax of this by thing

[Kevin Buzzard]

theorem canonical_iso_is_canonical_hom {R : Type u} [comm_ring R] {f g : R} (H : Spec.D' g ⊆ Spec.D' f) :
let gbar := of_comm_ring R (powers f) g in
let sα : R → loc (away f) (powers gbar) :=
  of_comm_ring (away f) (powers gbar) ∘ of_comm_ring R (powers f) in
let sγ := (of_comm_ring R (non_zero_on_U (Spec.D' g))) in
let H2 := (canonical_iso H).is_ring_hom in
let H3 : is_ring_hom sα := by apply_instance in
let H4 : is_ring_hom sγ := by apply_instance in
@is_unique_R_alg_hom _ _ _ _ _ _ sγ sα (canonical_iso H).to_fun H4 H3 H2 :=

[Kevin Buzzard]

This works

[Kenny Lau]

good luck proving that

[Kevin Buzzard]

begin
letI := (canonical_iso H).is_ring_hom,
have H5 := unique_R_alg_from_loc (canonical_iso H).to_fun,
have H6 := (canonical_iso H).R_alg_hom.symm,
simp [H6] at H5,
exact H5,
end

[Kevin Buzzard]

done

[Kenny Lau]

ok you win

[Kevin Buzzard]

Now I have good interface

[Kevin Buzzard]

so all the proofs are "this canonical thing is canonical"

[Kevin Buzzard]

or "this canonical thing is unique"

[Kevin Buzzard]

or "this unique thing is canonical"

[Kevin Buzzard]

I was trying to put all three hypotheses into one "by"

[Kevin Buzzard]

but I don't understand the syntax

[Kevin Buzzard]

but I've got it working

[Kevin Buzzard]

theorem canonical_iso_is_canonical_hom {R : Type u} [comm_ring R] {f g : R} (H : Spec.D' g ⊆ Spec.D' f) :
let gbar := of_comm_ring R (powers f) g in
let sα : R → loc (away f) (powers gbar) :=
  of_comm_ring (away f) (powers gbar) ∘ of_comm_ring R (powers f) in
let sγ := (of_comm_ring R (non_zero_on_U (Spec.D' g))) in
by letI H2 := (canonical_iso H).is_ring_hom; exact
by letI H3 : is_ring_hom sα := by apply_instance; exact
by letI H4 : is_ring_hom sγ := by apply_instance; exact
@is_unique_R_alg_hom _ _ _ _ _ _ sγ sα (canonical_iso H).to_fun H4 H3 H2 :=

[Kevin Buzzard]

I can't even parse that

[Kevin Buzzard]

and now the moment of truth...

[Kevin Buzzard]

wooah

[Kevin Buzzard]

stop everything

[Kevin Buzzard]

lean has silently crashed

[Kevin Buzzard]

OK great, when I restart Lean it just quietly exits

[Kevin Buzzard]

Restarting VS Code and I am back up and running

[Kevin Buzzard]

and it doesn't work after all

[Kevin Buzzard]

theorem canonical_iso_is_canonical_hom {R : Type u} [comm_ring R] {f g : R} (H : Spec.D' g ⊆ Spec.D' f) :
let gbar := of_comm_ring R (powers f) g in
let sα : R → loc (away f) (powers gbar) :=
  of_comm_ring (away f) (powers gbar) ∘ of_comm_ring R (powers f) in
let sγ := (of_comm_ring R (non_zero_on_U (Spec.D' g))) in
by letI H2 := (canonical_iso H).is_ring_hom;
letI H3 : is_ring_hom sα := by apply_instance;
letI H4 : is_ring_hom sγ := by apply_instance; exact
@is_unique_R_alg_hom _ _ _ _ _ _ sγ sα (canonical_iso H).to_fun H4 H3 H2 :=

doesn't work

[Kevin Buzzard]

It's not a problem because my multi-let @ solution works

[Kevin Buzzard]

I'll construct a MWE. I think this is just a syntax thing

[Kevin Buzzard]

gaargh it's not a syntax thing, my MWE is too minimal and strings of by letI ...; exact work fine

[Kevin Buzzard]

My by apply_instance proofs seem to be failing when wrapped up in the outer by

[Kevin Buzzard]

I am torn between giving up and constructing a MWE

[Kenny Lau]

lemme help you

[Kenny Lau]

give up.

[Kevin Buzzard]

OK

[Kevin Buzzard]

thanks

[Kenny Lau]

no probs

[Mario Carneiro]

Your letI : ... := by apply_instance lines are redundant. If the typeclass system can already find it, there's no reason to add it to the typeclass system. Unless you are trying to limit search depth?

[Mario Carneiro]

Also I recommend haveI over letI when possible. The only time you need letI is if you are unfolding the exact definition of the inferred ring or whatever later on in the same proof

[Patrick Massot]

About type classes, let me quickly share https://gist.github.com/PatrickMassot/0d28b74be6f7bc9c0814a87393c91663 It's a draft of documentation of something that took me an embarrassingly long time to understand (I don't say it's directly related to your issues, it's only general knowledge about type class magic)

[Mario Carneiro]

I think the ..prod.has_op on the last instance is unnecessary

[Mario Carneiro]

it is inferred if you don't specify

[Patrick Massot]

oooh

[Patrick Massot]

that's even better

[Patrick Massot]

How does this new magic trick work?

[Patrick Massot]

This file is all about understanding more magic

[Mario Carneiro]

The comm_magma.mk structure constructor has the to_has_op parent field as instance implicit, and in structure notation that translates to an optional field

[Mario Carneiro]

same with anonymous constructor notation, you could write it as just ⟨proof of commutativity⟩ instead of {op_comm := proof of commutativity}

[Kevin Buzzard]

Today's typeclass tale of woe:

[Kevin Buzzard]

import data.equiv
universes u v w u' v' w'
variables {α : Type u} {β : Type v} {γ : Type w} {α' : Type u'} {β' : Type v'} {γ' : Type w'}

structure canonically_isomorphic_add_group_homs (Cα : equiv α α') (Cβ : equiv β β') (f : α → β) (f' : α' → β')
[add_group α] [add_group β] [add_group α'] [add_group β']
[is_group_hom f] [is_group_hom f']
:= sorry

[Kevin Buzzard]

failed to synthesize type class instance for
α : Type u,
β : Type v,
α' : Type u',
β' : Type v',
Cα : α ≃ α',
Cβ : β ≃ β',
f : α → β,
f' : α' → β',
_inst_1 : add_group α,
_inst_2 : add_group β,
_inst_3 : add_group α',
_inst_4 : add_group β',
_inst_5 : is_group_hom f
⊢ group β'

[Kevin Buzzard]

dammit

[Kevin Buzzard]

import data.equiv
universes u v w u' v' w'
variables {α : Type u} {β : Type v} {γ : Type w} {α' : Type u'} {β' : Type v'} {γ' : Type w'}

structure canonically_isomorphic_add_group_homs (Cα : equiv α α') (Cβ : equiv β β') (f : α → β) (f' : α' → β')
[Hα : add_group α] [Hβ : add_group β] [add_group α'] [Hβ' : add_group β']
[@is_group_hom α β Hα (by apply_instance) f] [@is_group_hom _ _ _ Hβ' f']
:= sorry

[Kevin Buzzard]

type mismatch at application
  is_group_hom
term
  Hα
has type
  add_group α
but is expected to have type
  group α

[Kevin Buzzard]

Damn you Lean

[Kevin Buzzard]

finding out how to turn an add_group to a group is exactly the kind of question which you should be good at.

[Kevin Buzzard]

thus saving me from having to remember the details about names of instances.

[Kevin Buzzard]

Why am I constantly running into type class inference issues @Sebastian Ullrich ? Is this sort of thing going to change in Lean 4, do you think?

[Kevin Buzzard]

I find the whole letI stuff both essential and extremely confusing

[Kevin Buzzard]

I probably need to write some letI docs

[Kevin Buzzard]

but am I right in thinking that letI is just a hack which we will be doing away with in Lean 4 as the amazing new type class inference system / syntax comes in?

[Kevin Buzzard]

I know that Mario has work hard to keep up with Leo's changes in the type class inference system

[Kevin Buzzard]

but that means that it's currently really confusing for end users

[Kevin Buzzard]

I believe in Lean so much

[Kevin Buzzard]

and I am really hoping for a beautiful solution.

[Kevin Buzzard]

Type class inference issues are stopping me from working right now.

[Kevin Buzzard]

variable (α : Type)
lemma to_group [H : add_group α] : group α := by apply_instance

[Kevin Buzzard]

tactic.mk_instance failed to generate instance for
  group α
state:
α : Type,
H : add_group α
⊢ group α

[Sebastian Ullrich]

There are no plans to change class inference for Lean 4. On the other hand, lifting the distinction between group and add_group is the primary motivation behind refactoring the algebraic hierarchy.

[Kenny Lau]

but the algebraic hierarchy also has its own problems, right

[Kenny Lau]

Today's typeclass tale of woe:

look, I already wrote you an is_add_group_hom

[Kevin Buzzard]

Oh, I see, I am an idiot. Lean regards the add_group hierarchy as completely different to, the group hierarchy. I have mixed my hierarchies without noticing

[Kevin Buzzard]

The reason I have made this mistake

[Kevin Buzzard]

is that the two heirarchies are canonically isomorphic

[Kevin Buzzard]

and indeed there is a unique canonical isomorphism in each direction

[Kevin Buzzard]

however the type class inference procedure might not use these canonical isomorphisms

[Kevin Buzzard]

because neither of the hierarchies is "better" than the other one

[Kevin Buzzard]

so it would be asymmetric to let type class inference move from one to the other

[Kevin Buzzard]

and there is a risk of diamonds if we let it move between them freely

[Kevin Buzzard]

On the other hand, to a mathematician, they are the same object

[Kevin Buzzard]

canonical isomorphism is different to type class resolution

[Kevin Buzzard]

and I was applying canonical isomorphism

[Johan Commelin]

Does this mean I introduced a diamond:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
subset.submodule 𝔥
inferred
lie_algebra.to_module ↥𝔥

[Johan Commelin]

So the context is as follows:

instance subset.lie_algebra {𝔥 : set 𝔤} [H : @is_lie_subalgebra R ri 𝔤 la 𝔥] :
lie_algebra R 𝔥 :=
{ bracket := λ x y, ⟨[x.1,y.1], is_lie_subalgebra.closed _ x.2 y.2⟩,
  left_linear := begin
    intro y,
    constructor,
    { intros x₁ x₂,
      apply subtype.eq,
      simp,
      apply (lie_algebra.left_linear y).add, -- FAILS
      sorry },
    { intros r x,
      apply subtype.eq,
      -- apply (lie_algebra.left_linear y).smul, FAILS
      sorry }
  end,
  right_linear := sorry,
  alternating := assume ⟨x,_⟩, subtype.eq $ lie_algebra.alternating _,
  Jacobi_identity := assume ⟨x,_⟩ ⟨y,_⟩ ⟨z,_⟩, subtype.eq $ lie_algebra.Jacobi_identity _ _ _,
  anti_comm := assume ⟨x,_⟩ ⟨y,_⟩, subtype.eq $ lie_algebra.anti_comm _ _,
}

[Johan Commelin]

How do I tell Lean that it should infer subset.submodule 𝔥, instead of lie_algebra.to_module ↥𝔥.

[Johan Commelin]

I really don't get why the type class system is tripping up in this case. After all, the first instance unifies completely. The second instance has one meta-variable in it (and rightly so, because it can't infer that 𝔥 is a lie_algebra since that is exactly what I'm trying to prove.

[Johan Commelin]

So it seems to me like the type class inference went down a wrong path, but still got convinced that it did a good job. (While the correct path is actually there in Lean.)

[Johan Commelin]

Aaaahhrg.....

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_bracket 𝔤 := @commutator_bracket ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6
[class_instances] (1) ?x_2 : comm_ring ?x_1 := ri
[class_instances] (1) ?x_4 : @lie_algebra R ?x_3 ri := la
[class_instances] (1) ?x_6 : ring 𝔤 := @nonneg_ring.to_ring ?x_7 ?x_8
[class_instances] (2) ?x_8 : nonneg_ring 𝔤 := @linear_nonneg_ring.to_nonneg_ring ?x_9 ?x_10
[class_instances] (1) ?x_6 : ring 𝔤 := @domain.to_ring ?x_7 ?x_8
[class_instances] (2) ?x_8 : domain 𝔤 := @linear_nonneg_ring.to_domain ?x_9 ?x_10
[class_instances] (2) ?x_8 : domain 𝔤 := @to_domain ?x_9 ?x_10
[class_instances] (3) ?x_10 : linear_ordered_ring 𝔤 := @linear_nonneg_ring.to_linear_ordered_ring ?x_11 ?x_12
[class_instances] (3) ?x_10 : linear_ordered_ring 𝔤 := @linear_ordered_field.to_linear_ordered_ring ?x_11 ?x_12
[class_instances] (4) ?x_12 : linear_ordered_field 𝔤 := @discrete_linear_ordered_field.to_linear_ordered_field ?x_13 ?x_14

[the list goes on and on...]

[Johan Commelin]

No stupid! It's a Lie algebra!

[Johan Commelin]

Everywhere in this file it has realised immediately that 𝔤 is a Lie algebra, and therefore has a bracket.

[Johan Commelin]

But somehow, here it messes up completely.

[Andrew Ashworth]

I notice type class inference issues are quite common in this chat. Maybe in the future a visualization aide would be helpful for people trying to debug the process

[Andrew Ashworth]

Actually for myself I don't know any better method to debug it than to write out the expression in full, and then in order work forwards as if I was doing the search by hand...

[Johan Commelin]

Right... which is not really what you would expect in this "computer-era"

[Andrew Ashworth]

you'd be disappointed in how much paper I go through while using a computerized theorem prover... or programming in general

[Mario Carneiro]

I have mentioned this in previous instance issues, but comm_ring ?x_1 is a bad sign in an instance trace, that will usually run away

[Mario Carneiro]

what is the type of commutator_bracket?

[Johan Commelin]

variables {S : Type*} [ring S]
instance commutator_bracket : has_bracket S := ⟨λ x y, x*y - y*x⟩

[Mario Carneiro]

That can't be right, the printout has six variables not two

[Mario Carneiro]

what does #print commutator_bracket show?

[Johan Commelin]

Anyway, my point is that 𝔤 is a Lie algebra, and by definition that means it extends has_bracket. So I would hope that Lean could figure this one out.

[Johan Commelin]

@[instance]
protected def commutator_bracket : Π {R : Type u_1} [ri : comm_ring R] {𝔤 : Type u_2} [la : lie_algebra R 𝔤] {S : Type u_3} [_inst_1 : ring S],
  has_bracket S :=
λ {R : Type u_1} [ri : comm_ring R] {𝔤 : Type u_2} [la : lie_algebra R 𝔤] {S : Type u_3} [_inst_1 : ring S],
  {bracket := λ (x y : S), x * y - y * x}

[Mario Carneiro]

there's your problem

[Johan Commelin]

Which is crazy...

[Johan Commelin]

It pulls in way too much stuff.

[Mario Carneiro]

did you include stuff at the top maybe?

[Mario Carneiro]

try defining it outside the section, this instance has nothing to do with lie algebras

[Johan Commelin]

Yes... thanks for catching that!

[Johan Commelin]

Hmm, I need to run. In fact, I should try to get rid of those include ri la, but that seems to be non-trivial.

[Johan Commelin]

Anyway, I'll be back later. AFK

[Kevin Buzzard]

import algebra.punit_instances

-- works fine
example : add_comm_group unit := by apply_instance

class G_module (G : Type*) [group G] (M : Type*)
  extends add_comm_group M, has_scalar G M :=
(id : ∀ m : M, (1 : G) • m = m)
(mul : ∀ g h : G, ∀ m : M, g • (h • m) = (g * h) • m)
(linear : ∀ g : G, ∀ m n : M, g • (m + n) = g • m + g • n)

example : add_comm_group unit := by apply_instance -- fails
/-
maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
state:
⊢ add_comm_group unit
-/

What did I do to deserve that? Is the class bad in some way?

[Kevin Buzzard]

set_option class.instance_max_depth 1000 doesn't fix it

[Kevin Buzzard]

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : add_comm_group unit := @G_module.to_add_comm_group ?x_1 ?x_2 ?x_3 ?x_4
[class_instances] (1) ?x_2 : group ?x_1 := @subtype.group ?x_5 ?x_6 ?x_7 ?x_8
[class_instances] (2) ?x_6 : group ?x_5 := @subtype.group ?x_9 ?x_10 ?x_11 ?x_12
[class_instances] (3) ?x_10 : group ?x_9 := @subtype.group ?x_13 ?x_14 ?x_15 ?x_16
[class_instances] (4) ?x_14 : group ?x_13 := @subtype.group ?x_17 ?x_18 ?x_19 ?x_20
[class_instances] (5) ?x_18 : group ?x_17 := @subtype.group ?x_21 ?x_22 ?x_23 ?x_24
[class_instances] (6) ?x_22 : group ?x_21 := @subtype.group ?x_25 ?x_26 ?x_27 ?x_28
[class_instances] (7) ?x_26 : group ?x_25 := @subtype.group ?x_29 ?x_30 ?x_31 ?x_32
[class_instances] (8) ?x_30 : group ?x_29 := @subtype.group ?x_33 ?x_34 ?x_35 ?x_36
[class_instances] (9) ?x_34 : group ?x_33 := @subtype.group ?x_37 ?x_38 ?x_39 ?x_40
[class_instances] (10) ?x_38 : group ?x_37 := @subtype.group ?x_41 ?x_42 ?x_43 ?x_44
[class_instances] (11) ?x_42 : group ?x_41 := @subtype.group ?x_45 ?x_46 ?x_47 ?x_48
[class_instances] (12) ?x_46 : group ?x_45 := @subtype.group ?x_49 ?x_50 ?x_51 ?x_52
[class_instances] (13) ?x_50 : group ?x_49 := @subtype.group ?x_53 ?x_54 ?x_55 ?x_56
[class_instances] (14) ?x_54 : group ?x_53 := @subtype.group ?x_57 ?x_58 ?x_59 ?x_60
[class_instances] (15) ?x_58 : group ?x_57 := @subtype.group ?x_61 ?x_62 ?x_63 ?x_64
[class_instances] (16) ?x_62 : group ?x_61 := @subtype.group ?x_65 ?x_66 ?x_67 ?x_68
[class_instances] (17) ?x_66 : group ?x_65 := @subtype.group ?x_69 ?x_70 ?x_71 ?x_72
[class_instances] (18) ?x_70 : group ?x_69 := @subtype.group ?x_73 ?x_74 ?x_75 ?x_76
[class_instances] (19) ?x_74 : group ?x_73 := @subtype.group ?x_77 ?x_78 ?x_79 ?x_80
[class_instances] (20) ?x_78 : group ?x_77 := @subtype.group ?x_81 ?x_82 ?x_83 ?x_84
[class_instances] (21) ?x_82 : group ?x_81 := @subtype.group ?x_85 ?x_86 ?x_87 ?x_88
[class_instances] (22) ?x_86 : group ?x_85 := @subtype.group ?x_89 ?x_90 ?x_91 ?x_92
[class_instances] (23) ?x_90 : group ?x_89 := @subtype.group ?x_93 ?x_94 ?x_95 ?x_96
[class_instances] (24) ?x_94 : group ?x_93 := @subtype.group ?x_97 ?x_98 ?x_99 ?x_100
[class_instances] (25) ?x_98 : group ?x_97 := @subtype.group ?x_101 ?x_102 ?x_103 ?x_104
[class_instances] (26) ?x_102 : group ?x_101 := @subtype.group ?x_105 ?x_106 ?x_107 ?x_108
[class_instances] (27) ?x_106 : group ?x_105 := @subtype.group ?x_109 ?x_110 ?x_111 ?x_112
[class_instances] (28) ?x_110 : group ?x_109 := @subtype.group ?x_113 ?x_114 ?x_115 ?x_116
[class_instances] (29) ?x_114 : group ?x_113 := @subtype.group ?x_117 ?x_118 ?x_119 ?x_120
[class_instances] (30) ?x_118 : group ?x_117 := @subtype.group ?x_121 ?x_122 ?x_123 ?x_124
[class_instances] (31) ?x_122 : group ?x_121 := @subtype.group ?x_125 ?x_126 ?x_127 ?x_128
[class_instances] (32) ?x_126 : group ?x_125 := @subtype.group ?x_129 ?x_130 ?x_131 ?x_132

[Kevin Buzzard]

Can I solve this with some priority hack? Why does this happen?

[Mario Carneiro]

the class is bad, as you suspect

[Floris van Doorn]

Make add_comm_group M an argument of the class.

[Mario Carneiro]

and the offending instance is right there in the trace - G_module.to_add_comm_group

[Floris van Doorn]

something like

class G_module (G : Type*) (M : Type*) [group G] [add_comm_group M]
  extends has_scalar G M :=

[Kevin Buzzard]

That sounds like a really super instance though.

[Kevin Buzzard]

There is some subtlety here which I don't understand -- this is exactly one of those times where you're saying "don't do it this way, do it in some way which looks exactly the same to a mathematician". Is there some general principle I'm unaware of?

[Mario Carneiro]

Don't have a parent instance with fewer type arguments than the class

[Kevin Buzzard]

wait, what is a parent instance?

[Mario Carneiro]

extends produces an instance

[Kevin Buzzard]

And Floris' suggestion doesn't?

[Mario Carneiro]

In the original case it was [G_module G M] : add_comm_group M

[Mario Carneiro]

no, I am in complete agreement with floris

[Mario Carneiro]

floris is proposing to remove this instance, which is bad because G is "dangling"

[Kevin Buzzard]

Yes I understand that. And this is not generated in the suggested fix?

[Kevin Buzzard]

Sorry, I had a little internet time-out. My comment referred to "extends produces an instance"

[Johan Commelin]

@Kevin Buzzard You know about https://github.com/leanprover-community/mathlib/blob/66a86ffe010ffc32ee92e2e92cbdaf83487af168/src/group_theory/group_action.lean#L173 ?

[Mario Carneiro]

reading it from right to left, G just appears and lean doesn't know how to pick a value

[Johan Commelin]

/-- Typeclass for multiplicative actions on additive structures. This generalizes group modules. -/
class distrib_mul_action (α : Type u) (β : Type v) [monoid α] [add_monoid β] extends mul_action α β :=
(smul_add : ∀(r : α) (x y : β), r • (x + y) = r • x + r • y)
(smul_zero {} : ∀(r : α), r • (0 : β) = 0)

[Kevin Buzzard]

reading it from right to left, G just appears and lean doesn't know how to pick a value

I appreciate the problem; I am just saying that my understanding of why it occurs the way I did it and not the way Floris did it is hazy. extends produces an instance, this is the point. So Floris' method produces no instances?

[Kevin Buzzard]

Johan -- no, I didn't know about this.

[Floris van Doorn]

My solution doesn't generate the instance, because Lean will need to synthesize the instance add_comm_group M before it can even start searching for an instance of G_module G M

[Kevin Buzzard]

Right.

[Mario Carneiro]

there is still a parent instance coming from the other extends clause

[Kevin Buzzard]

In a parallel universe someone could tell me that this [Floris' suggestion] produces an instance anyway, and I would happily believe them.

[Mario Carneiro]

The easiest way to think of it is extends is notation for an extra field in the class + an instance to get to the parent from the child

[Mario Carneiro]

AFAIK it's the only way to get autogenerated instances

[Floris van Doorn]

Well, let's try do define this instance:

instance (G : Type*) (M : Type*) [group G] [add_comm_group M] [G_module G M] :
  add_comm_group M :=
_

What would you pick for the value of the underscore? It's the instance you already got as an argument. So this instance says "if you want add_comm_group M then you need to search for add_comm_group M (and a bunch more things). It's (worse than) useless.

[Kevin Buzzard]

My understanding of what is going on here is hazy at best. I even don't really understand, in some sense, why the instance is bad, because I don't really understand how type class inference works; I can of course see that it's bad because of what just happened, but the fact that I asked here instead of trying to fix it myself (which is nowadays my preferred solution with problems I run into) is just an indication of my poor understanding of this stuff.

I keep meaning to write some doc for docs/extras/ about the nitty-gritty of how type class inference works but I've had a busy year. The next three months are looking much nicer though, maybe I should actually do this; writing the docs myself will show me what I don't understand.

[Mario Carneiro]

It's a prolog-like search

[Mario Carneiro]

Every instance says "to prove A it suffices to prove B, C, D" and lean just applies all instances greedily hoping to get somewhere

[Kevin Buzzard]

[prolog] Yeah, somehow this is exactly the problem. I can believe that at some point in CS UG there's a chance to do some lectures / problem sets on how prolog works. In maths departments we don't do this. On a couple of occasions now I've sat down to fathom this out (even installing prolog on one occasion) but then never wrote down any of my thoughts and then I just forget them again. Writing things down is really helpful for me at my age -- only today did I look at my simp notes that I wrote so I could find out how to turn the trace on for simp -- I always forget, but I know where to look. The docs I write are "by me now, for me next week" :-)

[Floris van Doorn]

Btw, I don't have some magical superpower that I know how to do these things. The general strategy for a lot of formalization is to see if someone has done something similar before. If so, copy their code and adapt it to your case. In this case, the definition of module is similar:
https://github.com/leanprover-community/mathlib/blob/master/src/algebra/module.lean#L25
Often the design decisions will be the same for your case.

[Kevin Buzzard]

Btw, I don't have some magical superpower

Rotten luck! Mathematicians have a super-power.

[Floris van Doorn]

I do this all the time, even if I wrote the previous code. Past me was usually much more aware of all the pitfalls (because he fell into them, and then changed the code).

[Kevin Buzzard]

Unfortunately, Lean disables our super-power.

[Mario Carneiro]

You should mostly assume that lean applies instances in the worst possible order, because anything else is luck. So if there is an instance like "to prove T A it suffices to prove T (A x A)" then it should be clear that lean will loop

[Kevin Buzzard]

ha ha, that rule of thumb stinks! It's crying out for a fix.

[Kevin Buzzard]

The rule of thumb makes perfect sense, but somehow says "we could be doing this better". I guess we had this conversation once before quite recently.

[Mario Carneiro]

It's not as bad as it sounds; you just have to make sure that the worst possible order isn't that bad

[Kevin Buzzard]

I know that making typeclass inference better is on Leo's mind.

[Floris van Doorn]

i really think we should use priority n more in mathlib so that we can decide which instances should be applied first and which ones should be applied last.

[Kevin Buzzard]

[we had a brief email exchange when perfectoids got done, and he mentioned it]

[Mario Carneiro]

I agree that more use of priority would be a good thing, but I currently don't have a good model for how to structure the priorities

[Floris van Doorn]

My gut feeling says priorities should be as follows:

• Structural instances: an instance which only works for certain types (like group A -> group B -> group (prod A B) or ring int). If such an instance applies, then it's almost always the instance you want to apply. So the order doesn't matter that much, but you can put the more common instances in front.
• Forgetful instances, like comm_group A -> group A. Here you want to order them by how likely they are to apply (taking into consideration how long it would take for this instance to fail). Ultimately this will depend on which area of maths you're doing. When doing ring theory, you'll want to apply ring.to_add_comm_groupfirst, while in other cases you might want to do apply ordered_comm_group.to_add_comm_group first (this is not a great example, I think you almost always want to apply ring.to_add_comm_group first).

Looking a bit over #print instances, it looks like mathlib does this mostly right. I think this is partially accidental, since forgetful instances tend to be declared before structural instances are, and so even if they have the same priority they will be considered later. Some things I noticed:

• Sometimes there are "shortcuts", like decidable_linear_ordered_comm_group.to_add_comm_group and ordered_comm_group.to_add_comm_group (or linear_ordered_ring.to_linear_order and linear_ordered_semiring.to_linear_order). If these instances do not apply, the search through the "order hierarchy" will happen twice, right? Probably these shortcuts should be removed?
• nonneg_comm_group.to_add_comm_group should have a lower priority.
• Some declarations should probably not be instances: decidable_eq_of_decidable_le or decidable_lt_of_decidable_le. Unfortunately they are in core...

[Mario Carneiro]

We need a real test to find out if shortcuts are taken twice

[Floris van Doorn]

Is set_option trace.class_instances true a reliable test?

example : add_comm_group bool := by apply_instance

gives

[...]
[class_instances] (0) ?x_0 : add_comm_group bool := @decidable_linear_ordered_comm_group.to_add_comm_group ?x_1 ?x_2
[class_instances] (1) ?x_2 : decidable_linear_ordered_comm_group bool := int.decidable_linear_ordered_comm_group
failed is_def_eq
[class_instances] (1) ?x_2 : decidable_linear_ordered_comm_group bool := @decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_comm_group ?x_3 ?x_4
[class_instances] (2) ?x_4 : decidable_linear_ordered_comm_ring bool := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_5 ?x_6 ?x_7 ?x_8
[class_instances] (2) ?x_4 : decidable_linear_ordered_comm_ring bool := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (2) ?x_4 : decidable_linear_ordered_comm_ring bool := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_5 ?x_6
[class_instances] (0) ?x_0 : add_comm_group bool := @ordered_comm_group.to_add_comm_group ?x_1 ?x_2
[...]
[class_instances] (4) ?x_8 : linear_ordered_comm_ring bool := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring ?x_9 ?x_10
[class_instances] (5) ?x_10 : decidable_linear_ordered_comm_ring bool := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_11 ?x_12 ?x_13 ?x_14
[class_instances] (5) ?x_10 : decidable_linear_ordered_comm_ring bool := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (5) ?x_10 : decidable_linear_ordered_comm_ring bool := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_11 ?x_12
[class_instances] (1) ?x_2 : ordered_comm_group bool := @decidable_linear_ordered_comm_group.to_ordered_comm_group ?x_3 ?x_4
[class_instances] (2) ?x_4 : decidable_linear_ordered_comm_group bool := int.decidable_linear_ordered_comm_group
failed is_def_eq
[class_instances] (2) ?x_4 : decidable_linear_ordered_comm_group bool := @decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_comm_group ?x_5 ?x_6
[class_instances] (3) ?x_6 : decidable_linear_ordered_comm_ring bool := @linear_nonneg_ring.to_decidable_linear_ordered_comm_ring ?x_7 ?x_8 ?x_9 ?x_10
[class_instances] (3) ?x_6 : decidable_linear_ordered_comm_ring bool := int.decidable_linear_ordered_comm_ring
failed is_def_eq
[class_instances] (3) ?x_6 : decidable_linear_ordered_comm_ring bool := @discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ?x_7 ?x_8

It seems like it considered decidable_linear_ordered_comm_ring bool three times.

[Floris van Doorn]

Now sometimes duplication is impossible to avoid, without changing the code to the search, when you have diamonds...

[Mario Carneiro]

class A (α : Type) (n : ℕ)
class B (α : Type) (n : ℕ) extends A α n
class C (α : Type) (n : ℕ) extends B α n

instance C_nat : C ℕ 0 := @C.mk _ _ (@B.mk _ _ ⟨_, _⟩)

instance C_of_A' (α n) [A α n] : C α n.succ := @C.mk _ _ (@B.mk _ _ ⟨_, _⟩)
instance shortcut (α n) [C α n] : A α n := by apply_instance

set_option trace.class_instances true
set_option class.instance_max_depth 1000
#check (by apply_instance : C ℕ 30)

it's considering shortcut at each level but it's not exponential

[Floris van Doorn]

About the decidable_eq_of_decidable_leissue: maybe we should set their priorities in mathlib to 0, and decide that local attribute [instance, priority 10] classical.prop_decidable should happen at priority 10, not 0. Now, it probably searches through big chunks of the order hierarchy twice, when you want that prop_decidable should decide an equality on any type:

• through decidable_linear_order α
• through decidable_eq_of_decidable_le

[Mario Carneiro]

oh wait, C unit 7 is definitely exponential

[Mario Carneiro]

that's disconcerting

[Mario Carneiro]

once again I am staggered that typeclass inference works at all

[Floris van Doorn]

numerals have special support on nat, maybe that makes a difference?

[Mario Carneiro]

no, that just makes it a bit easier to write a bunch of succs here

[Mario Carneiro]

Compare the instance trace on C unit 7 with and without shortcut

[Floris van Doorn]

the problem is that your first instance never fails: all instances it tries succeed. Each branch is linear: backtracking is exponential.

[Mario Carneiro]

To some extent that's not unreasonable - I'm not sure how much we should care about failing searches

[Floris van Doorn]

a lot

[Floris van Doorn]

whenever you do local attribute [instance, priority 0] classical.prop_decidable there are a whole lot of failing searches.

[Floris van Doorn]

probably half of the "Forgetful instances" will fail. (even if applying another instance succeeds)

[Mario Carneiro]

here's a case where the instance succeeds but takes a long time:

class D (α : Type) (n : ℕ)
instance D_unit (n) : D unit n := ⟨_, _⟩
instance D_of_C (α n) [C α n] : D α n := ⟨_, _⟩

set_option trace.class_instances true
set_option class.instance_max_depth 1000
#check (by apply_instance : D unit 7)

[Floris van Doorn]

when doing some testing on my own

(message too long, truncated at 262144 characters)

lol,

But I think it's pretty clear we should remove these shortcuts of "forgetful" instances.

[Mario Carneiro]

this is a real shame, these could be useful in principle but lean really doesn't like them

[Kevin Buzzard]

(message too long, truncated at 262144 characters)

Gabriel put that check there precisely because I was fiddling around with this sort of thing once and managed to get a message that was so long that it broke stuff.

[Mario Carneiro]

but actually I don't know to what degree we can make our hierarchy "tree-like"

[Mario Carneiro]

algebraic hierarchies don't work like that

[Floris van Doorn]

There should really be a different algorithm for these "forgetful instances". Make a graph of all instances that change the class but not the type (like add_comm_group \a -> add_group \a) and when you have searched through all structural instances (or all instances with priority >= default priority), then use a graph reachability algorithm to quickly search for a path to any instance in the local context.

[Kevin Buzzard]

@Sebastian Ullrich how about you make type class search user-configurable? Everyone has different ideas :-)

[Johan Commelin]

I think that is one of the plans for Lean 4

[Sebastian Ullrich]

@Kevin Buzzard Making typeclass inference based on customizable tactics has been proposed before, but no one has figured out how to combine that with instance caching

[Kevin Buzzard]

My comment was really tongue-in-cheek I guess

[Kevin Buzzard]

The moment you let users do what they want is presumably the moment that things get really inefficient

[Kevin Buzzard]

We have seen type class inference doing some silly things recently

[Kevin Buzzard]

But it is not clear to me that there is some unified sensible algorithm which stops all of those silly things happening at once whilst remaining efficient

[Kevin Buzzard]

Why not just let prolog do it and make prolog a dependency?

[Kevin Buzzard]

Some people claimed that prolog was better than lean at prolog-like searches

[Kevin Buzzard]

I of course am in no position to comment

[Johan Commelin]

The difference is maybe that Prolog does a Prolog search, instead of merely a prolog-like search :grimacing:

[Sebastian Ullrich]

For starters, Lean's unification is much more complex than Prolog's. You wouldn't want to lose delta reduction in instance searches

[Kevin Buzzard]

I still reserve the right to snicker when Lean tries 20 random things in order to prove that rat has a one, before finally stumbling on rat.has_one

[Johan Commelin]

I still reserve the right to snicker when Lean tries 20 random things in order to prove that rat has a one, before finally stumbling on rat.has_one

:up: Completely agree. I think that guessing the correct name is one place where we could really win, and possibly win a lot.

[Johan Commelin]

For this reason, I've been trying to always use the auto-generated name for instances, in the hope that this will pay of in the future.

[Sebastian Ullrich]

This is one example where some instance indexing approach in Lean 4 should make the search instantaneous. Well, assuming you really have the same "one" in goal and instance.

[Johan Commelin]

It might break some sort of psychological/abstraction barrier in the software though: names ought to be irrelevant to Lean, and only relevant for humans.

[Chris Hughes]

Use some hidden name that isn't the name we have to look at.

[Wojciech Nawrocki]

Why does searching for instances in the local context work with explicit arguments but not under a lambda?

class myclass (α: Type)
def foo {α: Type} [myclass α] (a: α): α := a

def bar (n: ℕ) [h: myclass ℕ]: ℕ :=
foo n -- good

def bar': Π (n: ℕ) [myclass ℕ], ℕ :=
λ n h, foo n
/- failed to synthesize type class instance for
n : ℕ,
h : myclass ℕ
⊢ myclass ℕ -/

[Chris Hughes]

Performance reasons I think. You can do

def bar': Π (n: ℕ) [myclass ℕ], ℕ :=
λ n h, by exactI foo n

or

def bar': Π (n: ℕ) [myclass ℕ], ℕ :=
λ n h, by resetI; exact foo n

[Wojciech Nawrocki]

Ah indeed, local instances are "frozen". unfreeze_local_instances is the intrinsic for this. Thanks!