can I fix this deterministic timeout?

Stream: general

[Kevin Buzzard]

I am in the middle of a long proof and finding it hard to shorten. I have a hypothesis H3 in my local context. I have a killer theorem which I want to apply, which takes 11 inputs (it's one of these obvious-to-a-mathematician statements of the form "if something happens, then when you replace everything by something equiv to it then it still happens). I want one of the inputs to be H3, but if I put H3 into it then I get a deterministic timeout. Instead I write (_ : [type of H3]) as an input and then I get an extra goal, which I can clear with exact H3.

[Kevin Buzzard]

Am I missing a trick here? Am I likely to have made an error? I am not sure I can minimise.

[Mario Carneiro]

that's a bit vague. does by exact H3 work?

[Kevin Buzzard]

I know it's vague, but deterministic timeouts are a big vague too :-/

[Mario Carneiro]

is the type of H3 exactly the same as the expected type?

[Kevin Buzzard]

I believe so

[Kevin Buzzard]

by exact H3 doesn't work

[Kevin Buzzard]

in the sense that I still get the timeout

[Kevin Buzzard]

have H3 : (Π (i : γ), loc Rr (powers (f i))) ≃ Π (i : γ), loc R (non_zero_on_U (Ui i)) := equiv.prod H2,

[Kevin Buzzard]

[is equiv.prod already there, by the way? If X i equiv Y i for all i then prod_i X i = prod_i Y i]

[Mario Carneiro]

Pi_congr_right

[Kevin Buzzard]

and (H3 : ((Π (i : γ), loc Rr (powers (f i))) ≃ (Π (i : γ), loc R (non_zero_on_U (Ui i))))) as my input gives me a timeout

[Mario Carneiro]

prod is the binary product

[Kevin Buzzard]

thanks

[Kevin Buzzard]

that would be why I couldn't find it ;-)

[Kevin Buzzard]

I should say that one can't determine the type of H3 immediately, type class inference is doing a lot of work here

[Mario Carneiro]

I'm afraid this is a little too restricted to get the full picture

[Kevin Buzzard]

I have about 15 implicit inputs as well as about 10 explicit ones

[Mario Carneiro]

I suggest leaving this for later then, refine with a _ and then insert it after the unification works

[Kevin Buzzard]

yes this works fine

[Kevin Buzzard]

Here's the function I'm trying to apply

[Kevin Buzzard]

fourexact_from_iso_to_fourexact : ∀ {A B C A' B' C' : Type u_1} [_inst_1 : add_comm_group A] [_inst_2 : add_comm_group A'] [_inst_3 : add_comm_group B] [_inst_4 : add_comm_group B'] [_inst_5 : add_comm_group C] [_inst_6 : add_comm_group C'] (ab : A → B) [_inst_7 : is_add_group_hom ab] (bc : B → C) [_inst_8 : is_add_group_hom bc], (∀ (b : B), bc b = 0 → (∃! (a : A), ab a = b)) → ∀ (fa : A ≃ A') [_inst_9 : is_add_group_hom ⇑fa] (fb : B ≃ B') [_inst_10 : is_add_group_hom ⇑fb] (fc : C ≃ C') [_inst_11 : is_add_group_hom ⇑fc] (ab' : A' → B') [_inst_12 : is_add_group_hom ab'] (bc' : B' → C') [_inst_13 : is_add_group_hom bc'], (∀ (a : A), ⇑fb (ab a) = ab' (⇑fa a)) → (∀ (b : B), ⇑fc (bc b) = bc' (⇑fb b)) → ∀ (b' : B'), bc' b' = 0 → (∃! (a' : A'), ab' a' = b')

[Kevin Buzzard]

I have 13 things which need to be inferred by type class inference because someone somewhere decided that add_comm_group and is_add_group_hom were type classes

[Kevin Buzzard]

and I have six add_comm_groups

[Mario Carneiro]

I assume all those searches are trivial though, right?

[Kevin Buzzard]

and I want Lean to infer them from things like ab and fb etc

[Kevin Buzzard]

yes everything should be trivial

[Kevin Buzzard]

oh

[Kevin Buzzard]

let me rephrase

[Kevin Buzzard]

that

[Mario Carneiro]

like they are in the context

[Kevin Buzzard]

I have no idea whether these searches are trivial

[Kevin Buzzard]

I doubt they're in the context

[Kevin Buzzard]

I could easily put them in with by apply_instance

[Kevin Buzzard]

If I put them in the context, will type class inference pick them up? I thought not

[Mario Carneiro]

I suggest you have a type for group isos instead of (fa : A ≃ A') [_inst_9 : is_add_group_hom ⇑fa]

[Kevin Buzzard]

I have a type for R-algebra isos ;-)

[Kevin Buzzard]

and instances which give me the equiv and the add_group_hom

[Kevin Buzzard]

but I'm letting type class inference do all of this

[Kevin Buzzard]

This whole experience has been extremely hard going, by the way.

[Kevin Buzzard]

I've had to set that other parameter which causes me trouble up to 100

[Mario Carneiro]

I suggest you apply this theorem by writing apply fourexact_from_iso_to_fourexact ... bc' giving all the function arguments, and then prove the remaining goals

[Kevin Buzzard]

yes that's exactly what I'm doing

[Kevin Buzzard]

it avoids the time out

[Kevin Buzzard]

It does mean that all of a sudden I go from 1 goal to 11

[Kevin Buzzard]

I have set_option class.instance_max_depth 100 too

[Kevin Buzzard]

and all I am doing is proving something which is so trivial that it is not even explicitly mentioned in the stacks project

[Mario Carneiro]

An alternative is have := fourexact_from_iso_to_fourexact ... bc' then refine this ... with the remaining args

[Kevin Buzzard]

I have a workaround

[Kevin Buzzard]

I was just wondering what was happening

[Kevin Buzzard]

I was going to take the 11 goals

[Kevin Buzzard]

and then solve them all in squiggly brackets with "show" at the top of each one

[Mario Carneiro]

This theorem is more complicated than it needs to be btw

[Kevin Buzzard]

I know full well

[Mario Carneiro]

you don't need any groups at all

[Kevin Buzzard]

because it's all trivial

[Kevin Buzzard]

and your silly system doesn't know this

[Mario Carneiro]

the statement is just about functions

[Mario Carneiro]

so all the TC args can go away

[Kevin Buzzard]

TC?

[Mario Carneiro]

typeclass

[Kevin Buzzard]

yes you're right

[Kevin Buzzard]

It's a statement about pointed sets

[Kevin Buzzard]

Are there pointed sets in Lean?

[Kevin Buzzard]

I've been carrying the group homs around because in practice one uses some algebra to prove the diagram commutes -- "both maps are the unique group hom with some property" etc.

[Kevin Buzzard]

You need a zero though, to define kernel

[Mario Carneiro]

Floris knows a lot about pointed sets in lean

[Kevin Buzzard]

But you don't need anything else

[Kevin Buzzard]

I'll rephrase it in terms of pointed sets

[Kevin Buzzard]

and then someone will make [is_pointed_set_hom] a typeclass

[Kevin Buzzard]

and I'll be back to square one ;-)

[Kevin Buzzard]

So it's not just about functions in fact

[Kevin Buzzard]

I need that a kernel maps to a kernel

[Mario Carneiro]

For your purposes I would just take the pointedness assumption as an argument

[Kevin Buzzard]

so I need that 0 maps to 0

[Kevin Buzzard]

I need that my equivs are equivs of pointed sets

[Mario Carneiro]

You should study how the transfer tactic works, even if you don't use the tactic the supporting theorems may be of use to you

[Kevin Buzzard]

I am solving my 11 goals and I think I located the reason for the time-out. If I put H3 explicitly into the system then type class inference tries to prove it's a group hom and type class inference isn't very good at this sort of thing in my experience.

[Kevin Buzzard]

Ever since I've been trying to use type class inference to prove things are group homs / ring homs etc, I've been having trouble.

[Kevin Buzzard]

I've now realised that this is just another one of my type class woes

[Kevin Buzzard]

  show is_add_group_hom H3',
    apply_instance,

[Kevin Buzzard]

There's the time-out. So your instinct was right

[Kevin Buzzard]

Thanks.

[Kevin Buzzard]

It's a product of group homs

[Kevin Buzzard]

and maybe there's no instance that if X i -> Y i is a group hom for all i then Pi i, X i -> Pi i, Y i is a group hom

[Mario Carneiro]

that one is up to you, I don't think is_add_group_hom even exists in mathlib

[Mario Carneiro]

but you have to show that Pi_congr_right as defined respects the Pi group structure

[Kevin Buzzard]

I have type class inference issues :-(

[Kevin Buzzard]

How do I say "for all i, the proof (e i) of equiv (X i) (Y i) is a ring hom" (say)

[Kevin Buzzard]

in the sense that I want that to be the assumption, inferred by type class inference

[Kevin Buzzard]

This has nothing to do with equiv.

[Kevin Buzzard]

Let me formulate something easier, and in the correct thread.

[Mario Carneiro]

It's just \forall i, is_ring_hom (e i)

[Kevin Buzzard]

It was getting it in the brackets I was worried about

[Kevin Buzzard]

But [∀ (i : γ), ring (F i)] works fine

[Kevin Buzzard]

I've never seen that construction before

[Kevin Buzzard]

Thanks as ever. I'm back on track!

[Patrick Massot]

@Kevin Buzzard You should start reading from https://github.com/leanprover/mathlib/blob/master/algebra/pi_instances.lean#L61

[Patrick Massot]

and add things if needed

[Kevin Buzzard]

We use this stuff in the schemes work.

[Kevin Buzzard]

But it's only objects.

[Kevin Buzzard]

I now realise we need the morphisms too.

[Kevin Buzzard]

Currently my impression is that the morphisms which are classes are kind of random, and not all are classes.

[Kevin Buzzard]

For morphisms, I find myself needing both "if $X \to Y_i$ are group homs, then $X \to \Pi_i Y_i$ is"

[Kevin Buzzard]

and "if $X_i\to Y_i$ are group homs, then $\Pi_i X_i \to \Pi_i Y_i$ is too"

[Kevin Buzzard]

It was these instances that caused the time-out :-)

[Kevin Buzzard]

It knew that the product of groups was a group and then timed out trying to prove using type class inference only that the product of the morphisms was a morphism

[Mario Carneiro]

how are those functions being specified?

[Mario Carneiro]

you wrote the type but not the term there

[Patrick Massot]

Then I'm confused. How could you write: "[∀ (i : γ), ring (F i)] I've never seen that construction before"

[Patrick Massot]

Anyway, I think having Lean figuring out by itself that composition and products of morphisms are morphisms is a good reason to try to use type class here. But you need to add instances to that pi_instance file, which was written at a time were morphisms were defs

[Patrick Massot]

That may require improving Simon's pi_instance tactic

[Patrick Massot]

I'm not sure

[Kevin Buzzard]

how are those functions being specified?

There's only one sensible specification in each case. I just noticed that the Android Zulip app doesn't do maths mode.

[Kevin Buzzard]

Then I'm confused. How could you write: "[∀ (i : γ), ring (F i)] I've never seen that construction before"

I glanced at the Pi file at the time, realised I understood what it did, forgot how it did it, then had to do it myself. Patrick I'm nearly 50. It's completely consistent that I have to write [∀ (i : γ), ring (F i)] again in two months' time and again claim that I've never seen it before.

[Kevin Buzzard]

I mean "...according to my memory banks" :-)

