Issue in !4#2702 (Topology.UniformSpace.CompareReals)

Stream: mathlib4

[Arien Malec]

What's the fix for this?:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  PseudoMetricSpace.toUniformSpace
inferred
  AbsoluteValue.uniformSpace AbsoluteValue.abs

Maybe hide the mistaken instance?

[Arien Malec]

Nope:

attribute [-instance] PseudoMetricSpace.toUniformSpace
attribute [-instance] PseudoEMetricSpace.toUniformSpace

changes the message to 'failed to synthesize instance
UniformSpace ℚ'

[Eric Wieser]

Can you add a PR comment on the relevant line of !4#2702?

[Arien Malec]

Done

[Arien Malec]

import Mathlib.Topology.UniformSpace.AbstractCompletion
import Mathlib.Algebra.Order.AbsoluteValue
import Mathlib.Topology.UniformSpace.AbsoluteValue
import Mathlib.Topology.Instances.Rat

def rationalCauSeqPkg : @AbstractCompletion ℚ <| (@AbsoluteValue.abs ℚ _).uniformSpace
    where

demonstrates the issue

[Eric Wieser]

You can't use where for constructors relating to non-canonical instances

[Eric Wieser]

You have to use @AbstractCompletion.mk, and pass (_) as the instance argument

[Eric Wieser]

