Section Finite.

Variable X:MetricSpace.

Finite Enumerations

Here we define a classical in predicate for lists. Being classically in a list doesn't tell you which element in the list you are.
Fixpoint InFinEnumC (x:X) (l:list X) : Prop :=
match l with
| nil => ⊥
| y::ys => orC (st_eq x y) (InFinEnumC x ys)
end.

Lemma InFinEnumC_weaken : forall x l, (In x l) -> InFinEnumC x l.

Lemma InFinEnumC_wd1 : forall x y l, (st_eq x y) -> (InFinEnumC x l <-> InFinEnumC y l).

Lemma InFinEnumC_stable : forall x l, ~~(InFinEnumC x l) -> InFinEnumC x l.

Lemma InFinEnumC_app_l : forall x l1 l2, InFinEnumC x l1 -> InFinEnumC x (l1 ++ l2).

Lemma InFinEnumC_app_r : forall x l1 l2, InFinEnumC x l2 -> InFinEnumC x (l1 ++ l2).
Lemma InFinEnumC_app_orC : forall x l1 l2, InFinEnumC x (l1 ++ l2) -> orC (InFinEnumC x l1) (InFinEnumC x l2).

Equivalence

Two finite enumerations, represented as lists, are equivalent if they (classically) have the same elements.
Definition FinEnum_eq (a b:list X) : Prop :=
 forall x, InFinEnumC x a <-> InFinEnumC x b.

Lemma FinEnum_eq_refl : forall a, FinEnum_eq a a.

Lemma FinEnum_eq_sym : forall a b, FinEnum_eq a b -> FinEnum_eq b a.

Lemma FinEnum_eq_trans : forall a b c, FinEnum_eq a b -> FinEnum_eq b c -> FinEnum_eq a c.

Lemma FinEnum_is_Setoid : Setoid_Theory _ FinEnum_eq.

Definition FinEnumS : Setoid := Build_Setoid FinEnum_is_Setoid.

Metric Space

Finite enumerations form a metric space under the Hausdorff metric for any stable metric space X.
Definition FinEnum_ball (e:Qpos) (x y:list X) :=
 hausdorffBall X e (fun a => InFinEnumC a x) (fun a => InFinEnumC a y).

Lemma FinEnum_ball_wd : forall (e1 e2:Qpos), (e1==e2) ->
 forall (a1 a2 : FinEnumS), st_eq a1 a2 ->
 forall (b1 b2 : FinEnumS), st_eq b1 b2 ->
 (FinEnum_ball e1 a1 b1 <-> FinEnum_ball e2 a2 b2).

Hypothesis Xstable : stableMetric X.

Lemma hemiMetric_closed : forall e A b,
 (forall d, hemiMetric X (e+d) A (fun a => InFinEnumC a b)) ->
  hemiMetric X e A (fun a => InFinEnumC a b).

Lemma FinEnum_ball_closed : forall e a b,
 (forall d, FinEnum_ball (e+d) a b) ->
 FinEnum_ball e a b.

Lemma FinEnum_ball_eq :
 forall a b : list X, (forall e : Q+, FinEnum_ball e a b) -> FinEnum_eq a b.

Lemma FinEnum_is_MetricSpace : is_MetricSpace FinEnumS FinEnum_ball.

Definition FinEnum : MetricSpace :=
Build_MetricSpace FinEnum_ball_wd FinEnum_is_MetricSpace.

Our definition preserves stability
Lemma FinEnum_stable : stableMetric FinEnum.

Lemma FinEum_map_ball : forall (f:X -> X) e (s:FinEnum),
 (forall x, ball e x (f x)) -> ball e s (map f s).

Section Strong.

Strong Hausdroff Metric

This section shows that the strong version of the Hausdroff metric is equivalen to the weak version when X is a located metric.
Hypothesis almostDecideX : locatedMetric X.

Lemma HemiMetricHemiMetricStrong : forall (e:Qpos) A b,
 hemiMetric X e A (fun a => InFinEnumC a b) -> hemiMetricStrong X e A (fun a => InFinEnumC a b).

Lemma HausdorffBallHausdorffBallStrong : forall (e:Qpos) (a b:FinEnum),
 ball e a b ->
 hausdorffBallStrong X e (fun x => InFinEnumC x a) (fun x => InFinEnumC x b).

Lemma HemiMetricStrongAlmostDecidableBody :
 forall (e d:Qpos) a (b : FinEnum),
 e < d ->
 {hemiMetric X d (fun x => st_eq x a) (fun x => InFinEnumC x b)} +
 {~hemiMetric X e (fun x => st_eq x a) (fun x => InFinEnumC x b)}.

Lemma HemiMetricStrongAlmostDecidable :
 forall (e d:Qpos) (a b : FinEnum),
 e < d ->
 {hemiMetric X d (fun x => InFinEnumC x a) (fun x => InFinEnumC x b)} +
 {~hemiMetric X e (fun x => InFinEnumC x a) (fun x => InFinEnumC x b)}.

Finite Enumerations preserve the locatedness property.
Lemma FinEnum_located : locatedMetric FinEnum.

Finite Enumerations preserve the prelength property assuming X is a located metric space.

If we change the definition of prelenght space to use a classical existential, then we could drop the located assumption of X. I believe there would be no harm in changing the definition this way, but it has not been done yet.
Hypothesis preLengthX : PrelengthSpace X.

Lemma FinEnum_prelength : PrelengthSpace FinEnum.

End Strong.

End Finite.
A list is equivalent to it's reverse as finite enumerations
Lemma FinEnum_eq_rev : forall X (stable: stableMetric X) (f:FinEnum stable),
 st_eq f (rev f).


map is compatable with classical in
Lemma InFinEnumC_map : forall (X Y:MetricSpace) (f:X --> Y) a l, InFinEnumC a l -> InFinEnumC (f a) (map f l).

The map function for finite enumerations is uniformly continuous
Definition FinEnum_map_modulus (z:Qpos) (muf : Q+ -> Q+∞) (e:Qpos) :=
match (muf e) with
| ∞ => z
| Qpos2QposInf d => d
end.

Lemma FinEnum_map_uc : forall z X Y (SX:stableMetric X) (SY:stableMetric Y) (f:X --> Y), is_UniformlyContinuousFunction (map f:FinEnum SX -> FinEnum SY) (FinEnum_map_modulus z (mu f)).
Definition FinEnum_map z X Y (SX:stableMetric X) (SY:stableMetric Y) (f:X --> Y) :=
 Build_UniformlyContinuousFunction (FinEnum_map_uc z SX SY f).

maping Cunit is an injection from FinEnum X to FinEnum Complete X that preserves the metric
Lemma FinEnum_map_Cunit : forall X (SX:stableMetric X) SCX (s1 s2:FinEnum SX) e, ball e s1 s2 <-> ball e (map Cunit s1:FinEnum SCX) (map Cunit s2).