From 040722c7e7ca26fcd18eea5b0002f7336e40e92e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Jan 2018 12:48:59 -0800 Subject: [PATCH] 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 | 7 +++++++ library/init/meta/tactic.lean | 13 +++++++++++- src/library/tactic/apply_tactic.cpp | 19 +++++++++++++----- src/library/tactic/apply_tactic.h | 2 ++ src/library/tactic/tactic_state.cpp | 3 +-- .../goal_info_rw.lean.expected.out | 8 ++++---- tests/lean/run/mapply.lean | 20 +++++++++++++++++++ 7 files changed, 60 insertions(+), 12 deletions(-) create mode 100644 tests/lean/run/mapply.lean diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 8458ee4090..93fdca801d 100644 --- a/library/init/meta/interactive.lean +++ b/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. -/ diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 4cc3291318..07cfc3bc7f 100644 --- a/library/init/meta/tactic.lean +++ b/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. diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index d226c888c2..e172f0f28e 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/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 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); diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h index 3850b2c131..ebbc8b92bc 100644 --- a/src/library/tactic/apply_tactic.h +++ b/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); }; diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 5af8f871e1..a290497f4e 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/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 { diff --git a/tests/lean/interactive/goal_info_rw.lean.expected.out b/tests/lean/interactive/goal_info_rw.lean.expected.out index b900c1c0a0..1eff8b4cae 100644 --- a/tests/lean/interactive/goal_info_rw.lean.expected.out +++ b/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} diff --git a/tests/lean/run/mapply.lean b/tests/lean/run/mapply.lean new file mode 100644 index 0000000000..5987a1b3dc --- /dev/null +++ b/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