[Kevin Buzzard]

It's pretty depressing. Sometimes I want to know something about some technical number theory question so I google, find a good mathoverflow answer, read it, learn a lot, and then discover to my surprise that I had written the answer myself 5 years ago. The first time that happened to me was a genuine shock. Now I just consider it normal.

[Kevin Buzzard]

It's not depressing at all -- it's pretty funny :-)

[Mario Carneiro]

There's only one sensible specification in each case.

Not quite: are you giving an explicit lambda term or a definition?

[Kevin Buzzard]

I don't understand the subtlety you've found, but what I am saying is that I need the following two facts:

[Mario Carneiro]

I'm just asking what you wrote

[Mario Carneiro]

the typeclass system is trying to solve is_add_group_hom ...; what is in the place of the ...?

[Mario Carneiro]

the typeclass system is very sensitive to the way you write things

[Kevin Buzzard]

(1) If gamma is a type and for all i in gamma I have (f i : X -> Y i), which type class inference knows is a group hom (actually in my case this one was a ring hom) then the induced map from X to Pi i, Y i sending x i to f i (x) is a group hom

[Mario Carneiro]

the induced map from X to Pi i, Y i sending x i to f i (x)

and how did you write that

[Kevin Buzzard]

\lam x i,f i x I guess

[Mario Carneiro]

