Draft: Cantor

[zstone1]

Motivation for this change

The cantor set is generally useful construction, but not particularly general or easy to formalize. Instead we do most the theory using the "cantor space", that is, functions nat -> bool with the product topology. This is an early draft, but the approach already yields some promise

In terms of formalizability, this has the advantages that

• It's definable without putting a realType in scope
• The proofs generally induct over "prefixes" instead of dealing with nested intersections, or ternary representations.

In terms of theory, this is great because

• Hausdorff-Alexandroff theorem tells us that a metric space is compact iff there's a continuous surjection from the cantor space.
• uncountability, compactness, hausdorff, are all trivially true.

• Things need to go into files that make sense. The stuff about discrete topologies obviously belongs in topology. But the definition of the cantor_set belongs after sequences. Not clear where it the cantor_space itself goes.

Things done/to do

• [ ] added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries, only append new ones, be careful: merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
• [ ] added corresponding documentation in the headers
• [ ] prove this topology comes from a metric
• [ ] prove this set is complete in that metric
• [ ] prove the continuity of the cantor_map
• [ ] I don't know the measure-theoretic implications of this approach. I wonder if this makes things better or worse?

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

Not a deep comment but you may want to consider the if/is/then/else syntax to write functions, e.g.:

Fixpoint false_extend (s : seq bool) : cantor_space :=
  if s is b :: s then
    (fun n => if n is m.+1 then false_extend s m else b)
  else
    (fun=> false).

Fixpoint prefix_of (x : cantor_space) (n : nat) : seq bool :=
  if n is m.+1 then x 0 :: prefix_of (pull x) m else nil.

Local Fixpoint prefix_helper (i : nat) (s : seq bool) :=
  if s is b :: l then
    prod_topo_apply i @^-1` [set b] `&` prefix_helper (S i) l
  else
    [set: cantor_space].

[zstone1]

Bigger and better cantor stuff coming. With #763, the bulk of this work becomes redundant anyway.