# Zulip Chat Archive

## 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".

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

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?

#### Patrick Massot (Jun 28 2020 at 18:22):

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 : ordinals`

instead 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.

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

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.

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

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