did you prove that in a lemma?

[Kevin Buzzard]

I proved it in an instance

[Mario Carneiro]

show me

[Kevin Buzzard]

well I didn't yet

[Kevin Buzzard]

are you saying I'm going to run into trouble?

[Kevin Buzzard]

I proved the other one

[Mario Carneiro]

well if the instance isn't there of course it will fail

[Mario Carneiro]

but yes, that instance is trouble

[Mario Carneiro]

you want to wrap that function in a definition

[Kevin Buzzard]

Oh

[Kevin Buzzard]

Here's the one I did

[Kevin Buzzard]

instance Prod {γ : Type u} {F : γ → Type u} {G : γ → Type u} [∀ i, add_group (F i)]
[∀ i, add_group (G i)] (H : ∀ i : γ, F i → G i) [∀ i, is_add_group_hom (H i)] :
 is_add_group_hom (λ Fi i, H i (Fi i) : (Π i, F i) → Π i, G i) := ⟨λ a b, funext $ λ i,
show H i ((a i) + (b i)) = H i (a i) + H i (b i),
by rw (add (H i))⟩

[Kevin Buzzard]

You don't know the type class I'm using here

[Kevin Buzzard]

def is_add_group_hom {α : Type u} {β : Type v} [add_group α] [add_group β] (f : α → β) : Prop :=
@is_group_hom (multiplicative α) (multiplicative β) _ _ f

