Ssreflect Users Discussion List

[Georges Gonthier <>]

  Actually, ssrbool already defines a Coercion is_left : sumbool >-> bool, so 
all you need is
Lemma sumboolP P (dP : {P} +{~ P}) : reflect P dP.
Proof. by case: dP; constructor. Qed.

  That lemma should be in the library; for historical reasons there's only a 
special case in eqType (specifically, eqType.compareP), which was used to 
crank out eqType structures using decide equality in the 4-color theorem 
proof.

Georges

-----Original Message-----
From: Guillaume Melquiond [] 
Sent: 06 May 2011 15:48
To: Vincent Siles
Cc: 
Subject: Re: Specifying an equality to be decidable

Le vendredi 06 mai 2011 à 16:31 +0200, Vincent Siles a écrit :
> Hi everyone,
> I'm currently working on a formalization with an abstract relation R :
> A -> A -> Prop.
> Most of the work doesn't need to know anything else about R, but there 
> is a special set of results when R is a decidable equality.
> 
> I currently the following:
> 
> Section Eqdec.
> Variable eqA : A -> A -> Prop.
> Variable eqA_dec : forall x y, {eqA x y}+{~eqA x y}.
> Context `{Equivalence A eqA}.

I would directly use a relation eqA returning bool. But if you want to stick 
with returning Prop, I guess you can just add the following lines to your 
script:

Definition eqb x y :=
  match eqA_dec x y with left _ => true | right _ => false end.
Lemma eqAP : forall x y, reflect (eqA x y) (eqb x y).
rewrite /eqb => x y.
by case :eqA_dec ; constructor.
Qed.

Best regards,

Guillaume