Zulip Chat Archive

Stream: general

Topic: Possible diamond for the reals


Adam Topaz (Aug 17 2022 at 16:53):

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 (Aug 17 2022 at 16:54):

docs#is_absolute_value.uniform_space feels like a bad instance

Eric Wieser (Aug 17 2022 at 16:54):

Oh, but it's not an instance!

Adam Topaz (Aug 17 2022 at 16:55):

It's part of rational_cau_seq_pkg

Adam Topaz (Aug 17 2022 at 16:55):

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

Patrick Massot (Aug 17 2022 at 17:04):

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 (Aug 17 2022 at 17:06):

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

Adam Topaz (Aug 17 2022 at 17:07):

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

Adam Topaz (Aug 17 2022 at 17:08):

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

Adam Topaz (Aug 17 2022 at 17:09):

Or more generally for the absolute value thing

Adam Topaz (Aug 17 2022 at 17:14):

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 (Aug 17 2022 at 17:14):

Maybe a docstsring would indeed suffice for now ;)


Last updated: Dec 20 2023 at 11:08 UTC