[Kevin Buzzard]

theorem add (x y) : f (x + y) = f x + f y :=
@is_group_hom.mul (multiplicative α) (multiplicative β) _ _ f hf x y

[Kevin Buzzard]

Are there problems with this?

[Mario Carneiro]

this is bad: is_add_group_hom (λ Fi i, H i (Fi i))

[Kevin Buzzard]

Hmm

[Kevin Buzzard]

Well thanks for spotting this

[Mario Carneiro]

it's okay as a def but as an instance it requires higher order unification

[Kevin Buzzard]

On the other hand

[Kevin Buzzard]

these morphisms between mathematical objects are being defined to be type classes

[Kevin Buzzard]

so I am being pushed to use the type class inference system

[Mario Carneiro]

you just need to define Pi_lift H := λ Fi i, H i (Fi i and give that the instance

[Kevin Buzzard]

Oh so I can still use type class inference

[Mario Carneiro]

the typeclass system needs a constant to key on

[Kevin Buzzard]

This is of course the problem with me using things I don't understand completely

[Kevin Buzzard]

It's exactly what I tell my graduate students not to do

[Kevin Buzzard]

I don't know what "constant" or "key on" mean in your last post

[Mario Carneiro]

for example if you want to show is_group_hom (f o g) it's no problem but is_group_hom (\lam x, f (g x)) is not likely to work

[Kevin Buzzard]

boggle

[Sean Leather]

Mario probably means a unique definition name.

[Sean Leather]

function.compose in that case.

[Kevin Buzzard]

I just spent some time changing f circ g's to lam x, f (g x) because Kenny told me that things were better that way

[Kevin Buzzard]

in the sense that they were easier to work with

[Kenny Lau]

I just spent some time changing f circ g's to lam x, f (g x) because Kenny told me that things were better that way

you see, things have a context

[Mario Carneiro]

That's true for the most part, but if it shows up as the target of a typeclass problem you want it to be "obviously a morphism"

[Kenny Lau]

for example if you want to show is_group_hom (f o g) it's no problem but is_group_hom (\lam x, f (g x)) is not likely to work

but aren't they definitionally equivalent?

[Mario Carneiro]

and that means writing things functorially

[Mario Carneiro]

they are, but typeclass inference doesn't work up to definitional equivalence

[Kevin Buzzard]

I wonder if this has anything to do with the fact that three times now I've had to set_option class.instance_max_depth 100

[Mario Carneiro]

it's doing a big search through the whole library. It doesn't have time to unify everything properly

[Kenny Lau]

what do they work up to?

[Mario Carneiro]

unification of metavariables unfolding reducibles only

[Kevin Buzzard]

I want to give hints to the system

[Kenny Lau]

is that another type of equivalence?

[Kevin Buzzard]

because in every case I know exactly what I want it to do

[Mario Carneiro]

it's almost syntactic equality, except that reducible definitions are eagerly expanded

[Kevin Buzzard]

In some cases it's even "I want you to use precisely the instance which I just defined in another file precisely so that this next line will work"

[Mario Carneiro]

the key is to write the typeclass problem so that it's obvious to the system

[Mario Carneiro]

that basically means that all your typeclass instances should have the form my_class (my_operation A B C)

[Kevin Buzzard]

To put this into some context, the fact that the product of group homs is a group hom is the sort of thing which is explained in an undergraduate maths lecture in the 15 minute period just after the definition of a group hom has been given, and is then never mentioned again and everyone thinks it's obvious

[Mario Carneiro]

with some assumptions like my_class A my_class2 B

[Mario Carneiro]

and your typeclass problems should look like my_class (my_op (my_other_op A) B)

[Mario Carneiro]

no lambdas

[Kevin Buzzard]

Well this is very helpful. Whereabouts is all this documented? ;-)

[Sean Leather]

Look up. :arrow_up: :wink:

[Kevin Buzzard]

I don't know why I'm bothering writing docs, I could just refer people to https://leanprover.zulipchat.com/

[Sean Leather]

TBD: The type class reference section is currently empty.

