Brandon Moore (Jan 08 2021 at 15:46): Brandon Moore (Jan 08 2021 at 15:46):It seems that importing Reals makes tautostart using excluded middle, and the message for tauto failing changes to mention "classical tauto". I haven't found any documentation on this "classical tauto". I'd especially like to be able to switch it off.
Paolo Giarrusso (Jan 08 2021 at 18:17):Same question, but I’d like docs on how to switch on. Without Reals.
Paolo Giarrusso (Jan 08 2021 at 18:18):It probably comes from importing the Classic* axioms, but I didn’t know tauto supported using it.
Pierre-Marie Pédrot (Jan 08 2021 at 18:46):From the code, it's enough to have the core.nnpp.type reference registered.
Pierre-Marie Pédrot (Jan 08 2021 at 18:46):To turn it on, you thus only have to require Coq.Logic.Classical_Prop
Pierre-Marie Pédrot (Jan 08 2021 at 18:47):I don't know how to turn it off though, maybe registering a dummy definition over the old one is enough?
Pierre-Marie Pédrot (Jan 08 2021 at 18:49):Seems to be enough indeed.
Pierre-Marie Pédrot (Jan 08 2021 at 18:49):So, something along the lines of Register tt as core.nnpp.type. should turn off the classical tauto.
Pierre-Marie Pédrot (Jan 08 2021 at 18:50):It's quite hackish, definitely.
Pierre-Marie Pédrot (Jan 08 2021 at 18:50):En passant, it's yet another Require-bound behaviour...
Jasper Hugunin (Jan 08 2021 at 18:58):I'm curious as to why you want to switch it off. My understanding is that the excluded middle follows from the axiomatization of real numbers found in the Reals module, so once you are working with this version of the reals your setting is unavoidably classical. Are you defining terms with tauto? Or is classical tauto slower?
Pierre-Marie Pédrot (Jan 08 2021 at 18:59):The real axiomatization is weaker than full excluded middle, though.
Pierre-Marie Pédrot (Jan 08 2021 at 19:00):It's a hodgepodge of quite classical axioms, but not completely so IIRC
Pierre-Marie Pédrot (Jan 08 2021 at 19:06):It was rewritten recently amongst others to clean up that matter, and from a cursory look now it only depends on LPO in Type, WEM in Type and (dependent) funext
Brandon Moore (Jan 08 2021 at 19:37):I'm proving things that have nothing to do with Reals, I'd rather not accidentally depend on axioms.
Théo Zimmermann (Jan 08 2021 at 20:11):It was rewritten recently amongst others to clean up that matter, and from a cursory look now it only depends on LPO in Type, WEM in Type and (dependent) funext
Why does it still transitively require Classical_Prop then?
Théo Zimmermann (Jan 08 2021 at 20:15):Previous issue about this change of behavior of tauto: https://github.com/coq/coq/issues/5444
Pierre-Marie Pédrot (Jan 08 2021 at 22:50):If I'd to guess I'd say "backwards compat" although the require seems deliberate in RieamannInt and Rtopology
Guillaume Melquiond (Jan 09 2021 at 07:58):To be clear, the change of axioms in the lower layers of real numbers were no meant to clean them at all. The goal was to make it constructive rather than axiomatic. As a consequence, the newer axioms are actually stronger than before. In particular, functional extensionality was not needed before, and it is now. (LPO and WEM could be deduced from the old axioms. Functional extensionality could not.) So, that is kind of a regression (but that was the price to pay for constructive real numbers).
But that is the only for the lower layers. The upper layers of real analysis have not been rewritten at all. They were using the excluded middle before, and they are still using it now. For Riemann integration, this axiom is not needed (as we have proved in Coquelicot), though that is no small work to rewrite the current formalization. But for compactness, there is no real way around it. If you want a definition that looks like the traditional one ("you can extract a finite cover from any cover"), then you need excluded middle.
Last updated: Apr 19 2024 at 17:02 UTC