Zulip Chat Archive

Stream: new members

Topic: type class question


view this post on Zulip Nicolás Ojeda Bär (Oct 12 2019 at 07:13):

Hello! I have some basic mathlib-related questions:
Given a module \beta over a field \alpha where \beta is a ring I want to define the morphism \alpha \to \beta, given by x \mapsto x * 1_\beta.
So I have this:

universes u v
variables (α : Type u) (β : Type v)
variables [field α] [comm_ring β] [module α β]
def struct_hom : α  β := λ x, x  has_one.one β

(some of this may be nonsense!)
I get:

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')

I guess the system has trouble disambiguating some of the terms in the lambda definition. How can I supply the necessary constraints ?
Thanks!

view this post on Zulip Kevin Buzzard (Oct 12 2019 at 07:22):

Hi Nicolas! The problem seems to be here:

import algebra.module

universes u v
variables (α : Type u) (β : Type v)
variables [field α] [comm_ring β] [module α β]

example : has_scalar α β := by apply_instance  -- max instance depth

view this post on Zulip Kevin Buzzard (Oct 12 2019 at 07:25):

Whilst I'm not entirely sure why that's happening, I guess that one problem with the way you're setting things up here is that the alpha-module structure on beta will be completely unrelated to the commutative ring structure (so for example you will not even know that the addition on beta-as-alpha-module equals the addition on beta-as-commutative-ring), which is presumably not what you want.

view this post on Zulip Kevin Buzzard (Oct 12 2019 at 07:26):

There is already a theory of alpha-algebras which solves this problem and you probably want to use that.

view this post on Zulip Kevin Buzzard (Oct 12 2019 at 07:30):

import ring_theory.algebra

universes u v
variables (k : Type u) (R : Type v)
variables [field k] [comm_ring R] [algebra k R]

example : has_scalar k R := by apply_instance

def struct_hom : k  R := algebra_map R

view this post on Zulip Kevin Buzzard (Oct 12 2019 at 07:32):

NB when using mathematical objects I am on a crusade to stay away from this alpha beta etc notation and stick to the notation we're used to; initially this was just mathematicians trying to cause trouble but more recently there have been situations where the computer scientists have seen the value of this convention and my impression is that they're coming round to it.

view this post on Zulip Nicolás Ojeda Bär (Oct 12 2019 at 07:32):

Indeed, that makes sense. Thanks for pointing out ring_theory.algebra, I wasn't aware of it.

view this post on Zulip Nicolás Ojeda Bär (Oct 12 2019 at 07:33):

Ah yes, re the notation I would also prefer to use "traditional" notation but I thought the "house style" was to use greek letters for types. Will switch, thanks!

view this post on Zulip Kevin Buzzard (Oct 12 2019 at 07:34):

The house style is that, but mathematicians sort-of rebelled against it and because mathematicians infiltrated the mathlib maintainers it started slipping through into the library.

view this post on Zulip Kevin Buzzard (Oct 12 2019 at 07:35):

I think it's the unique case where mathematicians have suggested a notational change which the CS people could see the merits of. When we started suggesting that they called every lemma something like lemma 13.4 they were adamant that their more expressive system was a much better idea ;-)

view this post on Zulip Patrick Massot (Oct 12 2019 at 08:29):

Since https://github.com/leanprover-community/mathlib/pull/1521 was merged, this notation victory is official. We should update the style guide though.

view this post on Zulip Nicolás Ojeda Bär (Oct 12 2019 at 08:46):

Follow-up: trying to write down the definition of algebraic number. I have the following

import ring_theory.algebra

universes u v
variables (k : Type u) (R : Type v)
variables [field k] [ring R] [algebra k R]

def is_algebraic (x : R) : Prop :=  (p : polynomial k), polynomial.aeval k R x p = has_zero.zero R

I get :

failed to synthesize type class instance for
k : Type u,
R : Type v,
_inst_1 : comm_ring k,
_inst_2 : ring R,
_inst_3 : algebra k R,
x : R,
p : polynomial k
⊢ comm_ring R

(the error points to polynomial.aeval). What is the error saying ?

view this post on Zulip Patrick Massot (Oct 12 2019 at 08:47):

You declared a ring structure on R, but not a commutative one.

view this post on Zulip Nicolás Ojeda Bär (Oct 12 2019 at 08:48):

Ah, yes. Thanks!

view this post on Zulip Kevin Buzzard (Oct 12 2019 at 09:36):

You should demand that p is monic, to stop p=0 from letting everything be algebraic. And all this has_zero.zero R -- you can just write this as (0 : R). That's exactly the point of the has_zero typeclass -- it is a type class written specifically so that we can use 0 notation.

view this post on Zulip Nicolás Ojeda Bär (Oct 12 2019 at 09:41):

Yes, good point, I was just looking into how best to specify that p is non-zero. And thanks for the tip on the notation!

view this post on Zulip Kevin Buzzard (Oct 12 2019 at 09:46):

If you demand it's non-zero then you will often have to apply a lemma saying "if there's a non-zero poly which works then there's a monic poly which works" because we often say "wlog it's monic". On the other hand if you demand it's monic then you won't have to apply this lemma, but if you are trying to prove a specific thing is algebraic and you only manage to find a non-zero poly, you'll have to apply the lemma above. So you have to make a guess about whether you will say "wlog it's monic" more times than being in a situation where you've constructed a non-zero polynomial which is not obviously monic in a proof that something is algebraic, and in my comment I was implicitly guessing that there will be more wlogs.

view this post on Zulip Kevin Buzzard (Oct 12 2019 at 09:46):

Isn't formalising great ;-)

view this post on Zulip Kevin Buzzard (Oct 12 2019 at 09:48):

In maths we can just say "TFAE: (a) there's a non-zero poly (b) there's a monic poly. We define _algebraic_ to mean both of them". The advantage with this approach is that whichever one you need, you can just say it's true "by definition" :D In formalising you have to choose one of them to be the definition and then you prove the lemma that it's equivalent to the other one and then only some percentage of things are true "by definition" and the trick if you want to write smaller faster code is to maximise this percentage.


Last updated: May 09 2021 at 19:11 UTC