[Require Nsatz] should not change the behavior of [tauto]

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#5444
From: @JasonGross
Reported version: 8.6
CC: @herbelin

[coqbot]

Comment author: @JasonGross

Yet it does, because Classical_Prop is required by Rtopology is required by MVT
is required by PSeries_reg is required by Rtrigo is required by Reals is
required by Nsatz, and Classical_Prop adds

Hint Unfold not: core.

When we're willing to break backwards compatibility in the stdlib, this should
be fixed.

[coqbot]

Comment author: @JasonGross

Test case:

Goal forall (T : Type)
(eq : T -> T -> Prop)
(zero x y : T),
(not (eq x zero) -> eq y zero) <-> eq x zero / eq y zero.
Proof.
Fail intros; tauto.
Abort.
Require Coq.nsatz.Nsatz.

Goal forall (T : Type)
(eq : T -> T -> Prop)
(zero x y : T),
(not (eq x zero) -> eq y zero) <-> eq x zero / eq y zero.
Proof.
intros; tauto.
Qed.

[coqbot]

Comment author: @JasonGross

Ugh, it's worse than just [Hint Unfold not : core]; apparently the [tauto]
plugin checks to see whether or not Classical_Prop has been required, and
behaves differently on depending on whether or not it has.

[coqbot]

Comment author: @herbelin

Indeed, this is not related to the "Hint Unfold not" (which is actually also in Logic.v), but on "tauto" trying to use Classical_Prop.NNPP when the later is available.

Maybe it is a bad idea that the intuitionistic vs classical effect of tauto is dependent on the existence of an axiom. I tried to circumvent this but did not find a way.

Maybe providing explicitly some "itauto" and "ctauto"? Don't know what other think.

[coqbot]

Comment author: @JasonGross

One option is to add an option to tauto, e.g., [Set Classical Tauto.], which will use [Classical_Prop.NNPP] if it exists. Possibly have [Set Classical Tauto.] emit a warning if Classical_Prop is not required when it is set. Then you can [Set Classical Tauto] in the Compat86 file. You can possibly also have [tauto] emit a specialized error message to the effect of needing to [Set Classical Tauto] if it encounters a goal which it cannot prove, but which can be proven classically?

[coqbot]

Comment author: @JasonGross

I think that, even if nothing else happens, there should be [Set Classical
Tauto] or [Set Constructive Tauto] or [Set Intuitionistic Tauto]. Having
classical assumptions creep into proofs is unfortunate, and hard to work
around. (I just had to track down a case where [tauto] decided to use
classical axioms rather than contradicting a hypothesis [In x nil], when I
imported Lia.)

[coqbot]

Comment author: @JasonGross

Er, that should say, when I imported Psatz, not Lia.

[ppedrot]

FTR, since the switch to the registering mechanism it is possible to deactivate the classical behaviour of tauto even after Classical_Prop is required. Albeit definitely hackish, it is indeed enough to overwrite core.nnpp.type with a dummy value to make the call to the classical axiom fail, just as when the reference is not available. For instance, this can be done with the following command:

Register tt as core.nnpp.type.

N.B.: registering is Require-bound, so expect modularity issues.