feat(library/type_context, library/tactic): add eta-expansion method and tactic

library/init/meta/tactic.lean

@@ -220,6 +220,7 @@ meta_constant rename        : name → name → tactic unit
 meta_constant clear         : expr → tactic unit
 meta_constant revert_lst    : list expr → tactic nat
 meta_constant whnf_core     : transparency → expr → tactic expr
+meta_constant eta_expand    : expr → tactic expr
 meta_constant unify_core    : transparency → expr → expr → tactic unit
 /- Infer the type of the given expression.
    Remark: transparency does not affect type inference -/

src/library/tactic/tactic_state.cpp

@@ -309,6 +309,16 @@ vm_obj tactic_whnf_core(vm_obj const & t, vm_obj const & e, vm_obj const & s0) {
     }
 }
 
+vm_obj tactic_eta_expand(vm_obj const & e, vm_obj const & s0) {
+    tactic_state const & s = to_tactic_state(s0);
+    type_context ctx       = mk_type_context_for(s);
+    try {
+        return mk_tactic_success(to_obj(ctx.eta_expand(to_expr(e))), s);
+    } catch (exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
 vm_obj tactic_is_class(vm_obj const & e, vm_obj const & s0) {
     tactic_state const & s = to_tactic_state(s0);
     type_context ctx       = mk_type_context_for(s);
@@ -492,6 +502,7 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "format_result"}),        tactic_format_result);
     DECLARE_VM_BUILTIN(name({"tactic", "infer_type"}),           tactic_infer_type);
     DECLARE_VM_BUILTIN(name({"tactic", "whnf_core"}),            tactic_whnf_core);
+    DECLARE_VM_BUILTIN(name({"tactic", "eta_expand"}),           tactic_eta_expand);
     DECLARE_VM_BUILTIN(name({"tactic", "is_class"}),             tactic_is_class);
     DECLARE_VM_BUILTIN(name({"tactic", "mk_instance"}),          tactic_mk_instance);
     DECLARE_VM_BUILTIN(name({"tactic", "unify_core"}),           tactic_unify_core);

src/library/type_context.cpp

@@ -2529,6 +2529,31 @@ optional<expr> type_context::mk_subsingleton_instance(expr const & type) {
     return r;
 }
 
+/* -------------
+   Auxiliary
+   ------------- */
+
+expr type_context::eta_expand(expr const & e) {
+    tmp_locals locals(*this);
+    expr it = e;
+    while (is_lambda(it)) {
+        expr d = instantiate_rev(binding_domain(it), locals.as_buffer().size(), locals.as_buffer().data());
+        locals.push_local(binding_name(it), d, binding_info(it));
+        it     = binding_body(it);
+    }
+    it = instantiate_rev(it, locals.as_buffer().size(), locals.as_buffer().data());
+    expr it_type = relaxed_whnf(infer(it));
+    if (!is_pi(it_type)) return e;
+    buffer<expr> extra_args;
+    while (is_pi(it_type)) {
+        expr arg = locals.push_local_from_binding(it_type);
+        extra_args.push_back(arg);
+        it_type  = relaxed_whnf(instantiate(binding_body(it_type), arg));
+    }
+    expr r = mk_app(it, extra_args);
+    return locals.mk_lambda(r);
+}
+
 tmp_type_context::tmp_type_context(type_context & tctx, unsigned num_umeta, unsigned num_emeta): m_tctx(tctx) {
     m_tmp_uassignment.resize(num_umeta, none_level());
     m_tmp_eassignment.resize(num_emeta, none_expr());

src/library/type_context.h

@@ -265,6 +265,8 @@ public:
     transparency_mode mode() const { return m_transparency_mode; }
     unsigned mode_idx() const { return static_cast<unsigned>(mode()); }
 
+    expr eta_expand(expr const & e);
+
     struct transparency_scope : public flet<transparency_mode> {
         transparency_scope(type_context & ctx, transparency_mode m):
             flet<transparency_mode>(ctx.m_transparency_mode, m) {

tests/lean/eta_tac.lean

@@ -0,0 +1,13 @@
+open tactic
+
+set_option pp.binder_types true
+set_option pp.implicit true
+set_option pp.notation false
+
+example (a : nat) : true :=
+by do
+  mk_const `add >>= eta_expand >>= trace,
+  mk_const `nat.succ >>= eta_expand >>= trace,
+  to_expr `(add a) >>= eta_expand >>= trace,
+  to_expr `(λ x : nat, add x) >>= eta_expand >>= trace,
+  constructor

tests/lean/eta_tac.lean.expected.out

@@ -0,0 +1,4 @@
+λ {A : Type} [_inst_1 : has_add A] (a a_1 : A), @add A _inst_1 a a_1
+λ (a : nat), nat.succ a
+λ (a_1 : nat), @add nat nat_has_add a a_1
+λ (x a : nat), @add nat nat_has_add x a