Zulip Chat Archive

Stream: new members

Topic: Dangerous instance


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 28 2020 at 17:11):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 28 2020 at 17:11):

That's "dangerous".

view this post on Zulip Heather Macbeth (Jun 28 2020 at 17:12):

Ahh.

view this post on Zulip 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.)

view this post on Zulip Heather Macbeth (Jun 28 2020 at 17:12):

Oh, really? I used norm_pos_iff in my proof.

view this post on Zulip Heather Macbeth (Jun 28 2020 at 17:13):

Is algebra_map required to be injective in mathlib?

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 28 2020 at 17:21):

Ooh wait... I'm silly.

view this post on Zulip Johan Commelin (Jun 28 2020 at 17:22):

It doesn't work with just fields.

view this post on Zulip Heather Macbeth (Jun 28 2020 at 17:31):

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

view this post on Zulip Patrick Massot (Jun 28 2020 at 17:33):

I think we really don't want this instance.

view this post on Zulip Patrick Massot (Jun 28 2020 at 17:33):

It could be a local instance in some situations.

view this post on Zulip Heather Macbeth (Jun 28 2020 at 17:34):

OK, then I will just prove the lemma zero_ne_one

view this post on Zulip 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.

view this post on Zulip 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 -/

view this post on Zulip Johan Commelin (Jun 28 2020 at 17:42):

Aaah, then just do what it says (-;

view this post on Zulip Johan Commelin (Jun 28 2020 at 17:42):

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

view this post on Zulip Heather Macbeth (Jun 28 2020 at 18:18):

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

view this post on Zulip Patrick Massot (Jun 28 2020 at 18:22):

It is a Prop

view this post on Zulip 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?

view this post on Zulip Reid Barton (Jun 28 2020 at 18:28):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 28 2020 at 20:21):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Jun 28 2020 at 20:37):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Dave (Jun 28 2020 at 20:54):

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

view this post on Zulip 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/

view this post on Zulip Dave (Jun 28 2020 at 20:57):

I will read this now, thanks

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Dave (Jun 28 2020 at 21:04):

Is there some elaboration that makes sense of this?

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 21:04):

Everything is a term in Lean's type theory.

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 21:05):

Some terms are types and some types are props.

view this post on Zulip Dave (Jun 28 2020 at 21:06):

what terms are not types

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 21:06):

1 is not a type.

view this post on Zulip Dave (Jun 28 2020 at 21:06):

so things like constants?

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 21:07):

Not necessarily, you can declare type constants.

view this post on Zulip Dave (Jun 28 2020 at 21:07):

so 1 could be a type?

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 21:07):

types are sets, terms are their elements

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 21:07):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Dave (Jun 28 2020 at 21:08):

oh ok @Bryan Gin-ge Chen

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 21:09):

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

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 21:09):

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

view this post on Zulip Dave (Jun 28 2020 at 21:09):

right ok this makes sense

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 21:10):

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

view this post on Zulip 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 = {{}} ?

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 21:11):

That's a different 1 then.

view this post on Zulip Dave (Jun 28 2020 at 21:12):

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

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Jun 28 2020 at 21:14):

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

view this post on Zulip Marc Huisinga (Jun 28 2020 at 21:15):

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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 21:15):

what you are writing has no meaning

view this post on Zulip Kevin Buzzard (Jun 28 2020 at 21:16):

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

view this post on Zulip Dave (Jun 28 2020 at 21:16):

oops meant equals there

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 13 2020 at 16:49):

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

view this post on Zulip Nicolò Cavalleri (Jul 13 2020 at 17:37):

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

view this post on Zulip Johan Commelin (Jul 13 2020 at 17:38):

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

view this post on Zulip Johan Commelin (Jul 13 2020 at 17:38):

You can however move algebra R A to the extends

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 13 2020 at 17:42):

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

view this post on Zulip Nicolò Cavalleri (Jul 13 2020 at 17:43):

No topological_group, topological_ring

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Nicolò Cavalleri (Jul 13 2020 at 17:44):

Ok it make sense

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Nicolò Cavalleri (Jul 13 2020 at 17:50):

Okok

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Nicolò Cavalleri (Jul 17 2020 at 11:37):

Ok thanks I will do that

view this post on Zulip 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