Lean doesn't know how to synthesize an implicit argument

Stream: new members

[Michael Novak]

I'm defining the following structures:

--the type of parametrized curves of class Cʳ on the interval I
structure paramCurve (ι : Type*) [Fintype ι] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞) where
  toFun : ℝ → EuclideanSpace ℝ ι
  contDiff_toFun_on : ContDiffOn ℝ r toFun I

structure diffParamCurve (ι : Type*) [Fintype ι] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞)
  {once_diff : 1 ≤ r} extends paramCurve ι I r

structure regularParamCurve (ι : Type*) [Fintype ι] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞)
  {once_diff : 1 ≤ r} extends diffParamCurve ι I r where
  regular : ∀ t : I, deriv toFun t ≠ 0

but I'm getting an error on the definition of the last structure:

don't know how to synthesize implicit argument `once_diff`
  @diffParamCurve ι inst✝¹ I ⋯ r ⋯
context:
ι : Type u_1
inst✝¹ : Fintype ι
I : Set ℝ
inst✝ : I.OrdConnected
r : WithTop ℕ∞
once_diff : 1 ≤ r
⊢ 1 ≤ r

Do you have any suggestion how to solve this?

[Riccardo Brasca]

The usual trick is to use docs#Fact

[Riccardo Brasca]

Like this

import Mathlib

--the type of parametrized curves of class Cʳ on the interval I
structure paramCurve (ι : Type*) [Fintype ι] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞) where
  toFun : ℝ → EuclideanSpace ℝ ι
  contDiff_toFun_on : ContDiffOn ℝ r toFun I

structure diffParamCurve (ι : Type*) [Fintype ι] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞)
  [Fact (1 ≤ r)] extends paramCurve ι I r

structure regularParamCurve (ι : Type*) [Fintype ι] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞)
  [Fact (1 ≤ r)] extends diffParamCurve ι I r where
  regular : ∀ t : I, deriv toFun t ≠ 0

[Riccardo Brasca]

The doc should explain what is going on, but in practice you create a class saying 1 ≤ r. But you can also have it a "normal" assumption

[Riccardo Brasca]

import Mathlib

--the type of parametrized curves of class Cʳ on the interval I
structure paramCurve (ι : Type*) [Fintype ι] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞) where
  toFun : ℝ → EuclideanSpace ℝ ι
  contDiff_toFun_on : ContDiffOn ℝ r toFun I

structure diffParamCurve (ι : Type*) [Fintype ι] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞)
  (once_diff : 1 ≤ r) extends paramCurve ι I r

structure regularParamCurve (ι : Type*) [Fintype ι] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞)
  (once_diff : 1 ≤ r) extends diffParamCurve ι I r once_diff where
  regular : ∀ t : I, deriv toFun t ≠ 0

[Riccardo Brasca]

(if you do so you can make r implicit

[Michael Novak]

Thank you very much! I'll read about this to understand what's going on here

[Riccardo Brasca]

So it really depends if in the applications you have in mind you can expect Lean to find 1 ≤ r automatically or not. For example if you fix r once and for all this can work, but if you have sometimes r and sometimes 2*r then using Fact will make things more complicated.

[Riccardo Brasca]

Anyway the first error is simply Lean saying "I don't find that 1 ≤ r, you put this assumption between {}, so you cannot specify it, but I am not doing anything because you didn't use [] "

[Riccardo Brasca]

Yet another way is

import Mathlib

--the type of parametrized curves of class Cʳ on the interval I
structure paramCurve (ι : Type*) [Fintype ι] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞) where
  toFun : ℝ → EuclideanSpace ℝ ι
  contDiff_toFun_on : ContDiffOn ℝ r toFun I

structure diffParamCurve (ι : Type*) [Fintype ι] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞)
  {once_diff : 1 ≤ r} extends paramCurve ι I r

structure regularParamCurve (ι : Type*) [Fintype ι] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞)
  {once_diff : 1 ≤ r} extends diffParamCurve ι I r (once_diff := once_diff) where
  regular : ∀ t : I, deriv toFun t ≠ 0

but this is almost surely a bad idea

[Riccardo Brasca]

You can read this and this.

[Michael Novak]

My idea was that lean should know by itself to decide whether 1 ≤ r or not, given some r, so probably using square brackets is the best way to do it, right?

[Michael Novak]

I used the first solution you offered for now and after I'll finish reading about this, I'll decide if that's the best solution for my situation

[Riccardo Brasca]

