Add LoadPath "./interval".

Require Import Fourier Reals.
Require Import  ssreflect ssrbool ssrnat eqtype ssrfun fintype finfun matrix bigops.
Require Import Rstruct.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Open Scope R_scope.


Section topologyBase.

Variable T: Type.
(*  set union and intersection *)
Definition setU (s1 s2: T -> Prop) := fun x => s1 x \/ s2 x.
Definition setI (s1 s2: T -> Prop) := fun x => s1 x /\ s2 x.



End topologyBase.


(*METRIC SPACES*)
(*patch the SL Metric_Space structure *)

Definition Base_to_Type (X: Metric_Space): Type := Base X.

Coercion Base_to_Type: Metric_Space >-> Sortclass.

Implicit Arguments dist[m].
Implicit Arguments dist_pos[m].
Implicit Arguments dist_sym[m].
Implicit Arguments dist_refl[m].
Implicit Arguments dist_tri[m].

Canonical Structure metricSpace_R := R_met.


Section metricSpaceProp.

Variable Ms: Metric_Space.

Lemma dist_large_pos:
  forall (x y : Ms),  0 <= dist x y.
Proof.
move=> x y.
apply Rmult_le_reg_l with 2; first by fourier.
ring_simplify.
apply Rle_trans with (dist x x).
  by right; apply  sym_equal; rewrite dist_refl.
apply Rle_trans with (dist x y + dist y x); first by apply dist_tri.
rewrite dist_sym; right; ring.
Qed.

Lemma dist_strict_pos:
  forall (x y : Ms), x <> y -> 0 < dist x y.
Proof.
move=> x y Hxy.
elim (dist_large_pos x y); first by done.
move=> H; apply sym_equal in H.
by move:H; rewrite dist_refl =>H; elim Hxy.
Qed.

End metricSpaceProp.


Section topologyMetric.

Variable Ms: Metric_Space.

Definition openDisc (x:Ms) r := fun y => dist x y < r.
(*maybe define the open discs as structures - same as for inervals *)

Lemma separate_metric:
  forall (x1 x2: Ms), x1 <> x2 -> exists r1 , exists r2, 
  forall x, ~ setI (openDisc x1 r1) (openDisc x2 r2) x.
Proof.
move=> x1 x2.
pose r := (dist x1 x2 / 4). 
exists r; exists r => x [Hx1 Hx2].
have Hr : 0 < r.
  rewrite /r; apply Rmult_lt_reg_l with 4; first by fourier.
  field_simplify; rewrite /Rdiv Rinv_1; ring_simplify.
  by apply: dist_strict_pos.
have H2: 4*r < 2*r.
  replace (4*r) with (dist x1 x2); last by (rewrite /r; field) .
  apply Rle_lt_trans with (dist x1 x + dist x x2); first by apply dist_tri.
  replace (2*r) with (r+r); last by ring.
  by rewrite (dist_sym x _); apply: Rplus_lt_compat.
have H3: ~ 4 * r < 2 * r by  fourier.
by elim H3.
Qed.

(*Lemma separate_metric:
  forall (x1 x2: Ms), x1 <> x2 -> exists r1 , exists r2, 
  0 < r1 /\ 0 < r2 /\ (forall x, ~ intersect (openDisc x1 r1) (openDisc x2 r2) x).
Proof.
*)

End topologyMetric.
 
Implicit Arguments openDisc[Ms].