feat(library/init/meta): add unify config option to apply_cfg

This commit also fixes a problem in the `apply` tactic error messages.

library/init/meta/interactive.lean

@@ -199,6 +199,13 @@ Similar to the `apply` tactic, but allows the user to provide a `apply_cfg` conf
 meta def apply_with (q : parse parser.pexpr) (cfg : apply_cfg) : tactic unit :=
 concat_tags (do e ← i_to_expr_for_apply q, tactic.apply e cfg)
 
+/--
+Similar to the `apply` tactic, but uses matching instead of unification.
+`apply_match t` is equivalent to `apply_with t {unify := ff}`
+-/
+meta def mapply (q : parse texpr) : tactic unit :=
+concat_tags (do e ← i_to_expr_for_apply q, tactic.apply e {unify := ff})
+
 /--
 This tactic tries to close the main goal `... ⊢ t` by generating a term of type `t` using type class resolution.
 -/

library/init/meta/tactic.lean

@@ -373,7 +373,17 @@ meta constant get_goals     : tactic (list expr)
 meta constant set_goals     : list expr → tactic unit
 inductive new_goals
 | non_dep_first | non_dep_only | all
-/-- Configuration options for the `apply` tactic. -/
+/-- Configuration options for the `apply` tactic.
+
+- `new_goals` is the strategy for ordering new goals.
+- `instances` if `tt`, then `apply` tries to synthesize unresolved `[...]` arguments using type class resolution.
+- `auto_param` if `tt`, then `apply` tries to synthesize unresolved `(h : p . tac_id)` arguments using tactic `tac_id`.
+- `opt_param` if `tt`, then `apply` tries to synthesize unresolved `(a : t := v)` arguments by setting them to `v`.
+- `unify` if `tt`, then `apply` is free to assign existing metavariables in the goal when solving unification constraints.
+   For example, in the goal `|- ?x < succ 0`, the tactic `apply succ_lt_succ` succeeds with the default configuration,
+   but `apply_with succ_lt_succ {unify := ff}` doesn't since it would require Lean to assign `?x` to `succ ?y` where
+   `?y` is a fresh metavariable.
+-/
 structure apply_cfg :=
 (md            := semireducible)
 (approx        := tt)
@@ -381,6 +391,7 @@ structure apply_cfg :=
 (instances     := tt)
 (auto_param    := tt)
 (opt_param     := tt)
+(unify         := tt)
 /-- Apply the expression `e` to the main goal,
     the unification is performed using the transparency mode in `cfg`.
     If `cfg.approx` is `tt`, then fallback to first-order unification, and approximate context during unification.

src/library/tactic/apply_tactic.cpp

@@ -29,7 +29,8 @@ apply_cfg::apply_cfg(vm_obj const & cfg):
     m_new_goals(to_new_goals_kind(cfield(cfg, 2))),
     m_instances(to_bool(cfield(cfg, 3))),
     m_auto_param(to_bool(cfield(cfg, 4))),
-    m_opt_param(to_bool(cfield(cfg, 5))) {
+    m_opt_param(to_bool(cfield(cfg, 5))),
+    m_unify(to_bool(cfield(cfg, 6))) {
 }
 
 /*
@@ -198,13 +199,21 @@ static optional<tactic_state> apply(type_context & ctx, expr e, apply_cfg const
     }
     /* Unify */
     lean_assert(metas.size() == is_instance.size());
-    if (!ctx.is_def_eq(e_type, target)) {
+
+    if ((cfg.m_unify && !ctx.unify(e_type, target)) ||
+        (!cfg.m_unify && !ctx.match(e_type, target))) {
         if (out_error_obj) {
             auto thunk = [=]() {
-                format msg = format("invalid apply tactic, failed to unify");
-                msg += pp_indented_expr(s, target);
+                auto pp_ctx = ::lean::mk_pp_ctx(ctx.env(), s.get_options(), ctx.mctx(), ctx.lctx());
+                format msg = format("invalid apply tactic, failed to ");
+                if (cfg.m_unify)
+                    msg += format("unify");
+                else
+                    msg += format("match");
+                unsigned i = get_pp_indent(s.get_options());
+                msg += nest(i, line() + pp_ctx(target));
                 msg += line() + format("with");
-                msg += pp_indented_expr(s, e_type);
+                msg += nest(i, line() + pp_ctx(e_type));
                 return msg;
             };
             *out_error_obj = tactic::mk_exception(thunk, s);

src/library/tactic/apply_tactic.h

@@ -20,6 +20,7 @@ structure apply_cfg :=
 (instances     := tt)
 (auto_param    := tt)
 (opt_param     := tt)
+(unify         := tt)
 */
 struct apply_cfg {
     transparency_mode m_mode{transparency_mode::Semireducible};
@@ -28,6 +29,7 @@ struct apply_cfg {
     bool              m_instances{true};
     bool              m_auto_param{true};
     bool              m_opt_param{true};
+    bool              m_unify{true};
     apply_cfg() {}
     apply_cfg(vm_obj const & cfg);
 };

src/library/tactic/tactic_state.cpp

@@ -513,11 +513,10 @@ vm_obj tactic_unify(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_o
 vm_obj tactic_is_def_eq(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_obj const & s0) {
     tactic_state const & s = tactic::to_state(s0);
     type_context ctx       = mk_type_context_for(s, to_transparency_mode(t));
-    type_context::tmp_mode_scope scope(ctx);
     try {
         check_closed("is_def_eq", to_expr(e1));
         check_closed("is_def_eq", to_expr(e2));
-        bool r = ctx.is_def_eq(to_expr(e1), to_expr(e2));
+        bool r = ctx.pure_is_def_eq(to_expr(e1), to_expr(e2));
         if (r) {
             return tactic::mk_success(s);
         } else {

tests/lean/interactive/goal_info_rw.lean.expected.out

@@ -1,6 +1,6 @@
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"doc":"An abbreviation for `rewrite`.","source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":3}
-{"record":{"doc":"An abbreviation for `rewrite`.","source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":5}
+{"record":{"doc":"An abbreviation for `rewrite`.","source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":3}
+{"record":{"doc":"An abbreviation for `rewrite`.","source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":5}
 {"record":{"full-id":"h₁","state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = q","type":"p = q"},"response":"ok","seq_num":7}
-{"record":{"doc":"An abbreviation for `rewrite`.","source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":8}
-{"record":{"doc":"An abbreviation for `rewrite`.","source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":10}
+{"record":{"doc":"An abbreviation for `rewrite`.","source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":8}
+{"record":{"doc":"An abbreviation for `rewrite`.","source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":10}

tests/lean/run/mapply.lean

@@ -0,0 +1,20 @@
+constant p : nat → Prop
+constant q : nat → Prop
+constant h : nat → Prop
+axiom pq0 : q 0 → p 0
+axiom phx : ∀ x, h x → p x
+
+example (h₁ : h 1) : ∃ x, p x :=
+begin
+  constructor,
+  mapply pq0 <|> mapply phx, -- The first `mapply` should fail
+  assumption
+end
+
+open nat
+example : ∃ x, succ 0 > x :=
+begin
+  constructor,
+  fail_if_success { mapply succ_lt_succ },
+  apply zero_lt_succ
+end