diff --git a/lib/ModuRes/CSetoid.v b/lib/ModuRes/CSetoid.v index 0449cdf3116cacd3f6dd115ef12d2e20c63b6e01..223a7089e4ebbe130a164b06fce19e1755a076cb 100644 --- a/lib/ModuRes/CSetoid.v +++ b/lib/ModuRes/CSetoid.v @@ -402,3 +402,10 @@ Section OptDefs. Qed. End OptDefs. + +Section DiscreteType. + Context {T : Type}. + + Program Instance discreteType : Setoid T := mkType (@eq T). +End DiscreteType. + diff --git a/lib/ModuRes/MetricCore.v b/lib/ModuRes/MetricCore.v index 3d519e5ae6d27fe3daa195514a2e450e8cff6f80..0994fbc26520cad10bdb91cdc375c42bda3f72e2 100644 --- a/lib/ModuRes/MetricCore.v +++ b/lib/ModuRes/MetricCore.v @@ -870,22 +870,26 @@ Qed. (** Discrete spaces are proper metric spaces (discrete meaning that the distance is 1 if elements are diffent and 0 for equal elements. Equality here is propositional Coq equality. *) -Section Discrete. - Context {T : Type}. - - Program Instance discreteType : Setoid T := mkType (@eq T). +Section DiscreteMetric. + Context {T : Type} {T_type : Setoid T}. Definition discreteDist n (x y : T) := match n with O => True - | _ => x = y + | _ => x == y end. Global Arguments discreteDist n x y / . - + Program Instance discreteMetric : metric T := mkMetr discreteDist. Next Obligation. - split; intros HEq; [specialize (HEq 1) | intros [ | n] ]; - inversion HEq; subst; simpl; reflexivity. + intros x y Heq x' y' Heq'. split; (destruct n as [|n]; [reflexivity|simpl]). + - intros Heqx. rewrite <-Heq, <-Heq'. assumption. + - intros Heqy. rewrite Heq, Heq'. assumption. + Qed. + Next Obligation. + split; intros Heq. + - now apply (Heq 1). + - intros [|n]; tauto. Qed. Next Obligation. destruct n as [| n]; intros x y HS; simpl in *; [| symmetry]; tauto. @@ -903,11 +907,11 @@ Section Discrete. Next Obligation. intros n; exists 1; simpl; intros [| i] HLe; [inversion HLe |]. destruct n as [| n]; [exact I |]. - assert (HT := chain_cauchy σ _ 1 (S i) 1); inversion HT. - rewrite H0; reflexivity. + assert (HT := chain_cauchy σ _ 1 (S i) 1). rewrite HT. + reflexivity. Qed. -End Discrete. +End DiscreteMetric. Section Option. Context `{cT : cmetric T}.