mathlib documentation

tactic.tauto

find all assumptions of the shape ¬ (p ∧ q) or ¬ (p ∨ q) and replace them using de Morgan's law.

The following definitions maintain a path compression datastructure, i.e. a forest such that:

meta def tactic.tauto_state  :
Type

meta def tactic.modify_ref {α : Type} :
tactic.ref α(α → α)tactic unit

If there exists a symmetry lemma that can be applied to the hypothesis e, store it.

Retrieve the root of the hypothesis e from the proof forest. If e has not been internalized, add it to the proof forest.

Given hypotheses a and b, build a proof that a is equivalent to b, applying congruence and recursing into arguments if a and b are applications of function symbols.

meta structure tactic.tauto_cfg  :
Type

Configuration options for tauto. If classical is tt, runs classical before the rest of tauto. closer is run on any remaining subgoals left by tauto_core; basic_tauto_tacs.

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.

tautology {closer := tac} will use tac on any subgoals created by tautology that it is unable to solve before failing.

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.

tauto {closer := tac} will use tac on any subgoals created by tauto that it is unable to solve before failing.