Karl Palmskog (Aug 03 2020 at 13:51): Karl Palmskog (Aug 03 2020 at 13:51):so I have a project where I use some of the key files from analysis. However, by going to classical logic, all my "MathComp encoding instincts" seem to no longer apply - everything is decidable, everything becomes a boolean if you want it to. Should I use just use booleans connectives everywhere? Should I even bother with eqTypes anymore? Is there even a point to reflect anything? Do you guys have any heuristics to avoid foundational anxiety?
Cyril Cohen (Aug 03 2020 at 22:00):Karl Palmskog said:
so I have a project where I use some of the key files from analysis. However, by going to classical logic, all my "MathComp encoding instincts" seem to no longer apply - everything is decidable, everything becomes a boolean if you want it to. Should I use just use booleans connectives everywhere? Should I even bother with eqTypes anymore? Is there even a point to
reflectanything? Do you guys have any heuristics to avoid foundational anxiety?
Indeed, ssreflect instincts fall short, and we still have some hesitation. For now the dominant style is bool for math-comp core stuff compat and otherwise Prop connective (e.g. for classical sets). There might be a shift at some point but I cannot yet predict when and which one. So for now: Prop connective for analysis stuff, bool connective for coremathcomp stuff, and asbool as few times as possible for compatibility between the two.
Karl Palmskog (Aug 03 2020 at 22:02):that makes sense, thanks! (also glad I'm not alone in pondering how to play well with MC+boolp.v)
Last updated: Oct 13 2024 at 01:02 UTC