[Kevin Buzzard]

Oh, on a related topic, why Pi_congr_right?

[Kevin Buzzard]

I mean, why the name?

[Kevin Buzzard]

equiv.Pi_congr_right : Π {α : Sort u_3} {β₁ : α → Sort u_4} {β₂ : α → Sort u_5}, (Π (a : α), β₁ a ≃ β₂ a) → ((Π (a : α), β₁ a) ≃ Π (a : α), β₂ a)

[Kevin Buzzard]

That looks like equiv.Pi to me

[Kevin Buzzard]

modulo the fact that that name is probably illegal

[Kevin Buzzard]

but I don't see anything right about it, other than the fact that it's right

[Kevin Buzzard]

Are these fundamental constructions already in Lean:

[Kevin Buzzard]

definition Pi_lift₁ {γ : Type u} {F : γ → Type u} {G : γ → Type u}
  (H : ∀ i : γ, F i → G i) : (Π i, F i) → Π i, G i := λ Fi i, H i (Fi i)

definition Pi_lift₂ {γ : Type u} {X : Type u} {G : γ → Type u}
  (H : ∀ i : γ, X → G i) : X → Π i, G i := λ x i, H i x

[Mario Carneiro]

Pi takes two arguments

[Mario Carneiro]

a domain and a family

[Mario Carneiro]

Pi_congr_left is likely to be much messier though so I left it out

[Kevin Buzzard]

So is the following now OK:

[Kevin Buzzard]

instance is_add_group_hom.Pi_lift {γ : Type u} {F : γ → Type u} {G : γ → Type u} [∀ i, add_group (F i)]
[∀ i, add_group (G i)] (H : ∀ i : γ, F i → G i) [∀ i, is_add_group_hom (H i)] :
 is_add_group_hom (Pi_lift_map₁ H) := ⟨λ a b, funext $ λ i,
show H i ((a i) + (b i)) = H i (a i) + H i (b i),
by rw (add (H i))⟩

[Mario Carneiro]

yep that's ok

[Kevin Buzzard]

Can you appreciate that this is a subtlety that people are unlikely to guess, and it's up to the very few people who appreciate the subtlety to somehow get the news around? :-/

[Mario Carneiro]

certainly

[Kevin Buzzard]

I don't recall this being mentioned in TPIL

[Kevin Buzzard]

although as we've seen earlier in this thread, that's not saying much

[Kevin Buzzard]

I guess I felt the same way about simp earlier on.

[Mario Carneiro]

In a way, it's "your fault" in generalizing from "typeclasses can do X" to "typeclasses can do Y"

[Kevin Buzzard]

I would tag arbitrary things with simp and then had to be rolled back by people that actually knew what simp did

[Kevin Buzzard]

I mean, by people who knew _how simp actually worked_

[Kevin Buzzard]

and I guess the same is happening here.

[Mario Carneiro]

everything has limitations, and most of the existing documentation is vague about where the limitations are

[Kevin Buzzard]

In maths, generalizing like that is a _really_ important skill

[Kevin Buzzard]

It's not so clear that such limitations exist in maths

[Kevin Buzzard]

If you understand the idea behind a proof

[Kevin Buzzard]

then you can see the same idea working in many other situations

[Mario Carneiro]

on the one hand, you can assume Leo is magic and made everything work (which is not an unreasonable rule of thumb)

[Kevin Buzzard]

I feel like I need you a huge amount less than I needed you last October

[Kevin Buzzard]

but I still need you from time to time :-)

[Kevin Buzzard]

Many thanks as ever

[Mario Carneiro]

but sometimes if you don't know you should stick to areas that you know how to use already... it's a balancing act

[Mario Carneiro]

I don't use finish or cc because I don't understand them well

[Kevin Buzzard]

Don't say that in front of your advisor

[Kevin Buzzard]

didn't he write at least one of them?

[Mario Carneiro]

yes, Jeremy wrote finish

[Mario Carneiro]

I'm not sure he understands it either, since it's a complicated set of heuristics calling in to less understood things like e-matching

[Kevin Buzzard]

My impression is that computer scientists are much better at generating work that they "don't understand"

[Kevin Buzzard]

much better than mathematicians, I mean

[Kevin Buzzard]

If I use theorem X whose proof I've not read, in my proof, then I can just argue that I have a complete understanding of "theorem X implies the result I proved"

[Kevin Buzzard]

and all proofs are irrelevant

[Mario Carneiro]

says the man who is rediscovering his own proofs every five years :)

[Kevin Buzzard]

:-)

[Kevin Buzzard]

That's how irrelevant they are :-)

