Dangerous instance

Stream: new members

[Heather Macbeth]

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]

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

[Johan Commelin]

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

[Johan Commelin]

That's "dangerous".

[Heather Macbeth]

Ahh.

[Johan Commelin]

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

[Heather Macbeth]

Oh, really? I used norm_pos_iff in my proof.

[Heather Macbeth]

Is algebra_map required to be injective in mathlib?

[Heather Macbeth]

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]

Ooh wait... I'm silly.

[Johan Commelin]

It doesn't work with just fields.

[Heather Macbeth]

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

[Patrick Massot]

I think we really don't want this instance.

[Patrick Massot]

It could be a local instance in some situations.

[Heather Macbeth]

OK, then I will just prove the lemma zero_ne_one

[Johan Commelin]

@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]

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]

Aaah, then just do what it says (-;

[Johan Commelin]

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

[Heather Macbeth]

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

[Patrick Massot]

It is a Prop

[Heather Macbeth]

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

[Reid Barton]

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

[Heather Macbeth]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Heather Macbeth]

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]

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

[Heather Macbeth]

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

[Heather Macbeth]

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

[Kevin Buzzard]

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]

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]

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]

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

[Bryan Gin-ge Chen]

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

[Dave]

I will read this now, thanks

[Bryan Gin-ge Chen]

@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]

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]

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

[Dave]

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]

Is there some elaboration that makes sense of this?

[Bryan Gin-ge Chen]

Everything is a term in Lean's type theory.

[Bryan Gin-ge Chen]

Some terms are types and some types are props.

[Dave]

what terms are not types

[Bryan Gin-ge Chen]

1 is not a type.

[Dave]

so things like constants?

[Bryan Gin-ge Chen]

Not necessarily, you can declare type constants.

[Dave]

so 1 could be a type?

[Kevin Buzzard]

types are sets, terms are their elements

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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

[Dave]

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

[Dave]

oh ok @Bryan Gin-ge Chen

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Dave]

right ok this makes sense

[Bryan Gin-ge Chen]

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

[Dave]

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]

That's a different 1 then.

[Dave]

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

[Bryan Gin-ge Chen]

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

[Marc Huisinga]

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

[Marc Huisinga]

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

[Bryan Gin-ge Chen]

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

[Dave]

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

[Kevin Buzzard]

what you are writing has no meaning

[Kevin Buzzard]

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

[Dave]

oops meant equals there

[Dave]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Nicolò Cavalleri]

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

[Johan Commelin]

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

[Johan Commelin]

You can however move algebra R A to the extends

[Nicolò Cavalleri]

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]

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]

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

[Nicolò Cavalleri]

No topological_group, topological_ring

[Johan Commelin]

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

[Johan Commelin]

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]

Ok it make sense

[Nicolò Cavalleri]

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]

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]

Okok

[Johan Commelin]

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

[Nicolò Cavalleri]

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]

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]

Ok thanks I will do that

[Patrick Massot]

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