Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Difference between sum and sumbool

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Difference between sum and sumbool


Chronological Thread 
  • From: Dirk Pattinson <dirk.pattinson AT anu.edu.au>
  • To: <coq-club AT inria.fr>
  • Subject: [Coq-Club] Difference between sum and sumbool
  • Date: Tue, 25 Aug 2015 13:04:11 +1000
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dirk.pattinson AT anu.edu.au; spf=Pass smtp.mailfrom=dirk.pattinson AT anu.edu.au; spf=None smtp.helo=postmaster AT APC01-SG2-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:KO2q0BwgeB5laDrXCy+O+j09IxM/srCxBDY+r6Qd0e8fIJqq85mqBkHD//Il1AaPBtWAra8awLSJ+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStWU0pr8ib/60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGxmkql+rIsYDe26Ivx5HvRkC2FyOGcsocbvqBPrTA2V53JaXH9AwTRSBA2QwBDgXd/Juzfmt+xm3y/SacH3V7NyQT2+86ZtUxjuoC4BKng0/HyRg9Em3/ETmw6ouxEqm92cW4qSLvcrI/vQ
  • Spamdiagnosticmetadata: NSPM
  • Spamdiagnosticoutput: 1:23

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
- the same tactics apply to both (inversion, destruct, left, right)
- sum P Q and sumbool P Q are isomorphic when applied to P Q: Prop.

The only difference I could make out is their behaviour when extracting: sumbool can be extracted to Bool, e.g.

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

works (for me) but doing the same with sumbool doesn't. I hypothesise that this is because extraction "knows" that the arguments of sumbool will be discarded.

Is this the only difference, or am I missing something?

Dirk.




Archive powered by MHonArc 2.6.18.

Top of Page