Zulip Chat Archive

Stream: maths

Topic: representations


view this post on Zulip Johan Commelin (May 09 2019 at 13:43):

What is going on here? I was playing around with representations together with @Ben McDonnell
After importing linear_algebra.basic a silly lemma broke at the bottom of the quoted code:

import algebra.module
import group_theory.group_action
import linear_algebra.basic -- this import breaks the commented lines at the end of the file

class group_module (G M : Type) [monoid G] [add_comm_group M]
  extends mul_action G M :=
(smul_add  :  (g : G) (m₁ m₂ : M), g  (m₁ + m₂) = g  m₁ + g  m₂)

attribute [simp] group_module.smul_add

namespace fixed_points
open mul_action
variables {G M : Type}
variables [monoid G] [add_comm_group M]
variable [group_module G M]

lemma add_mem (x y : M) (hx : x  fixed_points G M) (hy : y  fixed_points G M) :
  x + y  fixed_points G M :=
begin
  intro g,
  simp only [mem_stabilizer_iff, group_module.smul_add, mem_fixed_points] at *,
  rw [hx, hy],
end

end fixed_points

class representation (G R M : Type) [monoid G] [ring R] [add_comm_group M] [module R M]
  extends group_module G M :=
(smul_comm :  (g : G) (r : R) (m : M), g  (r  m) = r  (g  m))

namespace representation
open mul_action linear_map
variables {G R M : Type}
variables [group G] [ring R] [add_comm_group M] [module R M] [representation G R M]

-- set_option trace.class_instances true

-- lemma smul_mem_fixed_points (r : R) (m : M) (hm : m ∈ fixed_points G M) :
--   r • m ∈ fixed_points G M :=
-- begin
--   simp only [mem_fixed_points] at *,
--   intro g,
--   rw [smul_comm, hm],
-- end
end representation

view this post on Zulip Johan Commelin (May 09 2019 at 13:43):

Without the import the code runs fine. With the import it reports maximum type class error.

view this post on Zulip Mario Carneiro (May 09 2019 at 13:44):

increase depth?

view this post on Zulip Johan Commelin (May 09 2019 at 13:44):

I couldn't figure out which type class it is even searching for. It performs a has_mul search and a mul_action search, and it finds those two instantly.

view this post on Zulip Johan Commelin (May 09 2019 at 13:44):

Bumping the depth to 100 didn't solve it.

view this post on Zulip Johan Commelin (May 09 2019 at 13:46):

@Mario Carneiro Any other ideas?

view this post on Zulip Johan Commelin (May 09 2019 at 13:47):

Modules work a lot better than half a year ago. But they are still pretty fragile, at least that's my impression...

view this post on Zulip Chris Hughes (May 09 2019 at 14:28):

Putting some brackets in lets you see the failing search. It's for has_scalar R M

view this post on Zulip Chris Hughes (May 09 2019 at 14:28):

lemma smul_mem_fixed_points (r : R) (m : M) (hm : m  fixed_points G M) :
  (r  m : M)  fixed_points G M :=
begin
  simp only [mem_fixed_points] at *,
  intro g,
  rw [smul_comm, hm],
end

view this post on Zulip Johan Commelin (May 09 2019 at 14:29):

Thanks @Chris Hughes

view this post on Zulip Johan Commelin (May 09 2019 at 14:29):

Now the question is... why does that import bork the class search

view this post on Zulip Mario Carneiro (May 09 2019 at 14:32):

is Ra discrete field?

view this post on Zulip Mario Carneiro (May 09 2019 at 14:32):

the tc looks for that a lot

view this post on Zulip Johan Commelin (May 09 2019 at 14:32):

Just any ring

view this post on Zulip Mario Carneiro (May 09 2019 at 14:33):

not exactly sure why... I mean it's directly looking for it

view this post on Zulip Johan Commelin (May 09 2019 at 14:33):

There is a module R M staring it in the face

view this post on Zulip Johan Commelin (May 09 2019 at 14:33):

Shouldn't be too hard to get a has_scalar R M from that.

view this post on Zulip Mario Carneiro (May 09 2019 at 14:33):

that's not all it's searching for

view this post on Zulip Mario Carneiro (May 09 2019 at 14:35):

