Stream: maths

Topic: t2_space

Reid Barton (Nov 10 2018 at 22:56):

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 (Nov 10 2018 at 22:59):

Is this perhaps to do with reals now being irreducible?

Reid Barton (Nov 10 2018 at 23:00):

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

Reid Barton (Nov 10 2018 at 23:01):

but it takes many seconds

Reid Barton (Nov 10 2018 at 23:01):

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

Reid Barton (Nov 10 2018 at 23:03):

It needs exactly 37

Reid Barton (Nov 10 2018 at 23:11):

Bisecting... :fencing:

Reid Barton (Nov 10 2018 at 23:30):

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

Reid Barton (Nov 11 2018 at 01:20):

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 (Nov 11 2018 at 01:30):

Is instance metric_space.to_uniform_space' still needed?

Reid Barton (Nov 11 2018 at 01:44):

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

Last updated: May 06 2021 at 18:20 UTC