[Kevin Buzzard]

I don't rediscover the proofs I created in my 20s and 30s, those are pretty much hard wired

[Kevin Buzzard]

It's the stuff I do in my 40s that I occasionally do again

[Kevin Buzzard]

This schemes code is getting quite unwieldy, and occasionally I prove some lemma and in the middle of the proof I think "I ran into this issue before, I think I already proved this lemma"

[Kevin Buzzard]

With the tag system I can really control well this sort of thing, most of the time

[Kevin Buzzard]

but when I go "off piste" because the tag says "this is now clear, as every mathematican knows" and Lean is saying "but the diagrams! You have to check they commute!" and I end up with 1000 lines of code checking a triviality, that's when I duplicate

[Kevin Buzzard]

My esteemed co-author writes

[Kevin Buzzard]

instance deus : comm_ring (α [1/S] /ᵣ (S⁻¹ I)) := by apply_instance
instance salva : module (α [1/S] /ᵣ (S⁻¹ I)) (α [1/S] /ᵣ (S⁻¹ I)) := ring.to_module
instance me : is_submodule (is_ring_hom.ker (to_be_named_aux3 S I)) := is_ring_hom.ker.is_submodule (to_be_named_aux3 S I)

[Kevin Buzzard]

Are these OK (modulo the names)

[Kenny Lau]

My esteemed co-author writes

right

[Mario Carneiro]

I would hope that is_submodule (is_ring_hom.ker f) always works

[Kevin Buzzard]

Kenny look how stupid type class inference is:

[Kevin Buzzard]

universe u
definition Pi_lift_map₁ {γ : Type u} {F : γ → Type u} {G : γ → Type u}
  (H : ∀ i : γ, F i → G i) : (Π i, F i) → Π i, G i := λ Fi i, H i (Fi i)

class foomap {α β : Type u} (f : α → β) :=
(preserves_structure : ∀ a : α, f a = f a)

instance Pi_foomap_is_foomap {γ : Type u} {F : γ → Type u} {G : γ → Type u}
(H : ∀ i : γ, F i → G i) [∀ i, foomap (H i)] : foomap (Pi_lift_map₁ H) := sorry

example {γ : Type u} {F : γ → Type u} {G : γ → Type u}
(H : ∀ i : γ, F i → G i) [∀ i, foomap (H i)] : foomap (Pi_lift_map₁ H) := by apply_instance

example {γ : Type u} {F : γ → Type u} {G : γ → Type u}
(H : ∀ i : γ, F i → G i) [∀ i, foomap (H i)] : foomap (λ Fi i, H i (Fi i) : (Π i, F i) → Π i, G i) := by apply_instance

[Mario Carneiro]

the salva instance is trouble

[Kevin Buzzard]

even though they're defeq

[Kevin Buzzard]

the last example fails

[Mario Carneiro]

It can be a local instance, but you don't necessarily want to always have that ring be a module over itself

[Kevin Buzzard]

I think this is because type class inference doesn't have a constant to key on

[Kevin Buzzard]

It can be a local instance, but you don't necessarily want to always have that ring be a module over itself

That ring _is_ always a module over itself, so what do you actually mean?

[Kevin Buzzard]

example {γ : Type u} {F : γ → Type u} {G : γ → Type u}
(H : ∀ i : γ, F i → G i) [∀ i, foomap (H i)] : foomap (Pi_lift_map₁ H) := by apply_instance

example {γ : Type u} {F : γ → Type u} {G : γ → Type u}
(H : ∀ i : γ, F i → G i) [∀ i, foomap (H i)] : (Pi_lift_map₁ H) = (λ Fi i, H i (Fi i) : (Π i, F i) → Π i, G i) := rfl

example {γ : Type u} {F : γ → Type u} {G : γ → Type u}
(H : ∀ i : γ, F i → G i) [∀ i, foomap (H i)] : foomap (λ Fi i, H i (Fi i) : (Π i, F i) → Π i, G i) := by apply_instance -- fails

[Kevin Buzzard]

well I've learnt something today

[Mario Carneiro]

I mean that when you make it an instance you are saying "this is the only ring I want to consider this as a module over"

[Mario Carneiro]

because modules infer their ring argument from typeclass inference

[Mario Carneiro]

Any ring is a module over itself, but that doesn't mean that's the only ring you want to consider, for example R as a Q-module

[Johan Commelin]

But if you consider R as an R-module, and later you need it as Q-module, then this could be inferred by some statement about forgetting scalars, right?

[Johan Commelin]

Except that we might get a diamond...

[Mario Carneiro]

forgetting scalars?

[Johan Commelin]