it looks for has_scalar R M a bunch, discrete_field R a bunch more, and also discrete_field (M →ₗ[R] M)

view this post on Zulip Johan Commelin (May 09 2019 at 14:35):

That last one is obviously stupid...

view this post on Zulip Mario Carneiro (May 09 2019 at 14:36):

You misunderstand. This is not a garden path it's looking for, it's the initial problem

view this post on Zulip Johan Commelin (May 09 2019 at 14:37):

Hmmm... so how do we fix this?

view this post on Zulip Johan Commelin (May 09 2019 at 14:38):

Are we just hitting limitations of tc search?

view this post on Zulip Mario Carneiro (May 09 2019 at 14:38):

no, this is worse

view this post on Zulip Johan Commelin (May 09 2019 at 14:38):

Wow, ok. I still don't understand the problem

view this post on Zulip Mario Carneiro (May 09 2019 at 14:38):

it's searching for things that don't make any sense

view this post on Zulip Mario Carneiro (May 09 2019 at 14:38):

it needs has_scalar so that's all it should be looking for

view this post on Zulip Mario Carneiro (May 09 2019 at 14:39):

I don't know why these discrete_field problems are coming up

view this post on Zulip Mario Carneiro (May 09 2019 at 14:41):

oh! I started deleting your definitions beforehand and representation causes the problem

view this post on Zulip Mario Carneiro (May 09 2019 at 14:41):

of course, representation is a bad class

view this post on Zulip Johan Commelin (May 09 2019 at 14:42):

Huh, what's wrong with it?

view this post on Zulip Mario Carneiro (May 09 2019 at 14:42):

class representation (G R M : Type) [monoid G] [ring R] [add_comm_group M] [module R M]
  extends group_module G M

This creates an instance group_module G M <= representation G ?R M and lean gets lost at ring ?R

view this post on Zulip Mario Carneiro (May 09 2019 at 14:43):

you shouldn't extend something with fewer explicit type parameters

view this post on Zulip Johan Commelin (May 09 2019 at 14:44):

Oh boy... that's really bad.

view this post on Zulip Mario Carneiro (May 09 2019 at 14:45):

it's pretty easy to fix:

class representation (G R M : Type) [monoid G] [ring R]
  [add_comm_group M] [module R M] [group_module G M] :=
(smul_comm :  (g : G) (r : R) (m : M), g  (r  m) = r  (g  m))

view this post on Zulip Johan Commelin (May 09 2019 at 14:46):

You know what this means, though

view this post on Zulip Johan Commelin (May 09 2019 at 14:46):

When a mathematician says: Let GG be a finite group, and let VV be a representation over a field KK.

view this post on Zulip Johan Commelin (May 09 2019 at 14:46):

That all fits nicely on one line.

view this post on Zulip Johan Commelin (May 09 2019 at 14:47):

To turn that line into Lean, we all of a sudden need 25 type class assumptions. And only 3 or 4 of them are actually interesting.

view this post on Zulip Johan Commelin (May 09 2019 at 14:47):

Can we have extends'?

view this post on Zulip Mario Carneiro (May 09 2019 at 14:48):

If you need the totality of representations, then you should bundle M, or R or something

view this post on Zulip Johan Commelin (May 09 2019 at 14:48):

Sure, but I don't want that category, yet.

view this post on Zulip Mario Carneiro (May 09 2019 at 14:48):

well, with the parameters pulled out representation is a prop

view this post on Zulip Mario Carneiro (May 09 2019 at 14:49):

it's not quite saying the same thing as your one line

view this post on Zulip Johan Commelin (May 09 2019 at 14:49):

I want extends' that signals to Lean: "Hey, if someone writes variable [representation G R M], please add [add_comm_group M] [module R M] [group_module G M] yourself."

view this post on Zulip Reid Barton (May 09 2019 at 14:49):

you need lean' for extends'

view this post on Zulip Mario Carneiro (May 09 2019 at 14:49):

sebastian proposed that back in the stone age, I don't know what happened to that proposal

view this post on Zulip Johan Commelin (May 09 2019 at 14:56):

Hmmz... I'm really not so happy with stacking all these assumptions on top of each other.

view this post on Zulip Johan Commelin (May 09 2019 at 14:57):

@Mario Carneiro Do you see another solution, except for bundling?

