Browse files

A decidability property of functional relations over decidable codoma…


git-svn-id: svn+ssh:// 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
herbelin committed Nov 15, 2012
1 parent 86c8f95 commit 8a225b67b616c89380caafad5f1cc1f6434ac9e1
Showing with 9 additions and 0 deletions.
  1. +9 −0 theories/Logic/Decidable.v
@@ -175,7 +175,16 @@ Proof.
unfold decidable. tauto.
+(* 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).
+intros X Y A Hdec H x y.
+destruct (H x) as (y',(Hex,Huniq)).
+destruct (Hdec y y') as [->|Hnot]; firstorder.
(** With the following hint database, we can leverage [auto] to check
decidability of propositions. *)

0 comments on commit 8a225b6

Please sign in to comment.