The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

At 2013-09-27T09:43:06+02:00, Arnaud Spiwack wrote:

> Well, not really. You have to change the definition of deceq for the
> proof to pass. Replacing Coq's native equality (which is pretty
> meaningless in the context of setoids) with  the setoid equality.
> Which is essentially the same thing as proving decequiv -> lem.

So is there no way to prove in Coq that deceq (with Coq's usual
equality) -> lem?

In any case, I am finding it difficult to understand how to define
setoids in Coq.  Here is the relation I am looking at:

Inductive blass (P : Prop) : bool -> bool -> Prop :=
| b_0 : blass P true true
| b_1 : blass P false false
| b_2 : P -> blass P true false
| b_3 : P -> blass P false true.

Given P : Prop, how does one define the quotient bool / (blass P) using
setoids?

Thanks for your help.

Best regards,
Raghu.

-- 
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/