feat(library/tactic): change apply tactic semantics: goals are not reversed; and dependent arguments are not included

This commit also adds the tactic rapply that corresponds to the previous
semantics we have been using.

library/tools/tactic.lean

@@ -43,9 +43,10 @@ opaque definition beta        : tactic := builtin
 inductive expr : Type :=
 builtin : expr
 
-opaque definition apply  (e : expr) : tactic := builtin
+opaque definition apply   (e : expr) : tactic := builtin
-opaque definition rename (a b : expr) : tactic := builtin
+opaque definition rapply  (e : expr) : tactic := builtin
-opaque definition intro (e : expr) : tactic := builtin
+opaque definition rename  (a b : expr) : tactic := builtin
+opaque definition intro   (e : expr) : tactic := builtin
 
 inductive expr_list : Type :=
 nil  : expr_list,

src/emacs/lean-syntax.el

@@ -118,7 +118,7 @@
      (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
      ;; tactics
      (,(rx (not (any "\.")) word-start
-           (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "rename" "intro" "intros"
+           (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "rapply" "apply" "rename" "intro" "intros"
                "back" "beta" "done" "exact" "repeat")
            word-end)
       . 'font-lock-constant-face)

src/library/tactic/apply_tactic.cpp

@@ -23,9 +23,39 @@ Author: Leonardo de Moura
 #include "library/tactic/expr_to_tactic.h"
 
 namespace lean {
+/**
+    \brief Given a sequence metas: <tt>(?m_1 ...) (?m_2 ... ) ... (?m_k ...)</tt>,
+    we say ?m_i is "redundant" if it occurs in the type of some ?m_j.
+    This procedure removes from metas any redundant element.
+*/
+static void remove_redundant_metas(buffer<expr> & metas) {
+    buffer<expr> mvars;
+    for (expr const & m : metas)
+        mvars.push_back(get_app_fn(m));
+    unsigned k = 0;
+    for (unsigned i = 0; i < metas.size(); i++) {
+        bool found = false;
+        for (unsigned j = 0; j < metas.size(); j++) {
+            if (j != i) {
+                if (occurs(mvars[i], mlocal_type(mvars[j]))) {
+                    found = true;
+                    break;
+                }
+            }
+        }
+        if (!found) {
+            metas[k] = metas[i];
+            k++;
+        }
+    }
+    metas.shrink(k);
+}
+
+enum subgoals_action_kind { IgnoreSubgoals, AddRevSubgoals, AddSubgoals };
+
 static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s,
                                          expr const & _e, buffer<constraint> & cs,
-                                         bool add_meta, bool add_subgoals, bool relax_main_opaque) {
+                                         bool add_meta, subgoals_action_kind subgoals_action, bool relax_main_opaque) {
     goals const & gs = s.get_goals();
     if (empty(gs))
         return proof_state_seq();
@@ -73,23 +103,33 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
             check_has_no_local(new_p, _e, "apply");
             new_subst.assign(g.get_name(), new_p);
             goals new_gs = tail_gs;
-            if (add_subgoals) {
+            if (subgoals_action != IgnoreSubgoals) {
                 buffer<expr> metas;
                 for (auto m : meta_lst) {
                     if (!new_subst.is_assigned(get_app_fn(m)))
                         metas.push_back(m);
                 }
-                for (unsigned i = 0; i < metas.size(); i++)
+                if (subgoals_action == AddRevSubgoals) {
-                    new_gs = cons(goal(metas[i], new_subst.instantiate_all(tc->infer(metas[i]).first)), new_gs);
+                    for (unsigned i = 0; i < metas.size(); i++)
+                        new_gs = cons(goal(metas[i], new_subst.instantiate_all(tc->infer(metas[i]).first)), new_gs);
+                } else {
+                    lean_assert(subgoals_action == AddSubgoals);
+                    remove_redundant_metas(metas);
+                    unsigned i = metas.size();
+                    while (i > 0) {
+                        --i;
+                        new_gs = cons(goal(metas[i], new_subst.instantiate_all(tc->infer(metas[i]).first)), new_gs);
+                    }
+                }
             }
             return proof_state(new_gs, new_subst, new_ngen, postponed);
         });
 }
 
 static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e,
-                                         bool add_meta, bool add_subgoals, bool relax_main_opaque) {
+                                         bool add_meta, subgoals_action_kind subgoals_action, bool relax_main_opaque) {
     buffer<constraint> cs;
-    return apply_tactic_core(env, ios, s, e, cs, add_meta, add_subgoals, relax_main_opaque);
+    return apply_tactic_core(env, ios, s, e, cs, add_meta, subgoals_action, relax_main_opaque);
 }
 
 tactic eassumption_tactic(bool relax_main_opaque) {
@@ -102,13 +142,13 @@ tactic eassumption_tactic(bool relax_main_opaque) {
             buffer<expr> hs;
             get_app_args(g.get_meta(), hs);
             for (expr const & h : hs) {
-                r = append(r, apply_tactic_core(env, ios, s, h, false, false, relax_main_opaque));
+                r = append(r, apply_tactic_core(env, ios, s, h, false, IgnoreSubgoals, relax_main_opaque));
             }
             return r;
         });
 }
 
-tactic apply_tactic(elaborate_fn const & elab, expr const & e, bool relax_main_opaque) {
+tactic apply_tactic(elaborate_fn const & elab, expr const & e, bool rev, bool relax_main_opaque) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();
             if (empty(gs))
@@ -122,7 +162,7 @@ tactic apply_tactic(elaborate_fn const & elab, expr const & e, bool relax_main_o
             to_buffer(ecs.second, cs);
             to_buffer(s.get_postponed(), cs);
             proof_state new_s(s.get_goals(), s.get_subst(), ngen, constraints());
-            return apply_tactic_core(env, ios, new_s, new_e, cs, true, true, relax_main_opaque);
+            return apply_tactic_core(env, ios, new_s, new_e, cs, true, rev ? AddRevSubgoals : AddSubgoals, relax_main_opaque);
         });
 }
 
@@ -135,7 +175,13 @@ void initialize_apply_tactic() {
     register_tac(name({"tactic", "apply"}),
                  [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      check_tactic_expr(app_arg(e), "invalid 'apply' tactic, invalid argument");
-                     return apply_tactic(fn, get_tactic_expr_expr(app_arg(e)));
+                     return apply_tactic(fn, get_tactic_expr_expr(app_arg(e)), false);
+                 });
+
+    register_tac(name({"tactic", "rapply"}),
+                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                     check_tactic_expr(app_arg(e), "invalid 'apply' tactic, invalid argument");
+                     return apply_tactic(fn, get_tactic_expr_expr(app_arg(e)), true);
                  });
 
     register_simple_tac(name({"tactic", "eassumption"}),

src/library/tactic/apply_tactic.h

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "util/lua.h"
 #include "library/tactic/tactic.h"
 namespace lean {
-tactic apply_tactic(elaborate_fn const & fn, expr const & e, bool relax_main_opaque = true);
+tactic apply_tactic(elaborate_fn const & fn, expr const & e, bool rev_goals = false, bool relax_main_opaque = true);
 tactic eassumption_tactic(bool relax_main_opaque = true);
 void open_apply_tactic(lua_State * L);
 void initialize_apply_tactic();

tests/lean/goals1.lean

@@ -5,5 +5,5 @@ set_option pp.notation false
 theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
 begin
   apply eq.trans,
-  apply Hbc
+  apply Hab
 end

tests/lean/goals1.lean.expected.out

@@ -1,5 +1,5 @@
 goals1.lean:9:0: error: unsolved placeholder, unsolved subgoals
-A : Type, a : A, b : A, c : A, Hab : eq a b, Hbc : eq b c ⊢ eq a b
+A : Type, a : A, b : A, c : A, Hab : eq a b, Hbc : eq b c ⊢ eq b c
 goals1.lean:9:0: error: failed to add declaration 'foo' to environment, value has metavariables
   λ (A : Type) (a b c : A) (Hab : eq a b) (Hbc : eq b c),
     ?M_1

tests/lean/have1.lean

@@ -6,7 +6,7 @@ axiom H1 : a = b
 axiom H2 : b = c
 
 check have e1 [visible] : a = b, from H1,
-      have e2 : a = c, by apply trans; apply H2; apply e1,
+      have e2 : a = c, by apply trans; apply e1; apply H2,
       have e3 : c = a, from e2⁻¹,
       have e4 [visible] : b = a, from e1⁻¹,
       have e5 : b = c, from e4 ⬝ e2,

tests/lean/run/beginend.lean

@@ -4,6 +4,6 @@ open tactic
 theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
 begin
   apply eq.trans,
+  apply Hab,
   apply Hbc,
-  apply Hab
 end

tests/lean/run/intros.lean

@@ -5,21 +5,21 @@ theorem tst1 (a b : Prop) : a → b → b :=
 by intro Ha; intro Hb; apply Hb
 
 theorem tst2 (a b : Prop) : a → b → a ∧ b :=
-by intro Ha; intro Hb; apply and.intro; apply Hb; apply Ha
+by intro Ha; intro Hb; rapply and.intro; apply Hb; apply Ha
 
 theorem tst3 (a b : Prop) : a → b → a ∧ b :=
 begin
  intro Ha,
  intro Hb,
  apply and.intro,
+ apply Ha,
  apply Hb,
- apply Ha
 end
 
 theorem tst4 (a b : Prop) : a → b → a ∧ b :=
 begin
   intros (Ha, Hb),
-  apply and.intro,
+  rapply and.intro,
   apply Hb,
   apply Ha
 end

tests/lean/run/rename_tac.lean

@@ -4,7 +4,7 @@ open tactic
 theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
 begin
   apply eq.trans,
-  apply Hbc,
   rename Hab Foo,
-  apply Foo
+  apply Foo,
+  apply Hbc,
 end

tests/lean/run/tactic10.lean

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

tests/lean/run/tactic11.lean

@@ -4,7 +4,7 @@ open tactic
 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 apply iff.intro;
+   by rapply iff.intro;
       apply (assume Ha, H1 Ha);
       apply (assume Hb, iff.elim_right H Hb)
 
@@ -12,7 +12,7 @@ theorem tst2 (a b : Prop) (H : a ↔ b) : b ↔ a
 := have H1 [visible] : a → b,
    from iff.elim_left H,
    begin
-     apply iff.intro,
+     rapply iff.intro,
      apply (assume Ha, H1 Ha),
      apply (assume Hb, iff.elim_right H Hb)
    end

tests/lean/run/tactic29.lean

@@ -12,7 +12,7 @@ section
   check H
   check H2
   theorem test : a = b ∧ a = a
-  := by apply and.intro; apply eq.refl; apply H
+  := by apply and.intro; apply H; apply eq.refl
 end
 
 check @test

tests/lean/run/tactic8.lean

@@ -3,7 +3,7 @@ open tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A :=
 by apply @and.intro;
-   apply (show B ∧ A, from and.intro H2 H1);
+   apply (show A, from H1);
-   apply (show A, from H1)
+   apply (show B ∧ A, from and.intro H2 H1)
 
 check @tst

tests/lean/show1.lean

@@ -8,7 +8,7 @@ axiom H2 : b = c
 check show a = c, from H1 ⬝ H2
 print "------------"
 check have e1 [visible] : a = b, from H1,
-      have e2 : a = c, by apply eq.trans; apply H2; apply e1,
+      have e2 : a = c, by apply eq.trans; apply e1; apply H2,
       have e3 : c = a, from e2⁻¹,
       have e4 [visible] : b = a, from e1⁻¹,
       show b = c, from e1⁻¹ ⬝ e2