From 8a225b67b616c89380caafad5f1cc1f6434ac9e1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 15 Nov 2012 05:56:22 +0000
Subject: A decidability property of functional relations over decidable
 codomains.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15972 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/Decidable.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index aaf1813bd6..0e74b63848 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -175,7 +175,16 @@ Proof.
 unfold decidable. tauto.
 Qed.
 
+(* Functional relations on decidable co-domains are decidable *)
 
+Theorem dec_functional_relation :
+  forall (X Y : Type) (A:X->Y->Prop), (forall y y' : Y, decidable (y=y')) ->
+  (forall x, exists! y, A x y) -> forall x y, decidable (A x y).
+Proof.
+intros X Y A Hdec H x y.
+destruct (H x) as (y',(Hex,Huniq)).
+destruct (Hdec y y') as [->|Hnot]; firstorder.
+Qed.
 
 (** With the following hint database, we can leverage [auto] to check
     decidability of propositions. *)
-- 
cgit v1.2.3