The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

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

Not without axioms.
 

In any case, I am finding it difficult to understand how to define
setoids in Coq.

Require Import Coq.Classes.RelationClasses.

Record Setoid := {
  El :> Type;
  equ : El->El->Prop;
  equ_equiv : Equivalence equ
}.
 

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?

Require Import Coq.Program.Program.

(* I am being a little disingenuous here, as it won't be a true quotient if R doesn't respect the equality of A. *)

Program Definition Quotient (A:Setoid) (R:A->A->Prop) {e:Equivalence R} : Setoid := {|
  El := A ;
  equ := R
|}.
Next Obligation.
  typeclasses eauto.
Qed.

Defintion Bool : Setoid := {|
  El := bool ;
  equ := eq
|}.
Next Obligation.
  typeclasses eauto.
Qed.

Instance blass_equiv (P:Prop) : Equivalence (blass P).
Proof.
  (* fill in the blanks *)
Qed.

Definition B (P:Prop) := Quotient A (blass P).


I've just typed this, it is possible that it doesn't compile as is (the incomplete proof notwithstanding)