view this post on Zulip Mario Carneiro (May 09 2019 at 14:57):

the problem is that if you describe your structure as data shared between objects then you potentially need one for every subset of objects in the context

view this post on Zulip Mario Carneiro (May 09 2019 at 14:59):

make fewer classes?

view this post on Zulip Johan Commelin (May 09 2019 at 14:59):

group_module is not just some random definition. They are pretty useful gadgets in their own right.

view this post on Zulip Mario Carneiro (May 09 2019 at 15:00):

okay but do you care about them right now?

view this post on Zulip Johan Commelin (May 09 2019 at 15:00):

Not exactly right now

view this post on Zulip Johan Commelin (May 09 2019 at 15:01):

But I somehow thought that refactoring it in later only made things harder

view this post on Zulip Mario Carneiro (May 09 2019 at 15:01):

on the contrary, I think it's best to refactor when you know what you want

view this post on Zulip Johan Commelin (May 09 2019 at 15:02):

Well, I do know that I want every representation to also be a G-module

view this post on Zulip Johan Commelin (May 09 2019 at 15:03):

Kevin has a student who is working on G-modules.

view this post on Zulip Johan Commelin (May 09 2019 at 15:03):

Ben wants to work on representation theory

view this post on Zulip Johan Commelin (May 09 2019 at 15:03):

It would be nice if their work was somewhat compatible at the end of the day...

view this post on Zulip Mario Carneiro (May 09 2019 at 15:05):

I assure you that having written down the definition group_module is nowhere near enough to ensure everyone's work is compatible at the end of the day

view this post on Zulip Johan Commelin (May 09 2019 at 15:05):

Ooh, I believe that.

view this post on Zulip Johan Commelin (May 09 2019 at 15:06):

I was just surprised that having written down two def's and two lemmas already brought the system to its knees

view this post on Zulip Johan Commelin (May 09 2019 at 15:06):

I now understand the error

view this post on Zulip Johan Commelin (May 09 2019 at 15:06):

I don't yet see a nice solution.

view this post on Zulip Mario Carneiro (May 09 2019 at 15:06):

the too many classes thing is a slow problem that won't get in your way in the immediate future, so I suggest you go with it for now

view this post on Zulip Sebastien Gouezel (May 12 2019 at 08:54):

you shouldn't extend something with fewer explicit type parameters

What about the existing

class normed_space (α : Type*) (β : Type*) [normed_field α]
  extends normed_group β, vector_space α β :=
(norm_smul :  (a:α) b, norm (a  b) = has_norm.norm a * norm b)

which seems to work pretty well?

view this post on Zulip Mario Carneiro (May 12 2019 at 09:36):

I am pretty sure you can also use that to cook up a bad typeclass search

view this post on Zulip Mario Carneiro (May 12 2019 at 09:36):

it's possible we just haven't run across it by accident yet

view this post on Zulip Mario Carneiro (May 12 2019 at 09:46):

Here's a bad typeclass search example:

import analysis.normed_space.basic

variables {α : Type} (a : α)
set_option trace.class_instances true

def normify : Type  Type := sorry
instance [field α] : normed_field (normify α) := sorry

#check -a

The reason we haven't come across this yet is because normed_field is pretty high in the hierarchy so there aren't many ways to get lower down yet. Here I've made up a perfectly normal instance for some made up normify operator that, in conjunction with normed_space, causes a loop that causes basically every typeclass search to overflow (like has_neg A here)

view this post on Zulip Patrick Massot (May 12 2019 at 10:00):

Mario, do you see a way to modify how type class search works that would solve this issue? Or is it the concept of type class itself that is irremediably broken and we should switch everything to unification hints?

view this post on Zulip Mario Carneiro (May 12 2019 at 10:02):

not typeclass search per se, but "prolog-like" needs some tweaking to make it not quite so stupid in some cases, i.e. loop detection and some forward inference

view this post on Zulip Patrick Massot (May 12 2019 at 10:03):

Is this something you could play with in the fork?

view this post on Zulip Patrick Massot (May 12 2019 at 10:04):

It's such a fundamental part of Lean that, to me, it looks much more important to fix than VM override or FFI or pretty much anything else

view this post on Zulip Mario Carneiro (May 12 2019 at 10:04):

