Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] symmetric equality

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] symmetric equality


chronological Thread 
  • From: vsiles AT lix.polytechnique.fr
  • To: "Ethan Aubin" <ethan.aubin AT gmail.com>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] symmetric equality
  • Date: Sat, 29 Sep 2007 08:35:56 +0200 (CEST)
  • Importance: Normal
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

> On Sat, Sep 29, 2007 at 12:26:06AM -0400, Ethan Aubin wrote:
>> Hi,  This might be an obvious question, but is 'forall (A:Set)(x y:A),
>> (x=y)=(y=x)' provable in Coq? - EA
>
> Equality is a very slippery subject in Coq and other systems based on
> intuitionistic type theories.  Your statement is certainly true if you
> replace the outer = with <-> (split; auto).  In general, it's a bad idea
> to use = on anything other than values of inductive types.
>
> Stefan
>
You also need (maybe it's too strong) the equality on A to be decidable
(forall x y:A, {x=y}+{x<>y}), otherwise you're not always allowed to test
x against any y of A.

Vincent





Archive powered by MhonArc 2.6.16.

Top of Page