coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [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
- Re: [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
Archive powered by MHonArc 2.6.18.