## Stream: new members

### Topic: Dangerous instance

#### Heather Macbeth (Jun 28 2020 at 17:10):

I have read a couple of discussions of "dangerous instance" linter errors, but can't figure out how to fix my specific one (#3210):

instance normed_algebra.to_nonzero {𝕜 : Type*} (𝕜' : Type*) [normed_field 𝕜]
[normed_ring 𝕜'] [h : normed_algebra 𝕜 𝕜'] : nonzero 𝕜' :=
{ zero_ne_one :=
begin
refine (norm_pos_iff.mp _).symm,
rw normed_algebra.norm_one 𝕜 𝕜', norm_num,
end }


What is the problem?

#### Johan Commelin (Jun 28 2020 at 17:11):

@Heather Macbeth There result only mentions k' but the statement also depends on k.

#### Johan Commelin (Jun 28 2020 at 17:11):

So if it tries to prove nonzero k' then it will go on a wild goose chase to find a k.

#### Johan Commelin (Jun 28 2020 at 17:11):

That's "dangerous".

Ahh.

#### Johan Commelin (Jun 28 2020 at 17:12):

(Note that your statement doesn't seem to need anything about normed_*. Just fields and algebras would also work.)

#### Heather Macbeth (Jun 28 2020 at 17:12):

Oh, really? I used norm_pos_iff in my proof.

#### Heather Macbeth (Jun 28 2020 at 17:13):

Is algebra_map required to be injective in mathlib?

#### Heather Macbeth (Jun 28 2020 at 17:15):

I don't actually need this instance, so I can kill it if fixing it is too difficult. But is there a fix?

#### Johan Commelin (Jun 28 2020 at 17:21):

Ooh wait... I'm silly.

#### Johan Commelin (Jun 28 2020 at 17:22):

It doesn't work with just fields.

#### Heather Macbeth (Jun 28 2020 at 17:31):

Is there a change I can make to pass the linter?

#### Patrick Massot (Jun 28 2020 at 17:33):

I think we really don't want this instance.

#### Patrick Massot (Jun 28 2020 at 17:33):

It could be a local instance in some situations.

#### Heather Macbeth (Jun 28 2020 at 17:34):

OK, then I will just prove the lemma zero_ne_one

#### Johan Commelin (Jun 28 2020 at 17:36):

@Heather Macbeth You can replace instance with def, and call it with

haveI : nonzero k' := normed_algebra.to_nonzero k k',


whenever you need it.

#### Heather Macbeth (Jun 28 2020 at 17:40):

Johan, I did actually try replacing instance with def, and got the following linter error:

/- INCORRECT DEF/LEMMA: -/
-- analysis/normed_space/basic.lean
#print normed_algebra.to_nonzero /- is a def, should be a lemma/theorem -/


#### Johan Commelin (Jun 28 2020 at 17:42):

Aaah, then just do what it says (-;

#### Johan Commelin (Jun 28 2020 at 17:42):

I.e., make it lemma instead of def.

#### Heather Macbeth (Jun 28 2020 at 18:18):

OK, I will. Is it really possible to have a lemma of non-Prop type?

It is a Prop

#### Heather Macbeth (Jun 28 2020 at 18:25):

Is this a feature of all structures? Or just specifically of the structure nonzero, which has one field, of type Prop?

#### Reid Barton (Jun 28 2020 at 18:28):

It's only a Prop if there is : Prop written before :=.

#### Heather Macbeth (Jun 28 2020 at 18:29):

This is a little mysterious to me, but if someone can suggest the appropriate section of #tpil, I will read up.

#### Reid Barton (Jun 28 2020 at 18:31):

Oh it's actually not a structure technically, it's defined as an inductive proposition for some reason

class inductive nonempty (α : Sort u) : Prop
| intro (val : α) : nonempty


#### Reid Barton (Jun 28 2020 at 20:21):

whoops I just noticed you were talking about nonzero not nonempty.

#### Reid Barton (Jun 28 2020 at 20:22):

Anyways class nonzero (α : Type u) [has_zero α] [has_one α] : Prop := is also declared to be a Prop.

#### Heather Macbeth (Jun 28 2020 at 20:36):

I think I see; are there many such classes? Like, from the user's point of view [nonempty α] and [ring α] look the same; is ring a Prop?

#### Reid Barton (Jun 28 2020 at 20:37):

No, it can't be because it contains the + and * operations which are data.

#### Heather Macbeth (Jun 28 2020 at 20:39):

OK, this is why when I was discussing subsingleton and unique with @Johan Commelin yesterday, he noted that unique was data.

#### Heather Macbeth (Jun 28 2020 at 20:42):

And why, in the code resulting from that discussion, psum is used for unique but ∨ for subsingleton?

#### Kevin Buzzard (Jun 28 2020 at 20:49):

We are slowly beginning to refactor algebra so that "core" classes like integral_domain are data (they contain the addition, multiplication, 0 and 1) and then there are lots of classes on top called things like is_local_ring R, the idea being that the is tells you what the props are, but then it was decided that local_ring R was smaller, so now you can't tell again.

#### Dave (Jun 28 2020 at 20:51):

Reid Barton said:

No, it can't be because it contains the + and * operations which are data.

I was just looking at this and wondered what is meant here by is/are data? Like they are positive information? How does this work in Lean?

#### Kevin Buzzard (Jun 28 2020 at 20:53):

types and terms live in the Type universe and are data. Theorems and proofs live in the Prop universe and aren't. The difference between add and add_assoc is that add is a definition, so lives on the Type side of things (its output is a number), but add_assoc is a proof, so lives on the Prop side of things.

#### Dave (Jun 28 2020 at 20:54):

Thank you. This was a very good explanation, I think

#### Bryan Gin-ge Chen (Jun 28 2020 at 20:57):

Kevin has a nice recent blog post that's also related: https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/

#### Dave (Jun 28 2020 at 20:57):

I will read this now, thanks

#### Bryan Gin-ge Chen (Jun 28 2020 at 20:58):

@Kevin Buzzard you should announce your blogposts somewhere in this Zulip. I always end up seeing them days or weeks after they come out...

#### Kevin Buzzard (Jun 28 2020 at 21:02):

I tend to announce them on Twitter and the discord -- I think that just an announcement of a blog post is a bit off topic for this site.

#### Bryan Gin-ge Chen (Jun 28 2020 at 21:03):

They're all Lean-related, so I don't see why they'd be off-topic.

#### Dave (Jun 28 2020 at 21:04):

Hey so I was reading the blog post and it says that proofs are terms in type theory, but up there you said that terms were types and proofs were props

#### Dave (Jun 28 2020 at 21:04):

Is there some elaboration that makes sense of this?

#### Bryan Gin-ge Chen (Jun 28 2020 at 21:04):

Everything is a term in Lean's type theory.

#### Bryan Gin-ge Chen (Jun 28 2020 at 21:05):

Some terms are types and some types are props.

#### Dave (Jun 28 2020 at 21:06):

what terms are not types

#### Bryan Gin-ge Chen (Jun 28 2020 at 21:06):

1 is not a type.

#### Dave (Jun 28 2020 at 21:06):

so things like constants?

#### Bryan Gin-ge Chen (Jun 28 2020 at 21:07):

Not necessarily, you can declare type constants.

#### Dave (Jun 28 2020 at 21:07):

so 1 could be a type?

#### Kevin Buzzard (Jun 28 2020 at 21:07):

types are sets, terms are their elements

#### Kevin Buzzard (Jun 28 2020 at 21:07):

1 is not a type because it's not a set

#### Bryan Gin-ge Chen (Jun 28 2020 at 21:08):

When I wrote 1, I meant the term 1 : nat. This is not a type and cannot be made a type.

#### Dave (Jun 28 2020 at 21:08):

that analogy seems kinda reasonable. so a proof is a term of the type prop? is that ok to say?

#### Dave (Jun 28 2020 at 21:08):

oh ok @Bryan Gin-ge Chen

#### Kevin Buzzard (Jun 28 2020 at 21:09):

proof : P and P : Prop, like 1 : real and real : Type

#### Kevin Buzzard (Jun 28 2020 at 21:09):

proof : 2+2=4 and 2+2=4 : Prop

#### Dave (Jun 28 2020 at 21:09):

right ok this makes sense

#### Bryan Gin-ge Chen (Jun 28 2020 at 21:10):

I think I learned most of this from chapters 2+3 of #tpil

#### Dave (Jun 28 2020 at 21:10):

also you said 1 is not a set, but what if you are an evil person and you say something like 1 = {{}} ?

#### Bryan Gin-ge Chen (Jun 28 2020 at 21:11):

That's a different 1 then.

#### Dave (Jun 28 2020 at 21:12):

why because it's something like 1 : ordinalsinstead of 1:nat ?

#### Bryan Gin-ge Chen (Jun 28 2020 at 21:13):

Yeah, basically. Any term can only have one type. So two terms with different types cannot be equal.

#### Marc Huisinga (Jun 28 2020 at 21:14):

there's a very nice picture in hitchhiker's guide to logical verification:
image.png

#### Marc Huisinga (Jun 28 2020 at 21:15):

but i guess whether propositions are types depends on your perspective :)

#### Bryan Gin-ge Chen (Jun 28 2020 at 21:15):

There's a link to the hitchhiker's guide on the website here. I liked it a lot!

#### Dave (Jun 28 2020 at 21:15):

ok I like this image, thanks- also would 1 = {{}} mean that each ordinal is kind of a type on its own?

#### Kevin Buzzard (Jun 28 2020 at 21:15):

what you are writing has no meaning

#### Kevin Buzzard (Jun 28 2020 at 21:16):

this is not set theory, and you cannot make definitions by just writing down sets

#### Dave (Jun 28 2020 at 21:16):

oops meant equals there

#### Dave (Jun 28 2020 at 21:16):

oh ok. I only brought it up because you said types are sets so I thought we could play with sets.

#### Mario Carneiro (Jun 29 2020 at 02:49):

Reid Barton said:

Oh it's actually not a structure technically, it's defined as an inductive proposition for some reason

class inductive nonempty (α : Sort u) : Prop
| intro (val : α) : nonempty


It can't be a structure, because then lean would try to create a projection called val which it can't because of universe restrictions

#### Johan Commelin (Jun 29 2020 at 04:05):

Heather Macbeth said:

OK, this is why when I was discussing subsingleton and unique with Johan Commelin yesterday, he noted that unique was data.

And why, in the code resulting from that discussion, psum is used for unique but ∨ for subsingleton?

Yup, exactly.

#### Nicolò Cavalleri (Jul 13 2020 at 16:13):

I've got a dangerous instance I managed to fix but which I'd still like to understand why is dangerous.
The problem is with the following, placed in topology/module right after the definition of topological module:

/-- A topological algebra, over a semiring which is topological semiring, is an algebra that is
both a topological semimodule and a topological semiring. -/
class topological_algebra (R : Type u) (A : Type v)
[comm_semiring R] [topological_space R]
[topological_space A] [semiring A] [algebra R A]
extends topological_semimodule R A, topological_semiring A : Prop


and the Linter says

/- DANGEROUS INSTANCES FOUND.
These instances are recursive, and create a new type-class problem which will have metavariables.
Possible solution: remove the instance attribute or make it a local instance instead.

Currently this linter does not check whether the metavariables only occur in arguments marked with out_param, in which case this linter gives a false positive.: -/
#print topological_algebra.to_topological_semiring /- The following arguments become metavariables. argument 1: (R : Type u) -/


I don't even know what a metavariable is in this case so I guess I'm looking for a very basic answer

#### Johan Commelin (Jul 13 2020 at 16:26):

Hmm... I'm confused about what is dangerous here... @Gabriel Ebner @Mario Carneiro Could one of you take a look please?

#### Mario Carneiro (Jul 13 2020 at 16:45):

topological_algebra R A has two arguments but has a parent topological_semiring A with only one argument, this is not allowed

#### Mario Carneiro (Jul 13 2020 at 16:46):

because it means that when determining if a type A has topological_semiring A, it will check if topological_algebra ? A which is bad

#### Johan Commelin (Jul 13 2020 at 16:49):

Ooh right, of course... I should have seen this :expressionless:

#### Nicolò Cavalleri (Jul 13 2020 at 17:37):

What is the most common solution to this? Moving topological ring to the hypotheses?

#### Johan Commelin (Jul 13 2020 at 17:38):

Yup... but I understand that this is becoming really bulky

#### Johan Commelin (Jul 13 2020 at 17:38):

You can however move algebra R A to the extends

#### Nicolò Cavalleri (Jul 13 2020 at 17:40):

Yeah the point is that I do not really need the notion of topological_algebra it was just so to make it closer to normal maths, but from a formal point of view one just needs to write down topological_semiring and topological_module so I guess I'll just remove it completely

#### Nicolò Cavalleri (Jul 13 2020 at 17:41):

Johan Commelin said:

You can however move algebra R A to the extends

I would really like to do this but people did not do it in the past for group, ring etc, so I guess they had some reason not to do it

#### Johan Commelin (Jul 13 2020 at 17:42):

What do you mean? ring extends monoid and add_group...

#### Nicolò Cavalleri (Jul 13 2020 at 17:43):

No topological_group, topological_ring

#### Johan Commelin (Jul 13 2020 at 17:43):

I see. That's right. Because it allows for easier mixing of algebraic properties and topological ones.

#### Johan Commelin (Jul 13 2020 at 17:44):

Otherwise we would end up with topological_X for all X in the algebra part of the library. And that's quite a lot.

Ok it make sense

#### Nicolò Cavalleri (Jul 13 2020 at 17:47):

Do you think it'd make sense to have topological_algebra as an abbreviation just as module for semimodule? It's quite useless but probably makes hypotheses clear and forces you not to forget the topological_semiring hypothesis which Lean often does not understand is the correct missing hypothesis from the proof

#### Johan Commelin (Jul 13 2020 at 17:49):

I don't know. At the moment I would just continue without it. If we find out that it really would help, we can always add it later.

Okok

#### Johan Commelin (Jul 13 2020 at 17:50):

Every new concept brings the obligation with it to write an interface for it, and connect it to all related concepts...

#### Nicolò Cavalleri (Jul 17 2020 at 11:19):

Just as a preamble: the following problem arose in geometry but the problem itself has nothing to do with geometry. I believe it is a general problem that probably was probably faced in mathlib many times, so I don't think familiarity with the geometry section of mathlib is necessary to help me here!

I have a new dangerous instance. This time it is the opposite: I know why it is there but I have no idea about how to fix it.
With this definition of Lie_group:

class Lie_group {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {E : Type*} [normed_group E]
[normed_space 𝕜 E] (I : model_with_corners 𝕜 E E) (G : Type*) [topological_space G]
[charted_space E G] [smooth_manifold_with_corners I G] [group G] : Prop :=
(smooth_mul : smooth (I.prod I) I (λ p : G×G, p.1 * p.2))
(smooth_inv : smooth I I (λ a:G, a⁻¹))


I need this instance

instance to_topological_group {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E : Type*} [normed_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E E}
(G : Type*) [topological_space G] [charted_space E G] [smooth_manifold_with_corners I G]
[group G] [h : Lie_group I G] : topological_group G :=
{ continuous_mul := h.smooth_mul.continuous,
continuous_inv := h.smooth_inv.continuous, }


However this produces

#print to_topological_group /- The following arguments become metavariables.
argument 1: {𝕜 : Type u_1}, argument 3: {E : Type u_2}, argument 6: {I : model_with_corners 𝕜 E E} -/


and I really need this instance otherwise I have to write twice every definition applying to topological_group.
If you want a mwe I can produce it easily even if I don't know how having code locally could help, since this is an exclusively conceptual problem.
What can I do?

#### Sebastien Gouezel (Jul 17 2020 at 11:34):

Lie group should take [topological_group G] as an instance parameter in this kind of situation. And you can have another constructor that constructs both the topological structure and the Lie group structure out of a structure called something like Lie_group.core. In the same way that you could construct a topology from a charted space structure, but instead charted spaces take the topology as an instance parameter, but there is a constructor in terms of charted_space_core

#### Nicolò Cavalleri (Jul 17 2020 at 11:37):

Ok thanks I will do that

#### Patrick Massot (Jul 17 2020 at 12:04):

Nicolò, did you watch https://youtu.be/RTfjSlwbKjQ?list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N ? It explains this issue pretty nicely.

Last updated: May 10 2021 at 00:31 UTC