feat(library/tactic/apply_tactic): modify heuristic for adding arguments to apply tactic.

src/library/tactic/apply_tactic.cpp

@@ -70,11 +70,12 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
     expr  e_t        = e_t_cs.first;
     buffer<expr> metas;
     if (add_meta) {
-        unsigned num_t   = get_expect_num_args(*tc, t);
+        // unsigned num_t   = get_expect_num_args(*tc, t);
         unsigned num_e_t = get_expect_num_args(*tc, e_t);
-        if (num_t > num_e_t)
-            return proof_state_seq(); // no hope to unify then
-        for (unsigned i = 0; i < num_e_t - num_t; i++) {
+        // Remark: we used to add (num_e_t - num_t) arguments.
+        // This would allow us to handle (A -> B) without using intros,
+        // but it was preventing us from solving other problems
+        for (unsigned i = 0; i < num_e_t; i++) {
             auto e_t_cs = tc->whnf(e_t);
             e_t_cs.second.linearize(cs);
             e_t        = e_t_cs.first;

tests/lean/run/tactic10.lean

@@ -2,7 +2,9 @@ import logic
 
 theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
 := by rapply iff.intro;
-      apply (assume Ha, iff.elim_left H Ha);
-      apply (assume Hb, iff.elim_right H Hb)
+      intro Ha;
+        apply (iff.elim_left H Ha);
+      intro Hb;
+        apply (iff.elim_right H Hb)
 
 check tst

tests/lean/run/tactic11.lean

@@ -4,14 +4,18 @@ theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
 := have H1 [visible] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics
    from iff.elim_left H,
    by rapply iff.intro;
-      apply (assume Ha, H1 Ha);
-      apply (assume Hb, iff.elim_right H Hb)
+      intro Ha;
+        apply (H1 Ha);
+      intro Hb;
+        apply (iff.elim_right H Hb)
 
 theorem tst2 (a b : Prop) (H : a ↔ b) : b ↔ a
 := have H1 [visible] : a → b,
    from iff.elim_left H,
    begin
      rapply iff.intro,
-     apply (assume Ha, H1 Ha),
-     apply (assume Hb, iff.elim_right H Hb)
+     intro Ha;
+       apply (H1 Ha),
+     intro Hb;
+       apply (iff.elim_right H Hb)
    end

tests/lean/run/tactic12.lean

@@ -4,7 +4,6 @@ open tactic
 theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b
 := by apply and.intro;
       assumption;
-      apply not_intro;
       exact
         (assume Ha, or.elim H
           (assume Hna, @absurd _ false Ha Hna)

tests/lean/run/tactic13.lean

@@ -5,7 +5,6 @@ theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
 begin
   apply and.intro,
   assumption,
-  apply not_intro,
   assume Ha, or.elim H
     (assume Hna, @absurd _ false Ha Hna)
     (assume Hnb, @absurd _ false Hb Hnb)