The list of hypothesis left to work on, renamed to be up-to-date with the current goal.
- currentGoal : Lean.MVarId
The current goal.
State of the
distribNotAt function. We need to carry around the list of
remaining hypothesis as fvars so that we can incrementally apply the
AssertAfterResult.subst from each step to each of them. Otherwise,
they could end up referring to old hypotheses.
The core loop of the
tauto tactic. Repeatedly tries to break down propositions
until no more progress can be made. Tries
contradiction at every
step, to discharge goals as soon as possible. Does not do anything that requires
TODO: The Lean 3 version uses more-powerful versions of
that additionally apply
symm and use a fancy union-find data structure to avoid
tauto breaks down assumptions of the form
_ ∧ _,
_ ∨ _,
_ ↔ _ and
∃ _, _
and splits a goal of the form
_ ∧ _,
_ ↔ _ or
∃ _, _ until it can be discharged
This is a finishing tactic: it either closes the goal or raises an error.
The Lean 3 version of this tactic by default attempted to avoid classical reasoning
where possible. This Lean 4 version makes no such attempt. The
is designed for that purpose.