[Merged by Bors] - feat(tactic/itauto): add support for [decidable p] assumptions

[digama0]

This allows proving theorems like the following, which use excluded middle selectively through decidable assumptions:

example (p q r : Prop) [decidable p] : (p → (q ∨ r)) → ((p → q) ∨ (p → r)) := by itauto

This also fixes a bug in the proof search order of the original itauto implementation causing nontermination in one of the new tests, which also makes the "big test" at the end run instantly.

Also adds a ! option to enable decidability for all propositions using classical logic.

Because adding decidability instances can be expensive for proof search, they are disabled by default. You can specify specific decidable instances to add by itauto [p, q], or use itauto* which adds all decidable atoms. (The ! option is useless on its own, and should be combined with * or [p] options.)

[robertylewis]

What's the relation now between itauto! and tauto? And tauto!? Is there any real difference between tauto and tauto!? (I had the vague memory that the former became the latter at some point, but it still parses the !.)

import tactic

example (p : Prop) : p ∨ ¬ p :=
by tauto

[ericrbg]

tauto! definitely does something more than tauto; I've had problems only one can solve. Mario said here:

Eric Rodriguez: is itauto! just a strictly better tauto! now?

Mario Carneiro: I believe so. tauto works on some heuristic instantiation stuff so it might be able to do some problems that aren't technically propositional logic, like A -> (A -> B) -> B where A and B are types

[robertylewis]

So tauto isn't intuitionistic, but weaker than tauto!, and itauto! isn't intuitionistic (despite the i) and is incomparable to tauto!. finish and friends are also incomparable, despite the description (like tauto) being "prop logic + heuristic instantiation."

This is a mess that needs cleaning. Will post on Zulip in a bit.

[digama0]

Given the situation with exponential blowup, I've reverted the default behavior of itauto to the previous version, where decidability instances are ignored. To turn on splitting on decidability instances, you can use itauto*, or itauto [p] for more controlled splitting.

[robertylewis]

Thanks for the changes!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests