Improve error message of `tauto`

Stream: mathlib4

[Jon Eugster]

Currently, if tauto fails, I find the error messages and proof state a bit confusing. It only shows the "unsolved goals" message which appears in various other contexts too, like having an incomplete proof skeleton, etc.

What would people think about adding an error message like "tauto failed" if tauto failed to make this clearer?

Here's a suggestion of what I'd like the behaviour to be:

MWE

import Mathlib.Tactic.Tauto

-- Current behaviour:
example (h : x = 2) : x ^ 2 = 4 := by
  tauto -- Error:
  -- unsolved goals
  -- x: ℕ
  -- h: x = 2
  -- em✝: (a : Prop) → Decidable a
  -- ⊢ x ^ 2 = 4
  simp


open Lean Elab Parser Tactic
open Mathlib.Tactic Tauto
namespace tactic.Tauto

def tautology : TacticM Unit := focus do
  evalTactic (← `(tactic| classical!))
  tautoCore
  allGoals (iterateUntilFailure
    (evalTactic (← `(tactic| rfl)) <|>
     evalTactic (← `(tactic| solve_by_elim)) <|>
     liftMetaTactic (constructorMatching · finishingConstructorMatcher)))

  -- Add some error message to the implementation of `tauto`
  if (← getUnsolvedGoals).length > 0 then logError "tauto failed."

  done

syntax (name := tauto') "tauto'" (config)? : tactic

elab_rules : tactic | `(tactic| tauto' $[$cfg:config]?) => do
  let _cfg ← elabConfig (mkOptionalNode cfg)
  tautology

-- Proposed behaviour
example (h : x = 2) : x ^ 2 = 4 := by
  tauto' -- Errors:
  -- tauto failed.
  --
  -- unsolved goals
  -- x: ℕ
  -- h: x = 2
  -- em✝: (a : Prop) → Decidable a
  -- ⊢ x ^ 2 = 4
  simp

[Eric Wieser]

Should there be a variant of focus that accepts a string title to describe the focus operation that failed? focus_with "tauto" (tacs)?

[Jon Eugster]

@Eric Wieser something like this?

-- `focusAndDone` already exists in core, modify it to take an error message
def focusAndDoneWithError (m : MessageData) (tactic : TacticM α) : TacticM α :=
  focus do
    let a ← tactic

    -- modified code of `done` to throw the error message
    let gs ← getUnsolvedGoals
    unless gs.isEmpty do
      logError m
      Term.reportUnsolvedGoals gs
      throwAbortTactic

    pure a

MWE

import Mathlib.Tactic.Tauto

open Lean Elab Parser Tactic
open Mathlib.Tactic Tauto

namespace tactic.Tauto

-- `focusAndDone` already exists in core, modify it to take an error message
def focusAndDoneWithError (m : MessageData) (tactic : TacticM α) : TacticM α :=
  focus do
    let a ← tactic

    -- modified code of `done` to throw the error message
    let gs ← getUnsolvedGoals
    unless gs.isEmpty do
      logError m
      Term.reportUnsolvedGoals gs
      throwAbortTactic

    pure a

def tautology : TacticM Unit := focusAndDoneWithError "tauto failed." do
  evalTactic (← `(tactic| classical!))
  tautoCore
  allGoals (iterateUntilFailure
    (evalTactic (← `(tactic| rfl)) <|>
     evalTactic (← `(tactic| solve_by_elim)) <|>
     liftMetaTactic (constructorMatching · finishingConstructorMatcher)))

syntax (name := tauto') "tauto'" (config)? : tactic

elab_rules : tactic | `(tactic| tauto' $[$cfg:config]?) => do
  let _cfg ← elabConfig (mkOptionalNode cfg)
  tautology


example (h : x = 2) : x ^ 2 = 4 := by
  tauto' -- Error:
-- tauto failed
--
-- unsolved goals
-- x: ℕ
-- h: x = 2
-- em✝: (a : Prop) → Decidable a
-- ⊢ x ^ 2 = 4
  done

[Eric Wieser]

What does it do if something fails within tauto?

[Eric Wieser]

(also note that focusAndDone was called solve in lean 3) nevermind, I see you're matching core's docs#Lean.Elab.Tactic.focusAndDone

[Jon Eugster]

currently tauto is implemented as

focus do
  [yada yada]
  done

which I think should be exactly equivalent to

focusAndDone do
  [yada yada]

from core :+1:

[Jon Eugster]

and all the code above does is adding tauto failed iff unsolved goals is displayed currently.

What would be a case that tauto fails internally?

[Eric Wieser]

I'm suggesting something like:

-- `focusAndDone` already exists in core, modify it to take a scope name
def focusAndDoneWithScope (m : MessageData) (tactic : TacticM α) : TacticM α :=
  focus do
    try
       let a ← tactic
   catch e =>
       throwError sorry -- combine m and e

    -- modified code of `done` to throw the error message
    let gs ← getUnsolvedGoals
    unless gs.isEmpty do
      logError m!"{m} could not solve some goals"
      Term.reportUnsolvedGoals gs
      throwAbortTactic

[Eric Wieser]

That is, distinguish the tactic crashing from it failing to close a goal

[Eric Wieser]

Maybe docs#Lean.Elab.throwAbortTactic does some of this for you though