Stream: Coq users

Topic: ✔ Computation Variant of In and String Comparison


view this post on Zulip Notification Bot (Jan 09 2024 at 10:10):

Julia Dijkstra has marked this topic as resolved.

view this post on Zulip Ana de Almeida Borges (Jan 09 2024 at 13:38):

MathComp uses a boolean list membership predicate by default (x \in X), but I wouldn't say it is worth it to learn MathComp just for that. (I do think it is worthwhile in general, it's a nice library and much "cleaner" / well-thought-out than the standard library.)

view this post on Zulip Karl Palmskog (Jan 09 2024 at 13:42):

more generally, ad-hoc use of bool is a bad idea, and will almost inevitably lead to unmaintainable code. The only realistic ways to handle decidability are in my view (1) via bool together with MathComp/SSReflect or (2) via the Decision typeclass as found in Std++ or Math-Classes. This classic blog post explains the core issue: https://existentialtype.wordpress.com/2011/03/15/boolean-blindness/

view this post on Zulip Meven Lennon-Bertrand (Jan 09 2024 at 15:13):

I do not entirely agree, I feel boolean blindness is much less dire in proof assistants than in programming languages: you can always show properties of boolean functions, which you can observe to more easily comprehend what a function returning a boolean is doing. Of course, as soon as you define a function you should start proving things about it, ideally exactly what predicate it decides, in which case relying on SSReflect's reflect(or Decision) gives a good, systematic way to organize things (and infrastructure). But I wouldn't say having a boolean function in the middle of a development is necessarily a bad idea.

view this post on Zulip Karl Palmskog (Jan 09 2024 at 15:49):

there are always exceptions, but I think the "bool(-valued) function in the middle of a development" hints at the maintenance issue: without the recommended approaches, there will be no a priori knowable connection between the returned boolean and its provenance, i.e., you'll have to read comments or search for the function name

view this post on Zulip Meven Lennon-Bertrand (Jan 09 2024 at 15:54):

I don't see how that's different from a boolean function in SSReflect, where you need the corresponding reflect lemma to know what's happening?

view this post on Zulip Karl Palmskog (Jan 09 2024 at 16:00):

if you're using MathComp, for all standard stuff you're going to use something like apply/myP to apply a reflect lemma

view this post on Zulip Karl Palmskog (Jan 09 2024 at 16:01):

I'm sure there could be even nicer automation for listing and selecting the right reflect, though, but it should be pretty clear which ones can be applied

view this post on Zulip Karl Palmskog (Jan 09 2024 at 16:09):

in contrast, an ad-hoc lemma about about the provenance of a boolean in a bool-valued function could have almost any shape

view this post on Zulip Paolo Giarrusso (Jan 09 2024 at 19:39):

having TC search find the right lemma is convenient, and it'd improve ssreflect if typeclasses work in that context (that is, if&when unifall lands). What's more, TC search can synthesize some decision procedures and infrastructure for you (even if that only saves boilerplate once you know ssreflect APIs)


Last updated: Jun 13 2024 at 19:02 UTC