fix(library/definitional): marking cases_on and rec_on as reducible

The idea is to avoid counter-intuitive behavior

src/library/definitional/cases_on.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/module.h"
 #include "library/protected.h"
+#include "library/reducible.h"
 
 namespace lean {
 static void throw_corrupted(name const & n) {
@@ -178,6 +179,7 @@ environment mk_cases_on(environment const & env, name const & n) {
     declaration new_d = mk_definition(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value,
                                       opaque, rec_decl.get_module_idx(), use_conv_opt);
     environment new_env = module::add(env, check(env, new_d));
+    new_env = set_reducible(new_env, cases_on_name, reducible_status::On);
     return add_protected(new_env, cases_on_name);
 }
 }

src/library/definitional/rec_on.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/inductive/inductive.h"
 #include "library/module.h"
+#include "library/reducible.h"
 #include "library/protected.h"
 
 namespace lean {
@@ -53,8 +54,10 @@ environment mk_rec_on(environment const & env, name const & n) {
     bool opaque       = false;
     bool use_conv_opt = true;
     environment new_env = module::add(env,
-                                      check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(), rec_on_type, rec_on_val,
+                                      check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(),
+                                                               rec_on_type, rec_on_val,
                                                                opaque, rec_decl.get_module_idx(), use_conv_opt)));
+    new_env = set_reducible(new_env, rec_on_name, reducible_status::On);
     return add_protected(new_env, rec_on_name);
 }
 }

tests/lean/run/elab_failure.lean

@@ -0,0 +1,15 @@
+import data.nat.basic data.bool
+open bool nat
+reducible nat.rec_on
+definition is_eq (a b : nat) : bool :=
+nat.rec_on a
+  (λ b, nat.cases_on b tt (λb₁, ff))
+  (λ a₁ r₁ b, nat.cases_on b ff (λb₁, r₁ b₁))
+  b
+
+example (a₁ : nat) (b : nat) : true :=
+@nat.cases_on (λ (n : nat), true) b
+  true.intro
+  (λ (b₁ : _),
+     have aux : is_eq a₁ b₁ = is_eq (succ a₁) (succ b₁), from rfl,
+     true.intro)