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.

Example : a discrete metric on the real line

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) (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) (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.