CoRN.metric2.Hausdorff

Require Import ZBasics.
Require Import Classic.
Require Export Metric.
Require Import Classification.
Require Import List.
Require Import ZArith.
Require Import QMinMax.
Require Import QposMinMax.
Require Import Qauto.
Require Import CornTac.

Open Local Scope Q_scope.

Section HausdorffMetric.

Hausdorff Metric

This module defines a Hausdorff metric for an arbitrary predicate over a metric space X.

Variable X : MetricSpace.

This is the (weak) hemiMetric, which makes an asymmetric metric. We make use of the classical quantifer in this definition.

Definition hemiMetric (e:Qpos) (A B: X → Prop) :=
∀ x:X, A x →
existsC X (fun y ⇒ B y ∧ ball e x y).

This (weak) metric, makes the full symmetric metric.

Definition hausdorffBall (e:Qpos) (A B: X → Prop) :=
hemiMetric e A B ∧ hemiMetric e B A.

Lemma hemiMetric_wd1 : ∀ (e0 e1:Qpos) A B,
(QposEq e0 e1) → hemiMetric e0 A B → hemiMetric e1 A B.
Proof.
intros e0 e1 A B He H x Hx.
destruct (H x Hx) as [HG | y [Hy Hxy]] using existsC_ind.
  apply existsC_stable; assumption.
apply existsWeaken.
∃ y.
rewrite → He in Hxy; auto.
Qed.

Lemma hausdorffBall_wd1 : ∀ (e0 e1:Qpos) A B,
(QposEq e0 e1) → hausdorffBall e0 A B → hausdorffBall e1 A B.
Proof.
intros e0 e1 A B He [H0 H1].
split; apply hemiMetric_wd1 with e0; assumption.
Qed.

Lemma hemiMetric_refl : ∀ e A, hemiMetric e A A.
Proof.
intros e A x Hx.
apply existsWeaken.
∃ x.
split; try assumption.
apply ball_refl.
Qed.

Lemma hausdorffBall_refl : ∀ e A, hausdorffBall e A A.
Proof.
intros e A.
split; apply hemiMetric_refl.
Qed.

Lemma hausdorffBall_sym : ∀ e A B,
hausdorffBall e A B → hausdorffBall e B A.
Proof.
intros e A B [H0 H1].
split; assumption.
Qed.

Lemma hemiMetric_triangle : ∀ e0 e1 A B C,
hemiMetric e0 A B → hemiMetric e1 B C → hemiMetric (e0 + e1) A C.
Proof.
intros e0 e1 A B C H0 H1 x Hx.
destruct (H0 x Hx) as [HG | y [Hy Hxy]] using existsC_ind.
  apply existsC_stable; assumption.
destruct (H1 y Hy) as [HG | z [Hz Hyz]] using existsC_ind.
  apply existsC_stable; assumption.
apply existsWeaken.
∃ z.
split; try assumption.
apply ball_triangle with y; assumption.
Qed.

Lemma hausdorffBall_triangle : ∀ e0 e1 A B C,
hausdorffBall e0 A B → hausdorffBall e1 B C → hausdorffBall (e0 + e1) A C.
Proof.
intros e0 e1 A B C [H0A H0B] [H1A H1B].
split.
  apply hemiMetric_triangle with B; assumption.
apply hemiMetric_wd1 with (e1 + e0)%Qpos.
  QposRing.
apply hemiMetric_triangle with B; assumption.
Qed.

Unfortunately this isn't a metric for an aribitrary predicate. More assumptions are needed to show our definition of ball is closed. See FinEnum for an example of an instance of the Hausdorff metric.

Hypothesis stableX : stableMetric X.

Lemma hemiMetric_stable :∀ e A B, ~~(hemiMetric e A B ) → hemiMetric e A B.
Proof.
unfold hemiMetric.
auto 7 using existsC_stable.
Qed.

Lemma hausdorffBall_stable :∀ e A B, ~~(hausdorffBall e A B ) → hausdorffBall e A B.
Proof.
unfold hausdorffBall.
firstorder using hemiMetric_stable.
Qed.

