feat: improve error messages and docstring for decide tactic (#3422)

The `decide` tactic produces error messages that users find to be
obscure. Now:
1. If the `Decidable` instance reduces to `isFalse`, it reports that
`decide` failed because the proposition is false.
2. If the `Decidable` instance fails to reduce, it explains what
proposition it failed for, and it shows the reduced `Decidable` instance
rather than the `Decidable.decide` expression. That expression tends to
be less useful since it shows the unreduced `Decidable` argument (plus
it's a lot longer!)

Examples:
```lean
example : 1 ≠ 1 := by decide
/-
tactic 'decide' proved that the proposition
  1 ≠ 1
is false
-/

opaque unknownProp : Prop

open scoped Classical in
example : unknownProp := by decide
/-
tactic 'decide' failed for proposition
  unknownProp
since its 'Decidable' instance reduced to
  Classical.choice ⋯
rather than to the 'isTrue' constructor.
-/
```

When reporting the error, `decide` only shows the whnf of the
`Decidable` instance. In the future we could consider having it reduce
all decidable instances present in the term, which can help with
determining the cause of failure (this was explored in
8cede580690faa5ce18683f168838b08b372bacb).

RELEASES.md

@@ -81,6 +81,8 @@ v4.7.0 (development in progress)
   In both cases, `h` is applicable because `simp` does not index f-arguments anymore when adding `h` to the `simp`-set.
   It's important to note, however, that global theorems continue to be indexed in the usual manner.
 
+* Improved the error messages produced by the `decide` tactic. [#3422](https://github.com/leanprover/lean4/pull/3422)
+
 Breaking changes:
 * `Lean.withTraceNode` and variants got a stronger `MonadAlwaysExcept` assumption to
   fix trace trees not being built on elaboration runtime exceptions. Instances for most elaboration

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -372,10 +372,24 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let d ← instantiateMVars d
-    let r ← withDefault <| whnf d
-    unless r.isConstOf ``true do
-      throwError "failed to reduce to 'true'{indentExpr r}"
-    let s := d.appArg! -- get instance from `d`
+    -- Get instance from `d`
+    let s := d.appArg!
+    -- Reduce the instance rather than `d` itself, since that gives a nicer error message on failure.
+    let r ← withDefault <| whnf s
+    if r.isAppOf ``isFalse then
+      throwError "\
+        tactic 'decide' proved that the proposition\
+        {indentExpr expectedType}\n\
+        is false"
+    unless r.isAppOf ``isTrue do
+      throwError "\
+        tactic 'decide' failed for proposition\
+        {indentExpr expectedType}\n\
+        since its 'Decidable' instance reduced to\
+        {indentExpr r}\n\
+        rather than to the 'isTrue' constructor."
+    -- While we have a proof from reduction, we do not embed it in the proof term,
+    -- but rather we let the kernel recompute it during type checking from a more efficient term.
     let rflPrf ← mkEqRefl (toExpr true)
     return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
 

src/Lean/Parser/Tactic.lean

@@ -66,13 +66,60 @@ doing a pattern match. This is equivalent to `fun` with match arms in term mode.
 @[builtin_tactic_parser] def introMatch := leading_parser
   nonReservedSymbol "intro" >> matchAlts
 
-/-- `decide` will attempt to prove a goal of type `p` by synthesizing an instance
-of `Decidable p` and then evaluating it to `isTrue ..`. Because this uses kernel
-computation to evaluate the term, it may not work in the presence of definitions
-by well founded recursion, since this requires reducing proofs.
-```
+/--
+`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`
+and then reducing that instance to evaluate the truth value of `p`.
+If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.
+
+Limitations:
+- The target is not allowed to contain local variables or metavariables.
+  If there are local variables, you can try first using the `revert` tactic with these local variables
+  to move them into the target, which may allow `decide` to succeed.
+- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined
+  by well-founded recursion might not work, because evaluating them requires reducing proofs.
+  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.
+  These can appear for instances defined using tactics (such as `rw` and `simp`).
+  To avoid this, use definitions such as `decidable_of_iff` instead.
+
+## Examples
+
+Proving inequalities:
+```lean
 example : 2 + 2 ≠ 5 := by decide
 ```
+
+Trying to prove a false proposition:
+```lean
+example : 1 ≠ 1 := by decide
+/-
+tactic 'decide' proved that the proposition
+  1 ≠ 1
+is false
+-/
+```
+
+Trying to prove a proposition whose `Decidable` instance fails to reduce
+```lean
+opaque unknownProp : Prop
+
+open scoped Classical in
+example : unknownProp := by decide
+/-
+tactic 'decide' failed for proposition
+  unknownProp
+since its 'Decidable' instance reduced to
+  Classical.choice ⋯
+rather than to the 'isTrue' constructor.
+-/
+```
+
+## Properties and relations
+
+For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.
+```lean
+example : 1 + 1 = 2 := by decide
+example : 1 + 1 = 2 := by rfl
+```
 -/
 @[builtin_tactic_parser] def decide := leading_parser
   nonReservedSymbol "decide"

tests/lean/2161.lean.expected.out

@@ -1,6 +1,12 @@
-2161.lean:15:48-15:54: error: failed to reduce to 'true'
-  Decidable.rec (fun h => (fun x => false) h) (fun h => (fun x => true) h)
-    (instDecidableEqFoo (mul (mul (mul 4 1) 1) 1) 4)
-2161.lean:22:48-22:54: error: failed to reduce to 'true'
-  Decidable.rec (fun h => (fun x => false) h) (fun h => (fun x => true) h)
-    (instDecidableEqFoo (add (add (add 4 1) 1) 1) 4)
+2161.lean:15:48-15:54: error: tactic 'decide' failed for proposition
+  mul (mul (mul 4 1) 1) 1 = 4
+since its 'Decidable' instance reduced to
+  Decidable.rec (fun h => (fun h => isFalse ⋯) h) (fun h => (fun h => h ▸ isTrue ⋯) h)
+    (instDecidableEqNat (mul (mul (mul 4 1) 1) 1).num 4)
+rather than to the 'isTrue' constructor.
+2161.lean:22:48-22:54: error: tactic 'decide' failed for proposition
+  add (add (add 4 1) 1) 1 = 4
+since its 'Decidable' instance reduced to
+  Decidable.rec (fun h => (fun h => isFalse ⋯) h) (fun h => (fun h => h ▸ isTrue ⋯) h)
+    (instDecidableEqNat (add (add (add 4 1) 1) 1).num 4)
+rather than to the 'isTrue' constructor.

tests/lean/decideTactic.lean

@@ -0,0 +1,21 @@
+/-!
+# Tests of the `decide` tactic
+-/
+
+/-!
+Success
+-/
+example : 2 + 2 ≠ 5 := by decide
+
+/-!
+False proposition
+-/
+example : 1 ≠ 1 := by decide
+
+/-!
+Irreducible decidable instance
+-/
+opaque unknownProp : Prop
+
+open scoped Classical in
+example : unknownProp := by decide

tests/lean/decideTactic.lean.expected.out

@@ -0,0 +1,8 @@
+decideTactic.lean:13:22-13:28: error: tactic 'decide' proved that the proposition
+  1 ≠ 1
+is false
+decideTactic.lean:21:28-21:34: error: tactic 'decide' failed for proposition
+  unknownProp
+since its 'Decidable' instance reduced to
+  Classical.choice ⋯
+rather than to the 'isTrue' constructor.