synthesize placeholder

Stream: general

[Heather Macbeth]

I am trying to solve some issues encountered by @Nicolò Cavalleri in #3641, but I also find them tricky. What am I doing wrong here?

import geometry.manifold.smooth_manifold_with_corners

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
variables {𝕜' : Type*} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
variables {E : Type*} [normed_group E] [normed_space 𝕜' E]

def i : normed_space 𝕜 E := normed_space.restrict_scalars 𝕜 𝕜'

#check @model_with_corners 𝕜 _ E _ i E _
example : @model_with_corners 𝕜 _ E _ i E _ := sorry

The #check succeeds, giving model_with_corners 𝕜 E E : Type u_3. The example has a bug somewhere; there is a red underline on the second underscore, with the error message "don't know how to synthesize placeholder ⊢ Type ?".

[Reid Barton]

I don't know this part of the library, but this behavior is not inconsistent. #check allows an expression which still contains metavariables, but a definition (including example) doesn't. As an extreme example, take #check _ vs example : _ := sorry.

[Reid Barton]

In this case the metavariable must appear in one of the implicit arguments of model_with_corners or you would see it displayed in the output of #check.

[Heather Macbeth]

Thank you, that's helpful. I'll experiment.

[Heather Macbeth]

Should the red underlining directly indicate the problematic implicit argument? Or is it more complicated?

[Reid Barton]

It should

[Heather Macbeth]

I think I have found a fix, but I don't really understand it. I noticed the following comment at the definition of docs#normed_space.restrict_scalars :

-- We could add a type synonym equipped with this as an instance,
-- as we've done for `module.restrict_scalars`.

So, acting on a hunch, I rewrote the restrict_scalars section of normed_space along the lines used in docs#module.restrict_scalars , which is rather different. I assume that what I did is adding a type synonym, although the concept is new to me .... And now

#check model_with_corners 𝕜 (normed_space.restrict_scalars 𝕜 𝕜' E) E
example : model_with_corners 𝕜 (normed_space.restrict_scalars 𝕜 𝕜' E) E := sorry

both parse.

It would be great if someone could explain to me why this worked and whether it's a good idea :smiley:

[Heather Macbeth]

@Nicolò Cavalleri, let's see what the experts think of this change. If it's a good idea, then one of us can add it to your branch tomorrow, and then retry the troublesome lemmas.

[Heather Macbeth]

By the way, "worked" might be an overstatement -- to build, I commented out quite a number of uses of the old restrict_scalars, all of which would have to be adjusted.

[Sebastien Gouezel]

Do you have a branch that I could have a look at?

[Heather Macbeth]

@Sebastien Gouezel https://github.com/leanprover-community/mathlib/tree/restrict_scalars_experiment

[Heather Macbeth]

The following snippet runs on top of the branch without errors (except for the sorry):

import geometry.manifold.smooth_manifold_with_corners

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
variables {𝕜' : Type*} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
variables {E : Type*} [normed_group E] [normed_space 𝕜' E]

#check model_with_corners 𝕜 (normed_space.restrict_scalars 𝕜 𝕜' E) E
example : model_with_corners 𝕜 (normed_space.restrict_scalars 𝕜 𝕜' E) E := sorry

[Heather Macbeth]

Whereas, wanting to do the equivalent on standard mathlib, I tried the code in my first post, but kept getting the error "don't know how to synthesize placeholder ⊢ Type ?".

[Heather Macbeth]

By the way, I noticed while making the branch that every use of restrict_scalars in the library is accompanied by a line like

local attribute [instance, priority 500] normed_space.restrict_scalars

Would a line like this have fixed the initial error I had? I'll experiment.

[Heather Macbeth]

OK, so running on top of standard mathlib (not the branch), if I add a local attribute line to my original code, I get a new error:

import geometry.manifold.smooth_manifold_with_corners

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
variables {𝕜' : Type*} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
variables {E : Type*} [normed_group E] [normed_space 𝕜' E]

local attribute [instance, priority 500] normed_space.restrict_scalars

#check model_with_corners 𝕜 E E  -- fine

/- maximum class-instance resolution depth has been reached (the limit can be increased by setting option
'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option
'trace.class_instances') -/
example : model_with_corners 𝕜 E E := sorry

I tried adding lines like

set_option class.instance_max_depth 1000

to the file but the error stays the same.

[Sebastien Gouezel]

I think it is a very good idea to use also the type synonym in the normed space case (but, contrary to your branch, I don't think it is necessary to introduce a new type synonym: we can still use module.restrict_scalars).

While trying to fix the library with this change, I encounter a situation where I feel I don't know how to convince Lean. The problem is in the following lemma (not a MWE). Here, module.restrict_scalars 𝕜 𝕜' E is a type synonym for E.

lemma has_strict_fderiv_at.restrict_scalars (f : E → F) (h : has_strict_fderiv_at f f' x) :
  has_strict_fderiv_at (f : module.restrict_scalars 𝕜 𝕜' E → module.restrict_scalars 𝕜 𝕜' F)
    (f'.restrict_scalars 𝕜) (x : module.restrict_scalars 𝕜 𝕜' E) :=
h

Lean complains that

type mismatch at application
  has_strict_fderiv_at f (restrict_scalars 𝕜 f')
term
  restrict_scalars 𝕜 f'
has type
  module.restrict_scalars 𝕜 𝕜' E →L[𝕜] module.restrict_scalars 𝕜 𝕜' F
but is expected to have type
  E →L[?m_1] F

because it ignores my type ascription f : module.restrict_scalars 𝕜 𝕜' E → module.restrict_scalars 𝕜 𝕜' F and comes back to f : E → F, so it wants the derivative to be a linear map from E to F.

A way out is to use a let to force the type ascription, as in

lemma has_strict_fderiv_at.restrict_scalars (f : E → F) (h : has_strict_fderiv_at f f' x) :
  let tildef : module.restrict_scalars 𝕜 𝕜' E → module.restrict_scalars 𝕜 𝕜' F := f in
  has_strict_fderiv_at tildef
    (f'.restrict_scalars 𝕜) (x : module.restrict_scalars 𝕜 𝕜' E) :=
h

Is there a more elegant way to proceed?

[Heather Macbeth]

@Sebastien Gouezel, thanks for experimenting, I am also curious to see whether the let can be removed.

Just out of interest, were you able to directly fix my other attempt at the same end goal, using local attribute [instance, priority 500] ?

[Sebastien Gouezel]

I have pushed a branch https://github.com/leanprover-community/mathlib/tree/norm_restrict_scalars in which I have done some work on the normed space structure for the type synonym restrict_scalars. I want to add some stuff to it (notably that differentiability of functions taking values in restrict_scalars k k' E is preserved by multiplication by an element of k', and same thing for continuity, and higher smoothness, and also the specific case of real/complex), but tomorrow. If someone wants to experiment with the branch, don't hesitate to push to it!

[Sebastien Gouezel]

I am convinced that the type synonym approach is better than the local attribute approach, so I have not tried to fix your other attempt, sorry.

[Heather Macbeth]

No problem! I only tried that experiment because I saw other parts of the normed space library using similar declarations, and wondered if it was preferred (over the type synonym method) for some reason.

[Sebastien Gouezel]

I have probably erased all of them in my branch :-) I had started with this approach initially, but since then @Scott Morrison has convinced me that the type synonym approach is better. I had not found the time to switch until now for lack of motivation.

[Heather Macbeth]

I see, thanks!

[Nicolò Cavalleri]

Thanks a lot to both! Is it maybe a good idea to do a separate PR with the branch you're working on and then integrate that into my branch?

[Sebastien Gouezel]

I have just PRed to mathlib a branch in which I prove that multiplying a real function by a complex number respects differentiability (in a more general framework), which if I understand correctly is something you are interested in. See #3731. Note though that it adds a layer of complexity over the simpler situation where one only multiplies by a scalar of the base field, so maybe for your PR it would be wiser to concentrate first on the easier situation, and try to generalize later.