Zulip Chat Archive

Stream: maths

Topic: out_param again


view this post on Zulip Patrick Massot (Mar 05 2019 at 09:26):

There are things I understand better after one year of Lean. But out_param is not among those. At https://gist.github.com/PatrickMassot/3c40ee89b1f0329432060e257c7e7cf3 does anyone know how to make Lean happy on line 105, without using the commented line 106? This is a standalone file that works with current mathlib

view this post on Zulip Sebastien Gouezel (Mar 05 2019 at 09:32):

Are you going after the inverse function theorem?

view this post on Zulip Kevin Buzzard (Mar 05 2019 at 09:34):

I'm on commit 05449a061744f8142bfc5396184e33ef19b08b82 from under a week ago and it doesn't compile for me -- do I need to update mathlib?

view this post on Zulip Kevin Buzzard (Mar 05 2019 at 09:36):

fixed with a sorry. What does id - u mean?

view this post on Zulip Johan Commelin (Mar 05 2019 at 09:36):

Probably... the topology of the topology/ directory changed a bit.

view this post on Zulip Kevin Buzzard (Mar 05 2019 at 09:38):

Patrick's error without the @ is

don't know how to synthesize placeholder
⊢ out_param (Type ?)

and his function with the out_params is

lipschitz_global_inverse :
  Π {α : out_param (Type u_3)} [_inst_1 : out_param (normed_field α)] {E : Type u_4} [B : banach_space α E],
    (E → E) → E → E

view this post on Zulip Kevin Buzzard (Mar 05 2019 at 09:40):

So you promised Lean that alpha would be inferred using unification, but it couldn't do it.

view this post on Zulip Kevin Buzzard (Mar 05 2019 at 09:44):

variables {α : out_param $ Type*} [out_param $ normed_field α]

So you have u : E -> E, and you want Lean to spot banach_space α E using type class inference and then realise that clearly you want α in that missing first slot.

view this post on Zulip Patrick Massot (Mar 05 2019 at 10:02):

@Kevin Buzzard Yes I want Lean to find alpha

view this post on Zulip Patrick Massot (Mar 05 2019 at 10:03):

@Sebastien Gouezel Yes, I'm going after the inverse function theorem. I was hoping that @Jeremy Avigad would give the mean value inequality while I was preparing on the Lipschitz side. But it looks like I'll also have to do the mean value inequality

view this post on Zulip Patrick Massot (Mar 05 2019 at 19:52):

Can anyone help me in this thread?

view this post on Zulip Patrick Massot (Mar 05 2019 at 19:53):

@Mario Carneiro maybe?

view this post on Zulip Jeremy Avigad (Mar 06 2019 at 01:16):

The MVT doesn't look too bad. I will put it next on my list, though I can't promise to do it soon. (@Patrick Massot if you do it let me know.)

view this post on Zulip Jan-David Salchow (Mar 07 2019 at 11:48):

@Patrick Massot I was toying with the idea of implementing the inverse/implicit function theorem in the style of McDuff/Salamon. While I haven't done that, I did implement the necessary Newton Picard iteration in the version of Audin / Damian, see https://github.com/jdsalchow/mathlib/blob/newton_picard/src/analysis/normed_space/newton_picard.lean

view this post on Zulip Jan-David Salchow (Mar 07 2019 at 11:50):

Maybe some of it is useful in your efforts?

view this post on Zulip Kevin Buzzard (Mar 07 2019 at 12:35):

