Lean4
/-- The core loop of the `tauto` tactic. Repeatedly tries to break down propositions
until no more progress can be made. Tries `assumption` and `contradiction` at every
step, to discharge goals as soon as possible. Does not do anything that requires
backtracking.
TODO: The Lean 3 version uses more-powerful versions of `contradiction` and `assumption`
that additionally apply `symm` and use a fancy union-find data structure to avoid
duplicated work.
-/
def tautoCore : TacticM Unit := do
_ ← tryTactic (evalTactic (← `(tactic| contradiction)))
_ ← tryTactic (evalTactic (← `(tactic| assumption)))
iterateUntilFailure do
let gs ← getUnsolvedGoals
allGoals
(liftMetaTactic
(fun m => do
pure [(← m.intros!).2]) <;>
distribNot <;>
liftMetaTactic (casesMatching casesMatcher (recursive := true) (throwOnNoMatch := false)) <;>
(do
_ ← tryTactic (evalTactic (← `(tactic| contradiction)))) <;>
(do
_ ← tryTactic (evalTactic (← `(tactic| refine or_iff_not_imp_left.mpr ?_)))) <;>
liftMetaTactic
(fun m => do
pure [(← m.intros!).2]) <;>
liftMetaTactic
(constructorMatching · coreConstructorMatcher (recursive := true) (throwOnNoMatch := false)) <;>
do
_ ← tryTactic (evalTactic (← `(tactic| assumption))))
let gs' ← getUnsolvedGoals
if gs == gs' then
failure
pure ()
