# mathlibdocumentation

tactic.tauto

meta def tactic.distrib_not  :

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:

• every node is the type of a hypothesis
• there is a edge between two nodes only if they are provably equivalent
• every edge is labelled with a proof of equivalence for its vertices
• edges are added when normalizing propositions.
meta def tactic.tauto_state  :
Type
meta def tactic.modify_ref {α : Type} (r : tactic.ref α) (f : α → α) :

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

meta def tactic.add_edge (r : tactic.tauto_state) (x y p : expr) :
meta def tactic.root (r : tactic.tauto_state) :

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

meta def tactic.symm_eq (r : tactic.tauto_state) :
expr

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
• classical : bool
• closer :

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.