Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Excluded middle and decidable equality

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Excluded middle and decidable equality


Chronological Thread 
  • From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • To: "N. Raghavendra" <raghu AT hri.res.in>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Excluded middle and decidable equality
  • Date: Fri, 27 Sep 2013 15:09:31 +0200


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)



Archive powered by MHonArc 2.6.18.

Top of Page