coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] symmetric equality, Ethan Aubin
- Re: [Coq-Club] symmetric equality,
Stefan O'Rear
- Re: [Coq-Club] symmetric equality, vsiles
- Re: [Coq-Club] symmetric equality,
Sean Wilson
- Re: [Coq-Club] symmetric equality, Stefan O'Rear
- Re: [Coq-Club] symmetric equality,
Stefan O'Rear
Archive powered by MhonArc 2.6.16.