possibly... It's a really hard problem in general though, and lots and lots of words have been spent on it, months of peoples' work can gone into proposals and alterations and no one has found that silver bullet yet

view this post on Zulip Patrick Massot (May 12 2019 at 10:05):

But prolog itself isn't so dumb, right? Why can't we look at what they do there?

view this post on Zulip Mario Carneiro (May 12 2019 at 10:06):

It's such a fundamental part of Lean that, to me, it looks much more important to fix

the problem with fixing fundamental things is that everything else has to adapt

view this post on Zulip Mario Carneiro (May 12 2019 at 10:06):

there is a high cost of switching and only a vague promise of something better on the other end

view this post on Zulip Patrick Massot (May 12 2019 at 10:07):

also it looks like this is not something that is currently worked on in the Lean 4 repository, so maybe there is hope to contribute some battle tested idea in this direction. Whereas things related to programming are clearly worked on by Leo and Sebastian, so everything done in the fork will be erased

view this post on Zulip Mario Carneiro (May 12 2019 at 10:07):

Prolog gives more mechanisms for being able to control how the search goes. For example you can say "no backtracking past this point"

view this post on Zulip Mario Carneiro (May 12 2019 at 10:08):

typeclasses are essential to lean. If you think you can sneak a change to it past leo I think you are mistaken

view this post on Zulip Patrick Massot (May 12 2019 at 10:08):

Who said "sneak"? Of course you don't want to sneak anything

view this post on Zulip Mario Carneiro (May 12 2019 at 10:09):

Meaning, you have to be working in conjunction with leo on the stuff

view this post on Zulip Patrick Massot (May 12 2019 at 10:09):

I wrote "contribute a battle tested idea"

view this post on Zulip Mario Carneiro (May 12 2019 at 10:09):

so unless he's interested in such a collaboration there's no chance of it happening in lean 4

view this post on Zulip Mario Carneiro (May 12 2019 at 10:09):

or if he does something himself

view this post on Zulip Mario Carneiro (May 12 2019 at 10:12):

also, nothing in the fork will be erased. I'm not sure exactly what will happen, but there is no way I am going to accept a regression like that

view this post on Zulip Mario Carneiro (May 12 2019 at 10:13):

"replaced with something better" is okay, "deleted with no alternatives" is not

view this post on Zulip Patrick Massot (May 12 2019 at 10:14):

Sure, you'll be able to continue using the fork if you want. But I guess most users will switch to Lean 4. And when I write "erased", I mean from the point of view of users. Nothing will be erased in the sense that the repository will still be there.

view this post on Zulip Patrick Massot (May 12 2019 at 10:15):

Leo doesn't have to care about that fork, he won't have to "delete" anything, he can simply and rightfully ignore it

view this post on Zulip Mario Carneiro (May 12 2019 at 10:16):

we still have to deal with integrating lean 4 and mathlib. That's not an easy task, and by the end of it we will probably know what the answer to this is

view this post on Zulip Mario Carneiro (May 12 2019 at 10:20):

Lean 4 promises to put a lot more into lean code that we can modify. If all the stuff in the fork is now in lean, then the contents of it can simply move to mathlib

view this post on Zulip Patrick Massot (May 12 2019 at 10:22):

I guess type class inference will stay C++ forever, it's a performance critical mission

view this post on Zulip Mario Carneiro (May 12 2019 at 10:23):

possibly

view this post on Zulip Mario Carneiro (May 12 2019 at 10:23):

lean is compiled now, maybe it can be made to work

view this post on Zulip Mario Carneiro (May 12 2019 at 10:24):

I don't know if Lean 4 will ever be "open for business" as in accepting issues or PRs. It's really hard to tell if that was just a phase of lean 3 during the transition, or if that's the new normal

view this post on Zulip Mario Carneiro (May 12 2019 at 10:24):

but I think the fork has a reason to exist at least until that day

view this post on Zulip Kevin Buzzard (May 12 2019 at 12:10):

Leo told me

Sebastian and I have a few ideas on how to improve the typeclass inference procedure, but we didn't get there yet. We are currently working on the new compiler, parser and expander.

From what Mario says, the whole thing sounds extremely delicate.


Last updated: May 12 2021 at 06:14 UTC