Lean4
/-- A decision procedure for intuitionistic propositional logic. Unlike `finish` and `tauto!` this
tactic never uses the law of excluded middle (without the `!` option), and the proof search is
tailored for this use case. (`itauto!` will work as a classical SAT solver, but the algorithm is
not very good in this situation.)
```lean
example (p : Prop) : ¬ (p ↔ ¬ p) := by itauto
```
`itauto [a, b]` will additionally attempt case analysis on `a` and `b` assuming that it can derive
`Decidable a` and `Decidable b`. `itauto *` will case on all decidable propositions that it can
find among the atomic propositions, and `itauto! *` will case on all propositional atoms.
*Warning:* This can blow up the proof search, so it should be used sparingly.
-/
@[tactic_parser 1000]
public meta def itauto : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.ITauto.itauto 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "itauto" false✝)
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "!")))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ " *" `token.« *» (ParserDescr.symbol✝ " *"))
(ParserDescr.unary✝¹ `group
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " [")
((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.cat✝ `term 0) ","
(ParserDescr.symbol✝ ", ") Bool.false✝))
(ParserDescr.symbol✝ "]"))))))