Lemma hemiMetric_wd :∀ (e1 e2:Qpos), (e1 ==e2) →
∀ A1 A2, (∀ x, A1 x ↔ A2 x) →
∀ B1 B2, (∀ x, B1 x ↔ B2 x) →
(hemiMetric e1 A1 B1 ↔ hemiMetric e2 A2 B2).
Proof.
cut (∀ e1 e2 : Qpos, e1 == e2 → ∀ A1 A2 : X → Prop, (∀ x : X, A1 x ↔ A2 x) →
   ∀ B1 B2 : X → Prop, (∀ x : X, B1 x ↔ B2 x) →
     (hemiMetric e1 A1 B1 → hemiMetric e2 A2 B2)).
  intros; split.
   eauto.
  symmetry in H0.
  assert (H1':∀ x : X, A2 x ↔ A1 x) by firstorder.
  assert (H2':∀ x : X, B2 x ↔ B1 x) by firstorder.
  eauto.
intros e1 e2 He A1 A2 HA B1 B2 HB H x Hx.
rewrite <- HA in Hx.
destruct (H x Hx) as [HG | y [Hy0 Hy1]] using existsC_ind.
  auto using existsC_stable.
apply existsWeaken.
∃ y.
change (QposEq e1 e2) in He.
rewrite <- HB.
rewrite <- He.
auto.
Qed.

Lemma hausdorffBall_wd :∀ (e1 e2:Qpos), (e1 ==e2) →
∀ A1 A2, (∀ x, A1 x ↔ A2 x) →
∀ B1 B2, (∀ x, B1 x ↔ B2 x) →
(hausdorffBall e1 A1 B1 ↔ hausdorffBall e2 A2 B2).
Proof.
intros.
unfold hausdorffBall.
setoid_replace (hemiMetric e1 A1 B1) with (hemiMetric e2 A2 B2).
  setoid_replace (hemiMetric e1 B1 A1) with (hemiMetric e2 B2 A2).
   reflexivity.
  apply hemiMetric_wd; auto.
apply hemiMetric_wd; auto.
Qed.

End HausdorffMetric.

Section HausdorffMetricStrong.

Variable X : MetricSpace.

Strong Hausdorff Metric

This section introduces an alternative stronger notition of Haudorff metric that uses a constructive existential.

Definition hemiMetricStrong (e:Qpos) (A B: X → Prop) :=
∀ x:X, A x →
∀ d:Qpos, {y:X | B y ∧ ball (e +d) x y}.

Definition hausdorffBallStrong (e:Qpos) (A B: X → Prop) :=
(hemiMetricStrong e A B × hemiMetricStrong e B A)%type.

Lemma hemiMetricStrong_wd1 : ∀ (e0 e1:Qpos) A B,
(QposEq e0 e1) → hemiMetricStrong e0 A B → hemiMetricStrong e1 A B.
Proof.
intros e0 e1 A B He H x Hx d.
destruct (H x Hx d) as [y [Hy Hxy]].
∃ y.
rewrite → He in Hxy; auto.
Qed.

Lemma hausdorffBallStrong_wd1 : ∀ (e0 e1:Qpos) A B,
(QposEq e0 e1) → hausdorffBallStrong e0 A B → hausdorffBallStrong e1 A B.
Proof.
intros e0 e1 A B He [H0 H1].
split; apply hemiMetricStrong_wd1 with e0; assumption.
Qed.

Lemma hemiMetricStrong_refl : ∀ e A, hemiMetricStrong e A A.
Proof.
intros e A x Hx d.
∃ x.
split; try assumption.
apply ball_refl.
Qed.

Lemma hausdorffBallStrong_refl : ∀ e A, hausdorffBallStrong e A A.
Proof.
intros e A.
split; apply hemiMetricStrong_refl.
Qed.

Lemma hausdorffBallStrong_sym : ∀ e A B,
hausdorffBallStrong e A B → hausdorffBallStrong e B A.
Proof.
intros e A B [H0 H1].
split; assumption.
Qed.

Lemma hemiMetricStrong_triangle : ∀ e0 e1 A B C,
hemiMetricStrong e0 A B → hemiMetricStrong e1 B C → hemiMetricStrong (e0 + e1) A C.
Proof.
intros e0 e1 A B C H0 H1 x Hx d.
destruct (H0 x Hx ((1#2)*d)%Qpos) as [y [Hy Hxy]].
destruct (H1 y Hy ((1#2)*d)%Qpos) as [z [Hz Hyz]].
∃ z.
split; try assumption.
setoid_replace (e0 + e1 + d)%Qpos with ((e0 + (1 # 2) × d) +(e1 + (1 # 2) × d))%Qpos by QposRing.
apply ball_triangle with y; assumption.
Qed.

Lemma hausdorffBallStrong_triangle : ∀ e0 e1 A B C,
hausdorffBallStrong e0 A B → hausdorffBallStrong e1 B C → hausdorffBallStrong (e0 + e1) A C.
Proof.
intros e0 e1 A B C [H0A H0B] [H1A H1B].
split.
apply hemiMetricStrong_triangle with B; assumption.
apply hemiMetricStrong_wd1 with (e1 + e0)%Qpos.
QposRing.
apply hemiMetricStrong_triangle with B; assumption.
Qed.

Hypothesis almostDecideX : locatedMetric X.

End HausdorffMetricStrong.