t2_space

Stream: maths

[Reid Barton]

This is producing a "maximum class-instance resolution depth has been reached" error: it used to work.

import analysis.topology.continuity analysis.real
noncomputable theory
def interval : Type := subtype {r : ℝ | 0 ≤ r ∧ r ≤ 1}
instance : topological_space interval := by unfold interval; apply_instance
set_option trace.class_instances true
instance : t2_space interval := by dunfold interval; apply_instance

[Kevin Buzzard]

Is this perhaps to do with reals now being irreducible?

[Reid Barton]

hmm, it worked with a depth of 38...

[Reid Barton]

but it takes many seconds

[Reid Barton]

There have been a number of changes to topological spaces and metric spaces which could be responsible too.

[Reid Barton]

It needs exactly 37

[Reid Barton]

Bisecting... :fencing:

[Reid Barton]

Apparently it stopped working in "add emetric spaces", though I don't know why yet

[Reid Barton]

I still don't have a very clear picture here, but this is what I've learned:

• The above code was pretty close to the default limit (32) before emetric spaces; it needed a depth of 29.
• emetric spaces do add some extra instances. You can now go (when solving, i.e., backwards) either from uniform_space to emetric_space to metric_space or from uniform_space directly to metric_space.
• I don't understand what the parameter instance_max_depth actually controls. It isn't the nesting level as shown in parentheses, which never goes above 10 in the successful trace with emetric spaces. Maybe it has something to do with the number of unassigned metavariables?
• Perhaps more concerning than hitting the depth limit is how long it takes to find the instance with the limit increased. The successful log is about 600MB. The instance search seems to have no memory, so alternative paths to the same point, like from uniform_space to metric_space, even if not causing a diamond problem, are still dangerous for performance: the work done to find an instance can grow exponentially in the number of such branches.

[Reid Barton]

Is instance metric_space.to_uniform_space' still needed?

[Reid Barton]

For this example, using apply subtype.t2_space is a workaround