Library Waterproof.Libs.Analysis.MetricSpaces

Require Import Coq.Reals.Reals.
Require Import Reals.ROrderedType.
Require Import micromega.Lra.

Require Import Tactics.
Require Import Automation.
Require Import Libs.Reals.
Require Import Notations.Common.
Require Import Notations.Reals.
Require Import Notations.Sets.
Require Import Chains.

Waterproof Enable Automation RealsAndIntegers.

Open Scope R_scope.
Open Scope subset_scope.

Section Definitions.
Context (X : Metric_Space).


Coercion Base : Metric_Space >-> Sortclass.

Definition dist_positive :
  ∀ x ∈ X, ∀ y ∈ X, dist X x y ≥ 0.
Proof.
  Take x, y ∈ X.
  By dist_pos we conclude that dist X x y ≥ 0.
Qed.

Definition dist_non_degenerate :
  ∀ x ∈ X, ∀ y ∈ X,
  (dist X x y = 0) ⇒ (x = y).
Proof.
  Take x, y ∈ X.
  By (proj1(_,_,(dist_refl X x y))) we conclude that dist X x y = 0 ⇨ x = y.
Defined.

Definition dist_symmetric :
  ∀ x ∈ X, ∀ y ∈ X,
  dist X x y = dist X y x.
Proof.
  Take x, y ∈ X.
  By dist_sym we conclude that dist X x y = dist X y x.
Qed.

Definition dist_triangle_inequality :
  ∀ x ∈ X, ∀ y ∈ X, ∀ z ∈ X,
  dist X x z ≤ dist X x y + dist X y z.
Proof.
  Take x, y, z ∈ X.
  By (dist_tri X) we conclude that dist X x z ≤ dist X x y + dist X y z.
Qed.

Definition dist_reflexive : ∀ x ∈ X, dist X x x = 0.
Proof.
  Take x ∈ X.
  By (proj2(_, _, (dist_refl X x x))) we conclude that dist X x x = 0.
Defined.

End Definitions.

Definition d_discrete_R :
  ℝ → ℝ → ℝ := fun (x y : ℝ) => if Reqb x y then 0 else 3.

Lemma d'_eq_0 : forall x y : ℝ,
  d_discrete_R x y = 0 -> (Reqb x y) = true.
Proof.
Take x, y : ℝ.
Assume that d_discrete_R x y = 0.
Either x = y or x ≠ y.
+ Case x = y.
  By Req_true we conclude that Reqb x y = true.

+ Case x ≠ y.
  It holds that (if Reqb(x, y) then 0 else 3) = 0 as (i).
  rewrite (Req_false x y H) in i.
  Contradiction.
Qed.

Lemma d'_eq_3 : forall x y : ℝ, d_discrete_R x y = 3 -> (Reqb x y) = false.
Proof.
Take x, y : ℝ.
Assume that d_discrete_R x y = 3.
It holds that (if Reqb x y then 0 else 3) = 3 as (i).
Either x = y or x ≠ y.
+ Case x = y.
  rewrite (Req_true x y H) in i.
  It holds that 0 ≠ 3.
  Contradiction.
+ Case x ≠ y.
  By Req_false we conclude that Reqb x y = false.
Qed.

#[export] Hint Resolve d'_eq_0 : wp_reals.
#[export] Hint Resolve d'_eq_3 : wp_reals.
#[export] Hint Extern 0 => unfold d_discrete_R; rewrite Req_true; lra : wp_reals.
#[export] Hint Extern 0 => unfold d_discrete_R; rewrite Req_false; lra : wp_reals.