I mean that you cannot expect Lean to find 1 ≤ 2*r having around 1 ≤ r

[Michael Novak]

That's surprising. Right now I don't think I will need to do something like that, but I'll have to see as I continue with project if that will change.

[Riccardo Brasca]

I am not saying it's difficult to prove it (it's actually extremely easy), but square bracket are not meant to be used like that (the point is to realize that if R is a ring that it is also an additive group or something like that)

[Michael Novak]

That makes sense. Do you think that I made a good decision to choose the first solution you proposed?

[Riccardo Brasca]

It really depends on what you think will happens in the rest of the code. The main question is how much r will change. If in a single file you will only consider r (and never 2*r or whatever) then it's most likely the easiest solution. But if r changes a lot (in the sense that you fix r at the beginning, but sometimes you consider 2*r, sometimes 2*r^2+1 ecc) then the second solution is probably better.

[Michael Novak]

O.k, thank you very much! I think I will only consider r in every section, but it's good to also remember the second solution you proposed in case I will see that I will need to also consider more complicated situations.

[Michael Rothgang]

Aside: I'm confused why in diffParamCurve and regularParamCurve, you make r explicit but once_diff implicit. In a theorem statement, I would expect the opposite. (Does that alone already fix your error?)

[Michael Novak]

Maybe that's a better way to do that. Honestly, I'm just trying to be as general as possible and I try to do what I think is expected in Mathlib. In the textbook I'm working from, the author just assumes always that the parametrized curves are smooth, but I imagine in Mathlib you want to be more general. Btw, do you think these structure definitions are a really bad idea and won't be excepted to Mathlib? I honestly enjoyed creating them, but it seems like this is not the way people in Mathlib write, and if so I probably shouldn't continue writing these definitions and instead try stating the theorems I want to prove more directly.

[Michael Rothgang]

My advice would be to try stating your theorems directly. (And my second advice is to trust Sebastien Gouezel: their opinions are usually very well thought out. Like everybody, they can be wrong, but then you should understand why first.)

[Michael Novak]

O.k, thank you! I'll try to do it and see how it goes.

[Moritz Doll]

Sorry for being late to the party, but I am not sure that docs#Fact is the way to go here. Most use-cases where it is the right solution are where you want to declare instances (for fields or vector spaces) that depend on a parameter (think ZMod or Lp). This is not the case here.
In my opinion a better options would be to omit once_diff and just use it in the theorems when needed. Note that regular implies that toFun is differentiable at each point (but the derivative does not have to be continuous obviously), so you might get away with not using 1 ≤ r for a lot of your theorems.

[Moritz Doll]

Also I think I mentioned this before, but I think your codomain should be an arbitrary normed space, not just EuclideanSpace. If you need finite dimensions or an inner product, then you can use the corresponding type classes and everything will work smoothly for EuclideanSpace.

[Michael Novak]

Moritz Doll said:

Sorry for being late to the party, but I am not sure that docs#Fact is the way to go here. Most use-cases where it is the right solution are where you want to declare instances (for fields or vector spaces) that depend on a parameter (think ZMod or Lp). This is not the case here.
In my opinion a better options would be to omit once_diff and just use it in the theorems when needed. Note that regular implies that toFun is differentiable at each point (but the derivative does not have to be continuous obviously), so you might get away with not using 1 ≤ r for a lot of your theorems.

Thank you very much for the feedback. As of now I don't use these definitions anymore, because I was advised not to create structures for everything and instead state things more directly in the theorems I want to prove. But if I will get to a similar situation, I'll remember your advice, so thank you.

[Michael Novak]

Moritz Doll said:

Also I think I mentioned this before, but I think your codomain should be an arbitrary normed space, not just EuclideanSpace. If you need finite dimensions or an inner product, then you can use the corresponding type classes and everything will work smoothly for EuclideanSpace.

I think you are right, thanks!

[Moritz Doll]

import Mathlib

variable (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E]

--the type of parametrized curves of class Cʳ on the interval I
structure paramCurve (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] (I : Set ℝ)
    [I.OrdConnected] (r : WithTop ℕ∞) where
  toFun : ℝ → E
  contDiff_toFun_on : ContDiffOn ℝ r toFun I

structure regularParamCurve (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] (I : Set ℝ)
    [I.OrdConnected] (r : WithTop ℕ∞) extends paramCurve E I r where
  regular : ∀ t : I, deriv toFun t ≠ 0

(just for completeness, this is what I would have suggested)