The Coq mailing list

[Daniil Frumin <difrumin AT gmail.com>]

Thanks a lot, this is easy indeed. I just got confused by the supposed
use of it in Matthieu's code: http://mattam.org/repos/coq/cat/TYPE.v

I wonder if it is possible to fix that proof at all?

On Tue, Jan 7, 2014 at 9:04 PM, Arnaud Spiwack
<aspiwack AT lix.polytechnique.fr>
 wrote:
> 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
>>
>



-- 
Sincerely yours,
-- Daniil