Possible diamond for the reals

Stream: general

[Adam Topaz]

This came up as part of a discussion in another thread -- a possible diamond in the uniform space structure of the reals:

import topology.uniform_space.compare_reals

example (f : ℝ → ℝ) (h1 : continuous f) (h2 : ∀ q : ℚ, f q = q) :
  ∀ x : ℝ, f x = x :=
begin
  intros x,
  have := rational_cau_seq_pkg.induction_on x, -- error on this line
  sorry
end

Error message:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  pseudo_metric_space.to_uniform_space
inferred
  is_absolute_value.uniform_space abs

[Eric Wieser]

docs#is_absolute_value.uniform_space feels like a bad instance

[Eric Wieser]

Oh, but it's not an instance!

[Adam Topaz]

It's part of rational_cau_seq_pkg

[Adam Topaz]

Okay, maybe not a diamond, but this makes rational_cau_seq_pkg fairly unusable.

[Patrick Massot]

To be honest, rational_cau_seq_pkg isn't meant to be usable. It's a leaf declaration whose only purpose is to be a consistency check.

[Jireh Loreaux]

Regardless of this (non?)diamond, can we put that statement, or something like it, in the docstring?

[Adam Topaz]

I think it should be a fairly easy fix, but I won't have time to do it myself today.

[Adam Topaz]

One should just use the uniform space structure on $\mathbb{Q}$ arising from the metric space structure, instead of this bespoke one.

[Adam Topaz]

Or more generally for the absolute value thing

[Adam Topaz]

Oh, this uniform space structure coming from an absolute value is more general, but it should still be possible to make them defeq

[Adam Topaz]

Maybe a docstsring would indeed suffice for now ;)