coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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)
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)
- [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 09/26/2013
- Re: [Coq-Club] Excluded middle and decidable equality, Arnaud Spiwack, 09/26/2013
- Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, Arnaud Spiwack, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, Andrej Bauer, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, Andrej Bauer, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, Arnaud Spiwack, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, Arnaud Spiwack, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, Andrej Bauer, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, Arnaud Spiwack, 09/27/2013
- Re: [Coq-Club] Excluded middle and decidable equality, Arnaud Spiwack, 09/26/2013
Archive powered by MHonArc 2.6.18.