find all assumptions of the shape ¬ (p ∧ q) or ¬ (p ∨ q) and
replace them using de Morgan's law.
def
tactic.interactive.tautology
:
interactive.parse (optional (lean.parser.tk "!")) → tactic unit
tautology breaks down assumptions of the form _ ∧ _, _ ∨ _, _ ↔ _ and ∃ _, _
and splits a goal of the form _ ∧ _, _ ↔ _ or ∃ _, _ until it can be discharged
using reflexivity or solve_by_elim.
This is a finishing tactic: it either closes the goal or raises an error.
The variant tautology! uses the law of excluded middle.
tauto breaks down assumptions of the form _ ∧ _, _ ∨ _, _ ↔ _ and ∃ _, _
and splits a goal of the form _ ∧ _, _ ↔ _ or ∃ _, _ until it can be discharged
using reflexivity or solve_by_elim.
This is a finishing tactic: it either closes the goal or raises an error.
The variant tauto! uses the law of excluded middle.