feat(library/equations_compiler/wf_rec): improve error message for failed decreasing proofs

library/init/meta/well_founded_tactics.lean

@@ -147,7 +147,7 @@ comp_val
 <|>
 assumption
 <|>
-fail "failed to prove function is descreasing"
+failed
 end simple_dec_tac
 
 meta def default_dec_tac : tactic unit :=

src/library/equations_compiler/wf_rec.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/instantiate.h"
+#include "kernel/error_msgs.h"
 #include "library/type_context.h"
 #include "library/trace.h"
 #include "library/constants.h"
@@ -500,7 +501,36 @@ struct wf_rec_fn {
         init(eqns, wf_tacs);
 
         /* Eliminate recursion using functional. */
-        eqns = elim_recursion(eqns);
+        try {
+            eqns = elim_recursion(eqns);
+        } catch (exception_with_pos & ex) {
+            expr R = m_R;
+            bool using_well_founded = is_wf_equations(eqns);
+            throw nested_exception(
+                ex.get_pos(),
+                [=](formatter const & fmt) {
+                    format r;
+                    formatter _fmt = fmt;
+                    if (is_app_of(R, get_has_well_founded_r_name())) {
+                        options o = fmt.get_options();
+                        o         = o.update_if_undef(get_pp_implicit_name(), true);
+                        _fmt      = fmt.update_options(o);
+                    }
+                    r += format("failed to prove recursive application is decreasing, well founded relation");
+                    r += pp_indent_expr(_fmt, R);
+                    if (!using_well_founded) {
+                        r += line() + format("Possible solutions: ");
+                        r += line() + format("  - Use 'using_well_founded' keyword in the end of your definition "
+                                             "to specify tactics for synthesizing well founded relations and "
+                                             "decreasing proofs.");
+                        r += line() + format("  - The default decreasing tactic uses the 'assumption' tactic, "
+                                             "thus hints (aka local proofs) can be provided using 'have'-expressions.");
+                    }
+                    r += line() + format("The nested exception contains the failure state for the decreasing tactic.");
+                    return r;
+                },
+                ex);
+        }
         trace_debug_wf(tout() << "after elim_recursion\n" << eqns << "\n";);
 
         /* Eliminate pattern matching */

tests/lean/eqn_hole.lean.expected.out

@@ -8,7 +8,14 @@ context:
 g : ℕ → ℕ,
 n : ℕ
 ⊢ ℕ
-eqn_hole.lean:8:11: error: failed to prove function is descreasing
+eqn_hole.lean:8:11: error: failed to prove recursive application is decreasing, well founded relation
+  @has_well_founded.r ℕ (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof)
+Possible solutions: 
+  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
+  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
+The nested exception contains the failure state for the decreasing tactic.
+nested exception message:
+failed
 state:
 g : ℕ → ℕ,
 n : ℕ

tests/lean/nested_match.lean

@@ -0,0 +1,30 @@
+namespace ex1
+
+def f : ℕ → ℕ
+| n :=
+  (match n with
+  | 0 := 0
+  | (m+1) := f m
+  end) + 1
+
+def g  : ℕ → ℕ
+| n :=
+  (match n, rfl : ∀ m, m = n → ℕ with
+  | 0,     h := 0
+  | (m+1), h :=
+    have m < n, begin rw [-h], apply nat.lt_succ_self end,
+    g m
+  end) + 1
+
+end ex1
+
+namespace ex2
+
+mutual def f, g
+with f : ℕ → ℕ
+| n := g n + 1
+with g : ℕ → ℕ
+| 0 := 0
+| (n+1) := f n
+
+end ex2

tests/lean/nested_match.lean.expected.out

@@ -0,0 +1,24 @@
+nested_match.lean:7:13: error: failed to prove recursive application is decreasing, well founded relation
+  @has_well_founded.r ℕ (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof)
+Possible solutions: 
+  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
+  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
+The nested exception contains the failure state for the decreasing tactic.
+nested exception message:
+failed
+state:
+f : ℕ → ℕ,
+n m : ℕ
+⊢ m < n
+nested_match.lean:25:7: error: failed to prove recursive application is decreasing, well founded relation
+  @has_well_founded.r (psum ℕ ℕ)
+    (@has_well_founded_of_has_sizeof (psum ℕ ℕ) (@psum.has_sizeof ℕ ℕ nat.has_sizeof nat.has_sizeof))
+Possible solutions: 
+  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
+  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
+The nested exception contains the failure state for the decreasing tactic.
+nested exception message:
+failed
+state:
+n : ℕ
+⊢ 1 < 1