Lean3 was happy to use unification here, Lean4 will use typeclass search (and then complain that it doesn't unify), unless you force it to not be able to use typeclass search

[Arien Malec]

def rationalCauSeqPkg : AbstractCompletion ℚ := @AbstractCompletion.mk
  (space := ℝ)
  (coe := (RatCast.ratCast : ℚ → ℝ))
  (uniformStruct := by infer_instance)
  (complete := by infer_instance)
  (separation := by infer_instance)
  (uniformInducing := Rat.uniformEmbedding_coe_real.toUniformInducing)
  (dense := Rat.denseEmbedding_coe_real.dense)

[Arien Malec]

Wanted the instance named...

[Eric Wieser]

I think for now you just have to use underscores...

[Arien Malec]

Lean yells if you do that

failed to infer definition type
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed

[Arien Malec]

Now the def compiles, has the expected type, but Lean yells later on when it's used. I think it's an implicit issue, but can't figure out how to supply implicits with dotted notation.

[Arien Malec]

Got it, and it doesn't help. This is the exact analogue of the type on the Lean 3 side:

noncomputable def compareEquiv : Bourbakiℝ ≃ᵤ ℝ :=
  @AbstractCompletion.uniformContinuous_compareEquiv Q uniformSpace bourbakiPkg rationalCauSeqPkg

And errors on rationalCauSeqPkg with:

argument
  rationalCauSeqPkg
has type
  @AbstractCompletion ℚ PseudoMetricSpace.toUniformSpace : Type 1
but is expected to have type
  @AbstractCompletion Q uniformSpace : Type 1

[Arien Malec]

Getting one step closer:

def rationalCauSeqPkg : (@AbstractCompletion ℚ uniformSpace) := AbstractCompletion.mk
  (space := ℝ)
  (coe := (RatCast.ratCast : ℚ → ℝ))
  (uniformStruct := by infer_instance)
  (complete := by infer_instance)
  (separation := by infer_instance)
  (uniformInducing := Rat.uniformEmbedding_coe_real.toUniformInducing)
  (dense := Rat.denseEmbedding_coe_real.dense)

fixes the typing errors later down, but fails on the uniformInducing and dense steps, the former with our friend:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  uniformSpace
inferred
  PseudoMetricSpace.toUniformSpace

The latter with the very confusing

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  toTopologicalSpace
inferred
  toTopologicalSpace

[Arien Malec]

I've gone so far as doing:

(uniformInducing := @UniformEmbedding.toUniformInducing ℚ ℝ uniformSpace _ RatCast.ratCast Rat.uniformEmbedding_coe_real)

which still gives me...

pplication type mismatch
  Rat.uniformEmbedding_coe_real.toUniformInducing
argument
  Rat.uniformEmbedding_coe_real
has type
  @UniformEmbedding ℚ ℝ PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toUniformSpace RatCast.ratCast : Prop
but is expected to have type
  @UniformEmbedding ℚ ℝ uniformSpace PseudoMetricSpace.toUniformSpace RatCast.ratCast : Prop
````

[Arien Malec]

When I turn pp.all true

I get as the type of Rat.uniformEmbedding_coe_real

Rat.uniformEmbedding_coe_real : @UniformEmbedding.{0, 0} Rat Real (@PseudoMetricSpace.toUniformSpace.{0} Rat (@MetricSpace.toPseudoMetricSpace.{0} Rat Rat.instMetricSpaceRat)) (@PseudoMetricSpace.toUniformSpace.{0} Real Real.pseudoMetricSpace) (@RatCast.ratCast.{0} Real Real.ratCast)

[Arien Malec]

The types check out the same on the Lean3 side but it doesn't seem to cause trouble there,

[Arien Malec]

The toTopologicalSpace issue is similar under the microscope of pp.all true

I don't understand the machinery well enough here, but is there a coercion between PseudoMetricSpace.toUniformSpace and ℝ.uniformSpace wanting?

[Arien Malec]

Or something something defeq?

[Kevin Buzzard]

Arien Malec said:

I've gone so far as doing:

(uniformInducing := @UniformEmbedding.toUniformInducing ℚ ℝ uniformSpace _ RatCast.ratCast Rat.uniformEmbedding_coe_real)

which still gives me...

Application type mismatch
  Rat.uniformEmbedding_coe_real.toUniformInducing
argument
  Rat.uniformEmbedding_coe_real
has type
  @UniformEmbedding ℚ ℝ PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toUniformSpace RatCast.ratCast : Prop
but is expected to have type
  @UniformEmbedding ℚ ℝ uniformSpace PseudoMetricSpace.toUniformSpace RatCast.ratCast : Prop

Are these terms defeq? If so it's lean's problem, if not it's our problem.

[Eric Wieser]

Arien Malec said:

Lean yells if you do that

failed to infer definition type
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed

The underscores belong after the := not before

[Arien Malec]

That leads to a different set of issues.

[Arien Malec]

I note that right before this definition we have:

theorem Rat.uniformSpace_eq : (AbsoluteValue.abs : AbsoluteValue ℚ ℚ).uniformSpace = PseudoMetricSpace.toUniformSpace which answers the defeq question

[Patrick Massot]

I'm really sorry I don't have time to help with this. I will have time this week-end if you are still stuck by then.

[Eric Wieser]

Arien Malec said:

That leads to a different set of issues.

I think these issues are the ones you should address. This isn't an unexpected instance diamond or anything, this is just an unusual theorem which mathport doesn't port correctly due to a conscious decision by lean4 to make you spell things the long/ugly way

[Eric Wieser]

We've hit this problem in multiple places before

[Arien Malec]

The issues are worse to be clear. The definition doesn’t compile & doesn’t typecheck in use. I think I just need to tell Lean about the defeq in proof.

[Eric Wieser]

They're not defeq and that's the point of the lemmas I think

[Eric Wieser]

I pushed a fix; the solution was to not change the statement of the def, and do roughly what I described above

[Eric Wieser]

Thanks for finding a better way to force unification than using @foo _ _ (_) x for instance arguments! It seems that using @foo (x := x) has the same effect.

[Eric Wieser]

(as a reminder, @foo _ _ _ x is not the same as @foo _ _ (_) x when it comes to elaborating the last underscore)

[Arien Malec]

Eric Wieser said:

Thanks for finding a better way to force unification than using @foo _ _ (_) x for instance arguments! It seems that using @foo (x := x) has the same effect.

I just borrowed the usual lawful monad fixes. Even a blind squirrel finds a nut.