3
$\begingroup$

When I experiment, I get inconsistent results. Running the following code (with a proof included to double-check that it's provable)

Require Import Classical.

Goal forall P, ~~P -> P. Proof. tauto. Qed.
Goal forall P, P \/ ~P. Proof. exact classic. Qed.
Goal forall P, P \/ ~P. Proof. tauto.

produces the error (on the last goal)

Tactic failure: Classical tauto failed.

which given the name "classical tauto" makes it sound like it's using classical logic, and it couldn't have proved the first goal without classical logic, so what's going on?

I tried looking at the tauto code but it's beyond my current level of understanding.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
2
$\begingroup$

From looking at the Ltac code (https://github.com/coq/coq/blob/d0ed66ddfaa765ad0d9185dd00b68b2fa83cd798/theories/Init/Tauto.v#L97) it seems that tauto in fact has ~~P -> P as its core primitive, rather than P \/ ~P.

What the tactic does is first try to apply NNPP (Try Check NNPP.), and then follow with intuitionistic tauto. I think that as a side effect of having applied NNPP in the first case, it causes the universal quantifier to be instantiated. Once it is, EM can be proven too. Try this:

Theorem em: forall P, P \/ ~P.
Proof. intros. tauto. Qed.
Improve this answer
$\endgroup$
6
  • $\begingroup$ Is applying NNPP to the goal enough to make every classical tautology provable using only intuitionistic logic? $\endgroup$
    – Malcolm Sharpe
    Commented Aug 22, 2022 at 5:35
  • $\begingroup$ If the goal is a tautology of propositional logic, yes. The issue with your setting is that this is not a valid strategy any more once your goal falls out of the propositional fragment, which is the case here due to the introduction, hence the failure. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Aug 22, 2022 at 9:54
  • $\begingroup$ @MalcolmSharpe yes, see this proof, which uses only intuitionistic rules. $\endgroup$
    – corwin.amber
    Commented Aug 23, 2022 at 8:26
  • $\begingroup$ Thanks for the link, but I think I was unclear with my question: although freely using NNPP gets you the full power of classical logic (as the link explains), the behavior you describe of classical tauto (if I understand correctly) is to use NNPP only once and only on the initial goal. It's not clear to me whether this very limited use of NNPP gives you as much power as using it freely. (At this point though I'm just curious.) $\endgroup$
    – Malcolm Sharpe
    Commented Aug 24, 2022 at 4:50
  • 2
    $\begingroup$ The answer is yes, in the setting of propositional logic. This is usually called Glivenko’s theorem, and is one of many double-negation translations that map classically provable facts to intuitionistically provable ones using double negation at well-chosen places. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Aug 24, 2022 at 9:30
2
$\begingroup$

There is a difference between trying to prove forall P, P \/ ~ P and trying to prove P \/ ~P where P : Prop. To get from the former to the latter you need to do an intro, after which tauto works:

Require Import Classical.

Goal forall P, ~~P -> P. Proof. intro. tauto. Qed.
Goal forall P, P \/ ~P. Proof. intro. tauto. Qed.
Goal forall P, P \/ ~P. Proof. intro. tauto. Qed.

You are just lucky that forall P, ~~P -> P can be proved using tauto because it just so happens that the goal precisely matches the axiom NNPP imported by Classical, so tauto just uses NNPP directly.

Improve this answer
$\endgroup$
1
  • $\begingroup$ That's surprising that intro makes a difference here, since the docs say "Moreover, if it has nothing else to do, tauto performs introductions. Therefore, the use of intros in the previous proof is unnecessary." However, the docs also only say that tauto succeeds on intuitionistic tautologies, so maybe classical tauto has different behavior. (Also, it seems to be classic that is the axiom in Coq.Logic.Classical_Prop rather than NNPP, although I don't see why it should matter either way, except as a quirk of code as described by @corwin.amber in their answer.) $\endgroup$
    – Malcolm Sharpe
    Commented Aug 22, 2022 at 5:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.