The Coq mailing list

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

It's fairly blatant indeed. The proof of inconsistency is almost a one-liner (I omitted the equivalence relation requirement for pedagogical purposes, but it is clear that R is indeed an equivalence relation):


Axiom setoideq_eq : forall {A:Type} (R:A->A->Prop) (x y : A), R x y -> x = y.

Goal False.
Proof.
  set (R := fun x y : bool => True).
  generalize (setoideq_eq R true false I); intros h.
  discriminate h.
Qed.

On 7 January 2014 17:46, Daniil Frumin <difrumin AT gmail.com> wrote:

It used to state the following:

Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.

Application of the extensionality principle for setoids.

Ltac setoid_extensionality :=
  match goal with
    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
  end.

I am pretty much a newb, so I am not sure if that's blatantly inconsistent

thanks

On Tue, Jan 7, 2014 at 8:24 PM, Pierre-Marie Pédrot
<pierre-marie.pedrot AT inria.fr> wrote:
> On 07/01/2014 16:59, Daniil Frumin wrote:
>> It has disappeared in V8.3 and I didn't find the mention of it in the changelog
>> and the last commit that removes it is 3b5e12a2eb98b34cacc1850f63b702dfea26cd57
>>
>> In particular I am looking for setoid_extensionality.
>
> Wasn't that an inconsistent axiom? I think I remember it stated
> something plain wrong. Can you remind us its type?
>
> PMP
>

--
Sincerely yours,
-- Daniil