feat(frontends/lean): add auto_param gadget

library/init/meta/name.lean

@@ -12,6 +12,13 @@ inductive name
 | mk_string  : string → name → name
 | mk_numeral : unsigned → name → name
 
+/-- Gadget for automatic parameter support. This is similar to the opt_param gadget, but it uses
+    the tactic declaration names tac_name to synthesize the argument.
+    Like opt_param, this gadget only affects elaboration.
+    For example, the tactic will *not* be invoked during type class resolution. -/
+@[reducible] def {u} auto_param (α : Sort u) (tac_name : name) : Sort u :=
+α
+
 instance : inhabited name :=
 ⟨name.anonymous⟩
 

src/frontends/lean/elaborator.cpp

@@ -1135,6 +1135,14 @@ static optional<expr> is_optional_param(expr const & e) {
     }
 }
 
+static optional<expr_pair> is_auto_param(expr const & e) {
+    if (is_app_of(e, get_auto_param_name(), 2)) {
+        return optional<expr_pair>(app_arg(app_fn(e)), app_arg(e));
+    } else {
+        return optional<expr_pair>();
+    }
+}
+
 static optional<expr> is_thunk(expr const & e) {
     if (is_app_of(e, get_thunk_name(), 1)) {
         return some_expr(app_arg(e));
@@ -1150,6 +1158,33 @@ static expr mk_thunk_if_needed(expr const & e, optional<expr> const & is_thunk)
         return e;
 }
 
+static optional<name> name_lit_to_name(expr const & name_lit) {
+    if (is_constant(name_lit, get_name_anonymous_name()))
+        return optional<name>(name());
+    if (is_app_of(name_lit, get_name_mk_string_name(), 2)) {
+        if (auto str = to_string(app_arg(app_fn(name_lit))))
+        if (auto p   = name_lit_to_name(app_arg(name_lit)))
+            return optional<name>(name(*p, str->c_str()));
+    }
+    return optional<name>();
+}
+
+expr elaborator::mk_auto_param(expr const & name_lit, expr const & expected_type, expr const & ref) {
+    auto c = name_lit_to_name(name_lit);
+    if (!c)
+        throw elaborator_exception(ref, format("invalid auto_param, name literal expected for identifying tactic") +
+                                   pp_indent(name_lit));
+    auto d = m_env.find(*c);
+    if (!d)
+        throw elaborator_exception(ref, sstream() << "invalid auto_param, unknown tactic '" << *c << "'");
+    if (!m_ctx.is_def_eq(d->get_type(), mk_tactic_unit()))
+        throw elaborator_exception(ref, format("invalid auto_param, invalid tactic '") + format(*c) +
+                                   format("' type should be (tactic unit)") +
+                                   pp_indent(d->get_type()));
+    expr t = copy_tag(ref, mk_by(copy_tag(ref, mk_constant(*c))));
+    return visit(t, some_expr(expected_type));
+}
+
 /* Check if fn args resulting type matches the expected type, and fill
    first_pass_info & info with information collected in this first pass.
    Return true iff the types match.
@@ -1168,7 +1203,7 @@ void elaborator::first_pass(expr const & fn, buffer<expr> const & args,
     while (is_pi(type)) {
         binder_info const & bi = binding_info(type);
         expr const & d = binding_domain(type);
-        if (bi.is_strict_implicit() && i == args.size() && !is_optional_param(d))
+        if (bi.is_strict_implicit() && i == args.size() && !is_optional_param(d) && !is_auto_param(d))
             break;
         expr new_arg;
         if (!is_explicit(bi)) {
@@ -1190,6 +1225,8 @@ void elaborator::first_pass(expr const & fn, buffer<expr> const & args,
             info.new_instances_size.push_back(info.new_instances.size());
         } else if (auto def_value = is_optional_param(d)) {
             new_arg = *def_value;
+        } else if (auto p = is_auto_param(d)) {
+            new_arg = mk_auto_param(p->second, p->first, ref);
         } else {
             break;
         }
@@ -1304,7 +1341,7 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer<
             binder_info const & bi = binding_info(type);
             expr const & d = binding_domain(type);
             expr new_arg;
-            if (amask == arg_mask::Default && bi.is_strict_implicit() && i == args.size() && !is_optional_param(d))
+            if (amask == arg_mask::Default && bi.is_strict_implicit() && i == args.size() && !is_optional_param(d) && !is_auto_param(d))
                 break;
             if ((amask == arg_mask::Default && !is_explicit(bi)) ||
                 (amask == arg_mask::InstHoExplicit && !is_explicit(bi) && !bi.is_inst_implicit() && !is_pi(d))) {
@@ -1346,6 +1383,8 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer<
                 i++;
             } else if (auto def_value = is_optional_param(d)) {
                 new_arg = *def_value;
+            } else if (auto p = is_auto_param(d)) {
+                new_arg = mk_auto_param(p->second, p->first, ref);
             } else {
                 break;
             }

src/frontends/lean/elaborator.h

@@ -252,6 +252,8 @@ private:
 
     void finalize_core(sanitize_param_names_fn & S, buffer<expr> & es,
                        bool check_unassigned, bool to_simple_metavar, bool collect_local_ctx);
+
+    expr mk_auto_param(expr const & name_lit, expr const & expected_type, expr const & ref);
 public:
     elaborator(environment const & env, options const & opts, name const & decl_name,
                metavar_context const & mctx, local_context const & lctx,

src/frontends/lean/util.cpp

@@ -338,7 +338,7 @@ pair<name, option_kind> parse_option_name(parser & p, char const * error_msg) {
 }
 
 expr mk_tactic_unit() {
-    return mk_app(mk_constant(get_tactic_name(), {mk_level_one()}), mk_constant(get_unit_name()));
+    return mk_app(mk_constant(get_tactic_name(), {mk_level_zero()}), mk_constant(get_unit_name()));
 }
 
 expr quote_name(name const & n) {

src/library/constants.cpp

@@ -15,6 +15,7 @@ name const * g_and = nullptr;
 name const * g_and_elim_left = nullptr;
 name const * g_and_elim_right = nullptr;
 name const * g_and_intro = nullptr;
+name const * g_auto_param = nullptr;
 name const * g_bit0 = nullptr;
 name const * g_bit1 = nullptr;
 name const * g_bool = nullptr;
@@ -495,6 +496,7 @@ void initialize_constants() {
     g_and_elim_left = new name{"and", "elim_left"};
     g_and_elim_right = new name{"and", "elim_right"};
     g_and_intro = new name{"and", "intro"};
+    g_auto_param = new name{"auto_param"};
     g_bit0 = new name{"bit0"};
     g_bit1 = new name{"bit1"};
     g_bool = new name{"bool"};
@@ -976,6 +978,7 @@ void finalize_constants() {
     delete g_and_elim_left;
     delete g_and_elim_right;
     delete g_and_intro;
+    delete g_auto_param;
     delete g_bit0;
     delete g_bit1;
     delete g_bool;
@@ -1456,6 +1459,7 @@ name const & get_and_name() { return *g_and; }
 name const & get_and_elim_left_name() { return *g_and_elim_left; }
 name const & get_and_elim_right_name() { return *g_and_elim_right; }
 name const & get_and_intro_name() { return *g_and_intro; }
+name const & get_auto_param_name() { return *g_auto_param; }
 name const & get_bit0_name() { return *g_bit0; }
 name const & get_bit1_name() { return *g_bit1; }
 name const & get_bool_name() { return *g_bool; }

src/library/constants.h

@@ -17,6 +17,7 @@ name const & get_and_name();
 name const & get_and_elim_left_name();
 name const & get_and_elim_right_name();
 name const & get_and_intro_name();
+name const & get_auto_param_name();
 name const & get_bit0_name();
 name const & get_bit1_name();
 name const & get_bool_name();

src/library/constants.txt

@@ -10,6 +10,7 @@ and
 and.elim_left
 and.elim_right
 and.intro
+auto_param
 bit0
 bit1
 bool

tests/lean/run/auto_param.lean

@@ -0,0 +1,29 @@
+open tactic
+
+meta def my_tac : tactic unit :=
+assumption <|> abstract (comp_val >> skip) <|> fail "my_tac failed to synthesize auto_param"
+
+def f (x : nat) (h : auto_param (x > 0) `my_tac) : nat :=
+nat.pred x
+
+check f 12
+check f 13
+
+lemma f_inj {x₁ x₂ : nat} {h₁ : x₁ > 0} {h₂ : x₂ > 0} : f x₁ = f x₂ → x₁ = x₂ :=
+begin
+  unfold f, intro h,
+  cases x₁,
+  exact absurd h₁ (lt_irrefl _),
+  cases x₂,
+  exact absurd h₂ (lt_irrefl _),
+  apply congr_arg nat.succ,
+  assumption
+end
+
+check @f_inj
+
+lemma f_def {x : nat} (h : x > 0) : f x = nat.pred x :=
+rfl
+
+-- The following is an error
+-- check λ x, f x