From R to Q

[Mario Carneiro]

as in you want to compose with a ring hom?

[Johan Commelin]

Every R-module is a Q-module

[Johan Commelin]

That is what I mean

[Kevin Buzzard]

I can envisage your implied assertion that each abelian group can only be a module over one ring as being problematic

[Johan Commelin]

And somehow newbie me would wish that typeclass inference can do that for me

[Kevin Buzzard]

I just found something else problematic too

[Kevin Buzzard]

def Pi_congr_right {α} {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) : (Π a, β₁ a) ≃ (Π a, β₂ a) :=
⟨λ H a, F a (H a), λ H a, (F a).symm (H a),
 λ H, funext $ by simp, λ H, funext $ by simp⟩

[Kevin Buzzard]

That's your(?) definition of Pi_congr_right

[Kevin Buzzard]

but you did not use definition Pi_lift_map₁ {γ : Type u} {F : γ → Type u} {G : γ → Type u} (H : ∀ i : γ, F i → G i) : (Π i, F i) → Π i, G i := λ Fi i, H i (Fi i)

[Johan Commelin]

Ok, I guess I don't understand typeclass inference... and what I mean is that I would like every R-module to automatically coerce to a Q-module when that's necessary

[Mario Carneiro]

of course not, you just wrote it

[Kevin Buzzard]

but I am using Pi_congr_right to construct my product instances

[Kevin Buzzard]

so now I can't use type class inference on them

[Mario Carneiro]

You will need a theorem saying that \u Pi_congr_right is a group hom

[Mario Carneiro]

it's defeq to your other one about Pi_lift

[Kevin Buzzard]

I see, so I don't try and get you to rewrite Pi_congr_right

[Mario Carneiro]

right, that's too much for TC inference

[Mario Carneiro]

even if it was rewritten it wouldn't help

[Kevin Buzzard]

But am I safe making this an instance?

[Mario Carneiro]

yes

[Kevin Buzzard]

I mean the proof that \u= Pi_congr_right is a group

[Kevin Buzzard]

hom

[Kevin Buzzard]

OK I see.

[Kevin Buzzard]

@Johan Commelin I didn't think too hard about the module ring thing yet

[Kevin Buzzard]

but one funny thing about type classes is that if the devs deem a structure to be worthy of being called a class

[Kevin Buzzard]

then you are only supposed to ever have one instance of that class

[Kevin Buzzard]

I am not being very precise

[Kevin Buzzard]

I mean that if group is a class, and G is a type, then H1 : group G and H2 : group G are supposed to be equal

[Kevin Buzzard]

because otherwise how can type class inference decide whether you want to use H1 or H2

[Kevin Buzzard]

So if you want more than one group structure on your type G, you have to jettison type classes

[Kevin Buzzard]

This happens in the topological space stuff in Lean -- a topological space is a structure

[Kevin Buzzard]

because Johannes wanted to put more than one topological space on a set so he could partially order them for some reason

[Kevin Buzzard]

But you can't edit the source, so a group is a class, so if there's more than one group structure on G then you have to go it alone

[Johan Commelin]

But there is only one instance of module R R right? So that shouldn't be the problem that Mario was talking about...

[Johan Commelin]

At the same time there could be an instance of module Q R

[Johan Commelin]

Or is that giving a conflict somewhere?

[Kevin Buzzard]

In semilinear algebra I've seen plenty of other ways of making R an R-module, but that's not the point right now ;-)

[Johan Commelin]