notation `∃!` binders `,` p:(scoped P, P) `,` `moreover` q:(scoped Q, Q) := exists_unique p ∧ ∀ x, p x → q x`

"moreover" :-)

view this post on Zulip Patrick Massot (Mar 07 2019 at 13:12):

@Jan-David Salchow Nice! I'm pretty sure that main proof can be mathlib'ed. I can't spend too much time on this right now, because have exams to prepare and I promised to work on uniform spaces. We definitely need some coordination about the basic definitions, like lipschitz_within_with that I also defined in my file, and the space of differentiable functions that you defined. There are very basic questions not yet adressed in deriv.lean, like: do we want to talk about the derivative of f for any f, getting junk if f has no derivative, or do we want bundled differentiable maps like you did? How do we define C^k functions? C^infinity? @Jeremy Avigad should tell us what he thinks here

view this post on Zulip Patrick Massot (Mar 07 2019 at 13:14):

That being said, I'm still interested in the question that started this thread. Can anyone help me here?

view this post on Zulip Patrick Massot (Mar 07 2019 at 15:58):

There are things I understand better after one year of Lean. But out_param is not among those. At https://gist.github.com/PatrickMassot/3c40ee89b1f0329432060e257c7e7cf3 does anyone know how to make Lean happy on line 105, without using the commented line 106? This is a standalone file that works with current mathlib

@Mario Carneiro could you help me here?

view this post on Zulip Mario Carneiro (Mar 07 2019 at 15:59):

To play well with the rest of the module hierarchy, you should take the out_param off alpha

view this post on Zulip Mario Carneiro (Mar 07 2019 at 15:59):

actually just take all the out_params off

view this post on Zulip Mario Carneiro (Mar 07 2019 at 15:59):

module doesn't work like that anymore

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:00):

instance inhabited_vector_space {k : Type*} {α : Type*}
  [discrete_field k] [add_comm_group α] [vector_space k α] : inhabited α := 0

this is a bad idea

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:01):

you don't even need all this stuff about k but it's going to make typeclass search get lost

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:02):

this should just say that an add_comm_group is inhabited... and it should be a local instance

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:02):

Thanks! The instance was trying to avoid the generic has_zero implies inhabited

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:03):

But not using add_comm_group was really stupid indeed

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:04):

why do you even need this? Is it something about inv_fun_on or something?

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:06):

In your definition of fixed_point you use nonempty, but for the properties you use inhabited. This seems reverse of what I would expect

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:06):

https://gist.github.com/PatrickMassot/3c40ee89b1f0329432060e257c7e7cf3#file-out_param_hell-lean-L48

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:06):

oh you found it

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:06):

If you are okay with using nonempty for fixed_point (and going classical), then you should use nonempty for the properties too

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:07):

I must admit I used nonempty and inhabited interchangeably

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:12):

So should I replace all by inhabited by nonempty?

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:12):

I tried removing all out_param, but Lean still does not find my base field

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:22):

Lean won't find the base field unless you include it in your functions, like a normal type

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:24):

Why is that?

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:25):

Is Lean missing something fundamental here?

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:26):

concretely, that means alpha should be explicit in lipschitz_with_translate and lipschitz_global_inverse

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:27):

Lean can't infer alpha, it appears nowhere in the theorem

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:28):

It appears in the instance for E

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:34):

instances don't get pulled in unless the types are

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:39):

Consider the point of application of your definition, lipschitz_global_inverse u. Lean knows u : E -> E, and knows the result has type E -> E, but nothing else tells it what α could be

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:40):

lean knows that E is a banach space over the local α, but doesn't know if this should be the same α that is used in the theorem

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:42):

long story short, this is just standard explicitness rules. Usually types appear as dependencies in further arguments, so they are usually implicit. In this case alpha is never used, so it has to be explicit

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:42):

This instance is pulled in, but it's not enough

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:42):

But I understand this is hopeless

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:43):

it gets pulled in the theorem but not in the use

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:45):

This is the effect of the out_param. Before, with out_param, this could be inferred because you have an order like u known -> E known -> B : banach_space ? E searched to determine α -> α known. Now you have u known -> E known -> no typeclass search because α unknown -> fail

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:46):

Or are you going to promise to me that a banach space will never have two scalar fields?

view this post on Zulip Mario Carneiro (Mar 07 2019 at 16:47):

I will remind you that this is why we don't use out_param here anymore

view this post on Zulip Patrick Massot (Mar 07 2019 at 16:51):

I certainly want complex banach spaces to be also real banach spaces

view this post on Zulip Patrick Massot (Mar 08 2019 at 09:28):

One more question about this: Mario, do you mean https://github.com/leanprover-community/mathlib/blob/master/src/analysis/normed_space/basic.lean#L327 should not have out_param anymore?


Last updated: May 12 2021 at 06:14 UTC