coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Singleton with sets as characteristic functions in classical logic

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Singleton with sets as characteristic functions in classical logic
Date: Mon, 26 Aug 2019 16:34:43 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dschepler AT gmail.com; spf=Pass smtp.mailfrom=dschepler AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f46.google.com
Ironport-phdr: 9a23:EdysyR9UeG4NhP9uRHKM819IXTAuvvDOBiVQ1KB41escTK2v8tzYMVDF4r011RmVBN+dsq8ZwLCK+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhWiDanfL9/LBW7oQrPusQZnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRQT2gykbKTE27GDXitRxjK1FphKhuwd/yJPQbI2MKfZyYr/RcdYcSGFcXMheSjZBD5uzYIsBDeUPPehWoYrgqVUQsRSzHhWsCP/1xzNUmnP6wa833uI8Gg/GxgwgGNcOvWzaotrvMqcSUP66zK3Vxjvec/xW2Sny6JDMch8/u/GHQLV9ftfKyUYzFwPKkE2QqYj7MDOPzekNvG2b4PBhVeKrkWIotwZxoj22y8oql4LHhZoVx0ja+SllxIs5P961RU5hbdK5EZZdtjuWOoR3T84kXmpmojw1yqcctp6+ZCUKyIooxxrYa/GfdoiH+BPjVOKILTd5g3JpZauzhxi9/EWh0OH8Wc600FFFripBjNbArGwC1xvW6sSfS/t9+Fmu2SqX2gzN9u1JJVo4mKnbJpI737I9l5sevV7MEyL3gEn2ibWZdkQg+uim8eTnZbDmq4eBOI9vlg7+MrohmtS7AesmKAgDRGeb+eGm273i+U31WqlFjvozkqXBqpDVOdwbprKlAw9Syoss9xG/Dy6/3NsEmXkHMUlKdQmcj4npPlHOOOr3Ae2+g1SqijdrxurJMqfvApXXfTD/l+LKeq81wEpBwkJnxtdGoplQF7spIfTpW0a3usaOXTEjNAnh7+/hCdh5nrgVWW+XBqKDePfeqlSI6/orLvOka4ocuTK7IP8gsa29xUQlkEMQKPH6laAcb2q1S7E/ex3AMCjcx+wZGGJPhTIQCenjiVmMSzlWPi/gUKc15zV9A4WjX96aG9KdxYeZ1SL+JaV4I2BLDlfWTCXtfoSAHvYLMWecfpEnnTsDWrysDYQm0EP27VOo+/9cNuPRvxYgm9f7ztEsvr/ckBgz8Xp/CMHPi2w=

On Mon, Aug 26, 2019 at 3:54 PM richard dapoigny
<richard.dapoigny AT univ-smb.fr>
wrote:
>
> Dear Coq users,
>
> Assuming classical logic with the following definitions:
>
> Variable object : Set. (* elements *)
>
> Definition eqobject := @Logic.eq object.
>
> Lemma eqobject_dec : forall x y:object, eqobject x y \/ ~(eqobject x y).
> Proof.
> intros x y;unfold eqobject;apply classic.
> Qed.
>
> Is there a way to transform the following definition with Prop in classical
> logic (i.e., to remove booleans since left and right refer to sumbool):
>
> Definition Singleton (a:object) :=
> Caract
> (fun a':object =>
> match eqobject_dec a a' with
> | left h => True
> | right h => False
> end).
>
> Thanks for your help.

If you also assume the constructive_definite_description axiom from
the Description module, then you can construct classic_dec : forall P
: Prop, {P} + {~P}. This axiom is in line with traditional
mathematics (but not with constructivist mathematics): it's a
formalization of the type of definition that goes "define foo to be
the unique x such that some condition holds on x".
--
Daniel Schepler

[Coq-Club] Singleton with sets as characteristic functions in classical logic, richard dapoigny, 08/27/2019
- Re: [Coq-Club] Singleton with sets as characteristic functions in classical logic, Daniel Schepler, 08/27/2019
  - Re: [Coq-Club] Singleton with sets as characteristic functions in classical logic, richard dapoigny, 08/27/2019
    - Re: [Coq-Club] Singleton with sets as characteristic functions in classical logic, Christian Doczkal, 08/27/2019
      - Message not available
        
        Message not available
        
        Re: [Coq-Club] Singleton with sets as characteristic functions in classical logic, richard dapoigny, 08/29/2019