Right (-;

[Kevin Buzzard]

Let's have a look at module

[Johan Commelin]

Those shouldn't be instances... for a reason

[Kevin Buzzard]

I can't find it :-)

[Kevin Buzzard]

got it

[Kevin Buzzard]

yes module takes both the ring and the module as parameters

[Kevin Buzzard]

so I don't understand Mario's comment

[Kevin Buzzard]

because modules infer their ring argument from typeclass inference

It's this though

[Johan Commelin]

I'm still confused...

[Kevin Buzzard]

In the definition of module do you see out_param?

[Johan Commelin]

Yes

[Kevin Buzzard]

out_param is a great function, it is the identity function

[Kevin Buzzard]

but behind the scenes in the C++ code, type class inference is affected by out_param

[Johan Commelin]

Ouch... I'm being cheated again

[Kevin Buzzard]

That out_param mean in practice "if you give me a module, I'm going to try and guess the ring"

[Kevin Buzzard]

My guess is that this was written by people with some specific usage in mind, who did not talk to a professional ring theorist beforehand

[Johan Commelin]

So we might get rid of the out_param and hopefully stuff would be better?

[Johan Commelin]

Or will mathlib break?

[Kevin Buzzard]

As you know from the docs

[Kevin Buzzard]

(i.e the chat)

[Johan Commelin]

Haha: docs = logs is now an axiom?

[Kevin Buzzard]

there was some discussion about this at some point

[Kevin Buzzard]

Jan 19th on gitter between Mario and Sebastian

[Kevin Buzzard]

according to my logs

[Johan Commelin]

Ok, gitter is from before my time

[Kevin Buzzard]

I'll quote it

[Kevin Buzzard]

To review, the problem is that the definition:

class module (α : out_param $ Type u) (β : Type v) [out_param $ ring α]
  extends has_scalar α β, add_comm_group β :=
...

leads to a search problem in which ring ?M1 is solved before module ?M1 β, which leads to a loop when there is an instance like [ring A] [ring B] : ring (A x B)
I would like to make lean search for module ?M1 β only, obtaining α and the ring instance by unification
Johannes suggested using {out_param $ ring α} instead of [out_param $ ring α], but then it doesn't work as a typeclass, and all the multiplications etc in the theorem statements break
A possible solution is to skip out_param typeclass search problems until after all the others are solved

***

So the real issue is: You want the elaborator to handle applying a function {A B} [ring A] [module A B] (x : B) : ..., yes...?
Mario Carneiro
@digama0
Jan 19 10:10
yes
Sebastian Ullrich
@Kha
Jan 19 10:10
Where you want it to solve the second instance first, which fixes A and the first instance

[Kevin Buzzard]

Every now and again stuff like this happens and I become convinced that type class inference is too stupid to handle non-trivial maths stuff

[Kevin Buzzard]

There is this diamond catastrophe, today we learn that it doesn't work for things defeq to stuff that works etc etc

[Kevin Buzzard]

It is extremely delicate to get right

[Johan Commelin]

Yeah, I see that (-;

[Johan Commelin]

Anyway, lunch time over here... see you later!

[Kevin Buzzard]

but on the plus side, every time I run into an explicit problem Mario has some workaround

[Kevin Buzzard]

One instance for maps, one for equivs:

[Kevin Buzzard]

instance Pi_lift {γ : Type u} {F : γ → Type u} {G : γ → Type u} [∀ i, add_group (F i)]
[∀ i, add_group (G i)] (H : ∀ i : γ, F i → G i) [∀ i, is_add_group_hom (H i)] :
 is_add_group_hom (Pi_lift_map₁ H) := ⟨λ a b, funext $ λ i,
show H i ((a i) + (b i)) = H i (a i) + H i (b i),
by rw (add (H i))⟩

instance equiv.Pi_congr_right {γ : Type u} {F : γ → Type u} {G : γ → Type u} [∀ i, add_group (F i)]
[∀ i, add_group (G i)] (H : ∀ i : γ, F i ≃ G i) [∀ i, is_add_group_hom (H i)] :
 is_add_group_hom (equiv.Pi_congr_right H) := ⟨λ a b, funext $ λ i,
 show H i ((a i) + (b i)) = H i (a i) + H i (b i),
by rw (add (H i))⟩

[Kevin Buzzard]

same proof

[Kevin Buzzard]

unsurprising because equivs are maps

[Kevin Buzzard]

[I'm in namespace is_add_group_hom]

[Kevin Buzzard]

but apparently I need both instances

[Kevin Buzzard]

I guess one thing I am unclear about is what is wrong with the following fix : I create a mathlib PR which adds the function Pi_lift_map₁ H which sends a product of maps to a map on the product and rewrites equiv.Pi_congr_right to use this function. I then delete my second instance and observe that type class inference should spot it. But Mario, I think, suggested that this would not work either.

[Kevin Buzzard]

and oh wow I now have my type class inference working, my time-out was indeed caused by type class inference failing, it now doesn't fail, and I can feed my parameters into my functions :-) So finally my initial problem is solved in the best possible way!

[Kevin Buzzard]

I want to argue that this is all about transport of structure. I'm switching to the canonical thread.

[Mario Carneiro]

You don't need to reprove the theorem

[Kenny Lau]

why is everyone using "reprove" to mean "prove again" lol

[Mario Carneiro]

just define the equiv.Pi_congr_right instance to equal Pi_lift

[Johan Commelin]

and oh wow I now have my type class inference working, my time-out was indeed caused by type class inference failing, it now doesn't fail, and I can feed my parameters into my functions :-) So finally my initial problem is solved in the best possible way!

Does it also solve your max_depth problem?

[Kevin Buzzard]

unfortunately not, but I don't know what other terrible type class sins I have committed.