mathlib3 documentation

tactic.tauto

source
meta def tactic.distrib_not  :
tactic unit

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:

source
meta def tactic.tauto_state  :
Type
source
meta def tactic.modify_ref {α : Type} (r : tactic.ref α) (f : α → α) :
tactic unit
source
meta def tactic.add_refl (r : tactic.tauto_state) (e : expr) :
tactic (expr × expr)
source
meta def tactic.add_symm_proof (r : tactic.tauto_state) (e : expr) :
tactic (expr × expr)

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

source
meta def tactic.add_edge (r : tactic.tauto_state) (x y p : expr) :
tactic unit
source
meta def tactic.root (r : tactic.tauto_state) :
expr → tactic (expr × expr)

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

source
meta def tactic.symm_eq (r : tactic.tauto_state) :
expr → expr → tactic 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.

source
meta def tactic.find_eq_type (r : tactic.tauto_state) :
expr → list expr → tactic (expr × expr)
source
meta def tactic.contradiction_with (r : tactic.tauto_state) :
tactic unit
source
meta def tactic.contradiction_symm  :
tactic unit
source
meta def tactic.assumption_with (r : tactic.tauto_state) :
tactic unit
source
meta def tactic.assumption_symm  :
tactic unit
source
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.

source
meta def tactic.tautology (cfg : tactic.tauto_cfg := {classical := bool.ff, closer := has_pure.pure unit.star()}) :
tactic unit
source
meta def tactic.interactive.tautology (c : interactive.parse (optional (lean.parser.tk "!"))) (cfg : tactic.tauto_cfg := {classical := bool.ff, closer := has_pure.pure unit.star()}) :
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.

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

source
meta def tactic.interactive.tauto (c : interactive.parse (optional (lean.parser.tk "!"))) (cfg : tactic.tauto_cfg := {classical := bool.ff, closer := has_pure.pure unit.star()}) :
tactic unit

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.

source
def tactic_doc.tactic.tautology  :
tactic_doc_entry

This tactic (with shorthand 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 variants tautology! and tauto! use the law of excluded middle.

For instance, one can write:

example (p q r : Prop) [decidable p] [decidable r] : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (r ∨ p ∨ r) := by tauto

and the decidability assumptions can be dropped if tauto! is used instead of tauto.

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