From 1a2cd3fd4a5bc3e92d67d089f63337045f2d6567 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 13 Feb 2015 16:40:01 +0100 Subject: [PATCH] make the discrete metric more general: for any setoid --- lib/ModuRes/CSetoid.v | 7 +++++++ lib/ModuRes/MetricCore.v | 26 +++++++++++++++----------- 2 files changed, 22 insertions(+), 11 deletions(-) diff --git a/lib/ModuRes/CSetoid.v b/lib/ModuRes/CSetoid.v index 0449cdf3..223a7089 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 3d519e5a..0994fbc2 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}. -- GitLab