coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Difference between sum and sumbool

From: "John Wiegley" <johnw AT newartisans.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Difference between sum and sumbool
Date: Tue, 25 Aug 2015 00:12:15 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pa0-f41.google.com
Ironport-phdr: 9a23:j/PKTBPjvc2y1GJyu6Yl6mtUPXoX/o7sNwtQ0KIMzox0KP/yrarrMEGX3/hxlliBBdydsKIfzbeI+PCxEUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35/xir75q8ybSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSJDUgKWE8osPx5jfZSg7arFkbUmNerRtFDAzI/VuyCpX2si3lnuxwxyCAIcztRLYvHz+l6vE4G1fTlC4bOmthoynsgctqgfcDrQ==
Organization: New Artisans LLC

>>>>> Dirk Pattinson
>>>>> <dirk.pattinson AT anu.edu.au>
>>>>> writes:

> Hi:
> I'm trying to understand the difference between Coq's sum and sumbool when
> applied to propositions. In particular, what are the benefits of using
> sumbool
> over the use of (plain and simple disjoint) sum?

> - both carry computational information

sumbool does not carry information usable outside of Prop.

> Extraction Language Haskell.
> Extract Inductive sumbool =>
> "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].

Right, sumbool is isomorphic to Bool, and sum to Either. The Prop witnesses
from the sumbool are erased in the extraction.

John

[Coq-Club] Difference between sum and sumbool, Dirk Pattinson, 08/25/2015
- Re: [Coq-Club] Difference between sum and sumbool, John Wiegley, 08/25/2015
  - Re: [Coq-Club] Difference between sum and sumbool, Dirk Pattinson, 08/25/2015
    - Re: [Coq-Club] Difference between sum and sumbool, Guillaume Melquiond, 08/25/2015
    - Re: [Coq-Club] Difference between sum and sumbool, John Wiegley, 08/25/2015