## Stream: maths

### Topic: out_param again

#### 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

#### Sebastien Gouezel (Mar 05 2019 at 09:32):

Are you going after the inverse function theorem?

#### 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?

#### Kevin Buzzard (Mar 05 2019 at 09:36):

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

#### Johan Commelin (Mar 05 2019 at 09:36):

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

#### 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


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

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

#### Patrick Massot (Mar 05 2019 at 10:02):

@Kevin Buzzard Yes I want Lean to find alpha

#### 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

#### Patrick Massot (Mar 05 2019 at 19:52):

Can anyone help me in this thread?

#### Patrick Massot (Mar 05 2019 at 19:53):

@Mario Carneiro maybe?

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

#### 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

#### Jan-David Salchow (Mar 07 2019 at 11:50):

Maybe some of it is useful in your efforts?

#### 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" :-)

#### 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

#### 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?

#### 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?

#### 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

#### Mario Carneiro (Mar 07 2019 at 15:59):

actually just take all the out_params off

#### Mario Carneiro (Mar 07 2019 at 15:59):

module doesn't work like that anymore

#### 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⟩


#### 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

#### 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

#### Patrick Massot (Mar 07 2019 at 16:02):

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

#### Patrick Massot (Mar 07 2019 at 16:03):

But not using add_comm_group was really stupid indeed

#### Mario Carneiro (Mar 07 2019 at 16:04):

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

#### 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

#### Patrick Massot (Mar 07 2019 at 16:06):

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

oh you found it

#### 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

#### Patrick Massot (Mar 07 2019 at 16:07):

I must admit I used nonempty and inhabited interchangeably

#### Patrick Massot (Mar 07 2019 at 16:12):

So should I replace all by inhabited by nonempty?

#### Patrick Massot (Mar 07 2019 at 16:12):

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

#### 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

Why is that?

#### Patrick Massot (Mar 07 2019 at 16:25):

Is Lean missing something fundamental here?

#### Mario Carneiro (Mar 07 2019 at 16:26):

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

#### Mario Carneiro (Mar 07 2019 at 16:27):

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

#### Patrick Massot (Mar 07 2019 at 16:28):

It appears in the instance for E

#### Mario Carneiro (Mar 07 2019 at 16:34):

instances don't get pulled in unless the types are

#### 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

#### 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

#### 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

#### Patrick Massot (Mar 07 2019 at 16:42):

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

#### Patrick Massot (Mar 07 2019 at 16:42):

But I understand this is hopeless

#### Mario Carneiro (Mar 07 2019 at 16:43):

it gets pulled in the theorem but not in the use

#### 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

#### 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?

#### Mario Carneiro (Mar 07 2019 at 16:47):

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

#### Patrick Massot (Mar 07 2019 at 16:51):

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