out_param again

Stream: maths

[Patrick Massot]

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

[Sebastien Gouezel]

Are you going after the inverse function theorem?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Patrick Massot]

@Kevin Buzzard Yes I want Lean to find alpha

[Patrick Massot]

@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

[Patrick Massot]

Can anyone help me in this thread?

[Patrick Massot]

@Mario Carneiro maybe?

[Jeremy Avigad]

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

[Jan-David Salchow]

@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

[Jan-David Salchow]

Maybe some of it is useful in your efforts?

[Kevin Buzzard]

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

"moreover" :-)

[Patrick Massot]

@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

[Patrick Massot]

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

[Patrick Massot]

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?

[Mario Carneiro]

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

[Mario Carneiro]

actually just take all the out_params off

[Mario Carneiro]

module doesn't work like that anymore

[Mario Carneiro]

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

this is a bad idea

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

But not using add_comm_group was really stupid indeed

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

oh you found it

[Mario Carneiro]

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

[Patrick Massot]

I must admit I used nonempty and inhabited interchangeably

[Patrick Massot]

So should I replace all by inhabited by nonempty?

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

Why is that?

[Patrick Massot]

Is Lean missing something fundamental here?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

It appears in the instance for E

[Mario Carneiro]

instances don't get pulled in unless the types are

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

But I understand this is hopeless

[Mario Carneiro]

it gets pulled in the theorem but not in the use

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

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?