From 062ebf43440606f82513e35c37730c8cf0373bb3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Nov 2017 11:21:17 -0800
Subject: [PATCH] fix(library/tactic/apply_tactic): when using elimator-like
 definitions

We found this problem when developing the red-black tree module.
---
 doc/changes.md                          |  4 +++
 src/library/tactic/apply_tactic.cpp     | 33 ++++++++++++++++++-------
 tests/lean/apply_elim.lean              | 12 +++++++++
 tests/lean/apply_elim.lean.expected.out |  6 +++++
 4 files changed, 46 insertions(+), 9 deletions(-)
 create mode 100644 tests/lean/apply_elim.lean
 create mode 100644 tests/lean/apply_elim.lean.expected.out

diff --git a/doc/changes.md b/doc/changes.md
index 8e5103b6e9..b7440d519f 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -35,6 +35,10 @@ master branch (aka work in progress branch)
 - Move `rb_map` and `rb_tree` to the `native` namespace. We will later add
   pure Lean implementations. Use `open native` to port files.
 
+- `apply t` behavior changed when type of `t` is of the form `forall (a_1 : A_1) ... (a_n : A_n), ?m ...`, where `?m` is an unassigned metavariable.
+  In this case, `apply t` behaves as `apply t _ ... _` where `n` `_` have been added, independently of the goal target type.
+  The new behavior is useful when using `apply` with eliminator-like definitions.
+
 *API name changes*
 
 v3.3.0 (14 September 2017)
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index 7baa8ae2b3..3f8ca8a801 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -31,13 +31,20 @@ apply_cfg::apply_cfg(vm_obj const & cfg):
     m_opt_param(to_bool(cfield(cfg, 5))) {
 }
 
-static unsigned get_expect_num_args(type_context & ctx, expr e) {
+/*
+  Compute the number of expected arguments and whether the result type is of the form
+  (?m ...) where ?m is an unassigned metavariable.
+*/
+static pair<unsigned, bool> get_expected_num_args_ho_result(type_context & ctx, expr e) {
     type_context::tmp_locals locals(ctx);
     unsigned r = 0;
     while (true) {
         e = ctx.relaxed_whnf(e);
-        if (!is_pi(e))
-            return r;
+        if (!is_pi(e)) {
+            expr fn = get_app_fn(e);
+            bool ho_result = is_metavar(fn) && !ctx.is_assigned(fn);
+            return mk_pair(r, ho_result);
+        }
         // TODO(Leo): try to avoid the following instantiate.
         expr local = locals.push_local(binding_name(e), binding_domain(e), binding_info(e));
         e = instantiate(binding_body(e), local);
@@ -45,6 +52,10 @@ static unsigned get_expect_num_args(type_context & ctx, expr e) {
     }
 }
 
+static unsigned get_expected_num_args(type_context & ctx, expr e) {
+    return get_expected_num_args_ho_result(ctx, e).first;
+}
+
 static bool try_instance(type_context & ctx, expr const & meta, tactic_state const & s, vm_obj * out_error_obj, char const * tac_name) {
     if (ctx.is_assigned(meta))
         return true;
@@ -161,12 +172,16 @@ static optional<tactic_state> apply(type_context & ctx, expr e, apply_cfg const
     local_context lctx   = g->get_context();
     expr target          = g->get_type();
     expr e_type          = ctx.infer(e);
-    unsigned num_e_t     = get_expect_num_args(ctx, e_type);
-    unsigned num_t       = get_expect_num_args(ctx, target);
-    if (num_t <= num_e_t)
-        num_e_t -= num_t;
-    else
-        num_e_t = 0;
+    unsigned num_e_t; bool ho_result;
+    std::tie(num_e_t, ho_result) = get_expected_num_args_ho_result(ctx, e_type);
+    if (!ho_result) {
+        /* Result type is not of the form `(?m ...)` */
+        unsigned num_t = get_expected_num_args(ctx, target);
+        if (num_t <= num_e_t)
+            num_e_t -= num_t;
+        else
+            num_e_t = 0;
+    }
     /* Generate meta-variables for arguments */
     buffer<expr> metas;
     buffer<bool> is_instance;
diff --git a/tests/lean/apply_elim.lean b/tests/lean/apply_elim.lean
new file mode 100644
index 0000000000..96269eb14d
--- /dev/null
+++ b/tests/lean/apply_elim.lean
@@ -0,0 +1,12 @@
+open nat
+
+def nat.ind_on {p : nat → Prop} (n : nat) (h₁ : p 0) (h₂ : ∀ n, p n → p (succ n)) : p n :=
+nat.rec_on n h₁ h₂
+
+example : ∀ a b : nat, a + b = b + a :=
+begin
+  intro a,
+  apply nat.ind_on a,
+  trace_state,
+  repeat {admit}
+end
diff --git a/tests/lean/apply_elim.lean.expected.out b/tests/lean/apply_elim.lean.expected.out
new file mode 100644
index 0000000000..f56bc1ad76
--- /dev/null
+++ b/tests/lean/apply_elim.lean.expected.out
@@ -0,0 +1,6 @@
+a : ℕ
+⊢ ∀ (b : ℕ), 0 + b = b + 0
+
+a : ℕ
+⊢ ∀ (n : ℕ), (∀ (b : ℕ), n + b = b + n) → ∀ (b : ℕ), succ n + b = b + succ n
+apply_elim.lean:6:0: warning: declaration '[anonymous]' uses sorry