continuous class

Stream: maths

[Patrick Massot]

Should we turn continuous into a class is_continuous like we did for group homorphisms? I spent quite a lot of time explicitly invoking lemmas that could be handled by type class inference. Same question for uniform continuity.

[Johan Commelin]

I think this is a very good idea. It's longhigh (thanks, Kenny) time it is turned in to a class.

[Kevin Buzzard]

Should we turn everything which returns a proposition into a class? There will be no diamonds! Why is this not a no-brainer? Johannes wrote def continuous (f : α → β) := ∀s, is_open s → is_open (f ⁻¹' s) in analysis/topology/continuity.lean so he has chosen to make a definition, and he knows what he's doing. Patrick is proposing instead using a class, but propositions are useful sometimes. But you could make the class a proposition, right? @Johannes Hölzl why is this not a class "by default"?

[Patrick Massot]

About what Johannes wrote: I think this was a very long time ago and maybe it wasn't a conscious decision (for me everything written before I started using Lean is ancient).

[Johannes Hölzl]

continuous needs to stay a definition, otherwise a lot of proofs break. I would prefer to use apply_rules and maybe auto_param instead of type classes. The problem with the type class mechanism is that it doesn't handle composition of functions very well. I'm still not sure if using the type class mechanism to handle morphisms is a good idea.

[Kevin Buzzard]

This is interesting -- I don't understand this at all. It certainly sounds like a proof that not everything which is a proposition should be handled by the type class inference system! So the issue is the instance corresponding to "if f and g are continuous then so is f o g" is poorly behaved? Why is this any different to "if G and H are groups then so is G x H"?

[Kevin Buzzard]

Is it the difference between f ∘ g and λ x, f (g x)?

[Johannes Hölzl]

the type class mechanism needs to be very fast, and it is often very annoying if one wants to force a specific type class instance (i.e. writing it down using @t A _inst1 ...). So, yes: many things shouln't be type class instances.

[Patrick Massot]

Ok, I'll try playing with apply_rules (I had no luck with apply_rules and tendsto so I'm not very optimistic)

[Johannes Hölzl]

Hm, yes we might have the same problem

[Reid Barton]

Yes, I had the same experiences.

• I tried making a type class is_continuous but I couldn't get inference to work in even some simple cases, I think involving function composition. But it's possible I didn't set things up quite right. Does the type class work well for group homomorphisms? I haven't had occasion to use that.

• I've been happy with a tactic which just repeatedly tries to apply continuous.comp and continuous_fst and so on. But it doesn't work to literally use apply. Possibly the reason is that continuous is a Pi type and this causes apply to guess the wrong number of _s to insert (I think Mario explained this once). Anyways it works fine to use refine and manually specify the correct number of arguments.

[Reid Barton]

What I'm currently using: https://gist.github.com/rwbarton/d088776fa881a00c6820a02d14c5c9e0
It's based on (a somewhat old version at this point of) Scott's tidy library.