Stream: Coq users

Topic: "classical tauto"?


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 08 2021 at 18:17):

Same question, but I’d like docs on how to switch on. Without Reals.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jan 08 2021 at 18:46):

From the code, it's enough to have the core.nnpp.type reference registered.

view this post on Zulip Pierre-Marie Pédrot (Jan 08 2021 at 18:46):

To turn it on, you thus only have to require Coq.Logic.Classical_Prop

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jan 08 2021 at 18:49):

Seems to be enough indeed.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jan 08 2021 at 18:50):

It's quite hackish, definitely.

view this post on Zulip Pierre-Marie Pédrot (Jan 08 2021 at 18:50):

En passant, it's yet another Require-bound behaviour...

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jan 08 2021 at 18:59):

The real axiomatization is weaker than full excluded middle, though.

view this post on Zulip Pierre-Marie Pédrot (Jan 08 2021 at 19:00):

It's a hodgepodge of quite classical axioms, but not completely so IIRC

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Jan 28 2023 at 05:02 UTC