Commit 2021-12-30 21:39 e1a8b886

feat(tactic/itauto): add support for [decidable p] assumptions (#10744) 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.)