Homeomorphism example

[Columbus240]

Sample proof, that unit sphere is homeomorphic to a unit interval with glued ends.

TODO:

• Make CI happy with 8.12
• Decide whether to keep supporting 8.10 & 8.11
• Possibly move examples to a separate subdirectory.
• Generalize to n-spheres using suspension.
• Rebase it onto master and squash/split commits

Copied from #36.

[Columbus240]

Maybe we should consider creating a separate directory for examples – since it would inevitably require supplementary lemmas unrelated to topology, that have a little value outside it. Among real number lemmas above, perhaps, only sin x < x is useful, so I submitted it to the standard library - see coq/coq#15599.

Sounds reasonable to me.

[stop-cran]

The reference asin was not found in the current environment.

Looks like asin was not defined in versions 8.11 and 8.10.

[Columbus240]

We could drop support to 8.10 & 8.11 if we want.

I looked more closely over your work. We could avoid defining the function from S¹ to [0,1] explicitly, by using the theorem that any continuous function from a compact to a Hausdorff space is an embedding (a homeomorphism onto its image). Because the function f_inv : [0,1]/{0,1} → S¹ is such a function, we can spare ourselves the technical details of the inverse map.
Also, we can simplify the definition of f_inv as

Definition circle_cover (t : RTop) : ProductTopology2 RTop RTop :=
  (cos (2*PI*t), sin (2*PI*t)).

Axiom circle_cover_image : forall t, In S1_Ensemble (circle_cover t).

Axiom f_inv_helper : forall (x y : UnitInterval) :
  SpaceAdjunction (Couple U0 U1) x y ->
  (fun x => exist _ (circle_cover (subspace_inc _ x)) (circle_cover_image _)) x =
  (fun x => exist _ (circle_cover (subspace_inc _ x)) (circle_cover_image _)) y.

Definition f_inv : ClosedUnitInterval -> S1 :=
  induced_function
    (fun x => exist _ (circle_cover (subspace_inc _ x)) _)
    (SpaceAdjunction_equivalence _) f_inv_helper.

Using some (new) lemmas about the properties of induced_function, we can reduce the length of the proofs and remove technical details, by staying "more conceptual".

[Columbus240]

I am so free and push some changes, implementing the above sketch.
Above I claimed

We could avoid defining the function from S¹ to [0,1] explicitly, by using the theorem …

But this is wrong. For surjectivity we still need to do define this function. At least we can avoid concerning ourselves with continuity of that function, or we could define the function only inside the proof.

The largest proofs are currently circle_cover_inj, circle_cover_preimage (less so) and f_inv_bijective. A lot of time they spend shuffling real numbers around.
Erm, there are some redundancies in a proof (I pose both PI > 0 and PI <> 0) and the commit a18aac7 should not be in this branch.

[Columbus240]

The theorems cos_inj and sin_inj of the stdlib were only added in coq/coq@aa99264, which is part of v8.12. If we wanted this branch to be compatible with v8.10 and v8.11 we would need to add the theorems to our library ourselves or get them from another dependency.
I don't think either of these things is worth it and propose removing support for v8.10 and v8.11. Because I don't know of any project that makes use of this library, I think it's ok to do so. Dropping support for v8.10 would also allow us to fix the deprecated-ident-entry warnings of v8.13 and upwards (see #17).

[stop-cran]

@Columbus240 I agree to remove support for v8.10 and v8.11, because apart from the last issue, we have missing definition of asin and related lemmas.

[Columbus240]

Ok, then I will make a new release and then drop support in master.
You may have seen already: I pushed my previous notes on the product of Ensembles to master.

[Columbus240]

I extracted those lemmas out of Examples/S1.v which I found worthy. If we did more work involving the reals or trigonometry, we might need the other ones too, but that can be done as necessary. The rest of the commits I squashed down.
I moved the file into a separate folder, as we discussed.
I'll merge this, as it is now.