feat(tactic/solve_by_elim): add accept parameter to prune tree search (…

…#2245)

* chore(tactic/solve_by_elim): cleanup

* cleanup

* what happened to my commit?

* fix

* fix

* fixed?

* Tweak comments

* feat(tactic/solve_by_elim): add accept parameter to prune tree search

* when called with empty lemmas, use the same default set as the interactive tactic

* stop cheating with [] ~ none

* indenting

* various

* various

* docstring

* fix docstrings

* more docs

* docs

* fix doc-strings

* improve documentation of accept, and add doc-string

* improve docs

* try again with documentation

* clarify when accept runs

* Update src/tactic/solve_by_elim.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* Update src/tactic/solve_by_elim.lean

* Update src/tactic/solve_by_elim.lean

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/meta/expr.lean

@@ -307,6 +307,15 @@ e.fold mk_name_set (λ e' _ es, if e'.is_constant then es.insert e'.const_name e
 meta def list_meta_vars (e : expr) : list expr :=
 e.fold [] (λ e' _ es, if e'.is_mvar then insert e' es else es)
 
+/--
+Test `t` contains the specified subexpression `e`, or a metavariable.
+This represents the notion that `e` "may occur" in `t`,
+possibly after subsequent unification.
+-/
+meta def contains_expr_or_mvar (t : expr) (e : expr) : bool :=
+-- We can't use `t.has_meta_var` here, as that detects universe metavariables, too.
+¬ t.list_meta_vars.empty ∨ e.occurs t
+
 /-- Returns a name_set of all constants in an expression starting with a certain prefix. -/
 meta def list_names_with_prefix (pre : name) (e : expr) : name_set :=
 e.fold mk_name_set $ λ e' _ l,

src/tactic/core.lean

@@ -688,24 +688,45 @@ let ap e := tactic.apply e {new_goals := new_goals.non_dep_only} in
 ap e <|> (iff_mp e >>= ap) <|> (iff_mpr e >>= ap)
 
 /--
-`apply_any` tries to apply one of a list of lemmas to the current goal.
+Configuration options for `apply_any`:
+* `use_symmetry`: if `apply_any` fails to apply any lemma, call `symmetry` and try again.
+* `use_exfalso`: if `apply_any` fails to apply any lemma, call `exfalso` and try again.
+* `all_goals`: attempt to solve all goals simultaneously,
+    backtracking if a solution to one goal results in other goals being impossible.
+* `apply`: specify an alternative to `tactic.apply`; usually `apply := tactic.eapply`.
+-/
+meta structure apply_any_opt :=
+(use_symmetry : bool := tt)
+(use_exfalso : bool := tt)
+(all_goals : bool := tt)
+(apply : expr → tactic (list (name × expr)) := tactic.apply)
 
-Optional arguments:
-* `lemmas` controls which expressions are applied.
-* `tac` is called after a successful application. Defaults to `skip`.
-* `use_symmetry`: if no lemma applies, call `symmetry` and try again.
-* `use_exfalso`: if no lemma applies, call `exfalso` and try again.
+/--
+`apply_any lemmas` tries to apply one of the list `lemmas` to the current goal.
+
+`apply_any lemmas opt` allows control over how lemmas are applied.
+`opt` has fields:
+* `use_symmetry`: if no lemma applies, call `symmetry` and try again. (Defaults to `tt`.)
+* `use_exfalso`: if no lemma applies, call `exfalso` and try again. (Defaults to `tt`.)
+* `all_goals`: attempt to apply the lemmas to each of the goals sequentially. (Defaults to `tt`.)
+* `apply`: use a tactic other than `tactic.apply` (e.g. `tactic.fapply` or `tactic.eapply`).
+
+`apply_any lemmas tac` calls the tactic `tac` after a successful application.
+Defaults to `skip`. This is used, for example, by `solve_by_elim` to arrange
+recursive invocations of `apply_any`.
 -/
 meta def apply_any
   (lemmas : list expr)
-  (tac : tactic unit := skip)
-  (use_symmetry : bool := tt)
-  (use_exfalso : bool := tt) : tactic unit :=
+  (opt : apply_any_opt := {})
+  (tac : tactic unit := skip) : tactic unit :=
 do
   let modes := [skip]
-    ++ (if use_symmetry then [symmetry] else [])
-    ++ (if use_exfalso then [exfalso] else []),
-  modes.any_of (λ m, do m, lemmas.any_of (λ H, apply H >> tac)) <|>
+    ++ (if opt.use_symmetry then [symmetry] else [])
+    ++ (if opt.use_exfalso then [exfalso] else []),
+  goals ← if opt.all_goals then list.range <$> num_goals else pure [0],
+  goals.any_of (λ g, do rotate g,
+    modes.any_of (λ m, do m,
+      lemmas.any_of (λ H, opt.apply H >> tac))) <|>
   fail "apply_any tactic failed; no lemma could be applied"
 
 /-- Try to apply a hypothesis from the local context to the goal. -/

src/tactic/solve_by_elim.lean

@@ -5,8 +5,26 @@ Authors: Simon Hudon, Scott Morrison
 -/
 import tactic.core
 
+/-!
+# solve_by_elim
+
+A depth-first search backwards reasoner.
+
+`solve_by_elim` takes a list of lemmas, and repeating tries to `apply` these against
+the goals, recursively acting on any generated subgoals.
+
+It accepts a variety of configuration options described below, enabling
+* backtracking across multiple goals,
+* pruning the search tree, and
+* invoking other tactics before or after trying to apply lemmas.
+
+At present it has no "premise selection", and simply tries the supplied lemmas in order
+at each step of the search.
+-/
+
 namespace tactic
 
+namespace solve_by_elim
 /--
 Builds a collection of lemmas for use in the backtracking search in `solve_by_elim`.
 
@@ -39,42 +57,77 @@ do (hs, gex, hex, all_hyps) ← decode_simp_arg_list hs,
    else return hs
 
 /--
-The internal implementation of `solve_by_elim`, with a limiting counter.
+Configuration options for `solve_by_elim`.
+
+* `accept : list expr → tactic unit` determines whether the current branch should be explored.
+   At each step, before the lemmas are applied,
+   `accept` is passed the proof terms for the original goals,
+   as reported by `get_goals` when `solve_by_elim` started.
+   These proof terms may be metavariables (if no progress has been made on that goal)
+   or may contain metavariables at some leaf nodes 
+   (if the goal has been partially solved by previous `apply` steps).
+   If the `accept` tactic fails `solve_by_elim` aborts searching this branch and backtracks.
+   By default `accept := λ _, skip` always succeeds.
+   (There is an example usage in `tests/solve_by_elim.lean`.)
+* `pre_apply : tactic unit` specifies an additional tactic to run before each round of `apply`.
+* `discharger : tactic unit` specifies an additional tactic to apply on subgoals
+  for which no lemma applies.
+  If that tactic succeeds, `solve_by_elim` will continue applying lemmas on resulting goals.
 -/
-meta def solve_by_elim_aux (discharger : tactic unit) (lemmas : list expr)  : ℕ → tactic unit
-| 0 := done
-| (n+1) := done <|>
-    (apply_any lemmas $ solve_by_elim_aux n) <|>
-    (discharger >> solve_by_elim_aux n)
+meta structure basic_opt extends apply_any_opt :=
+(accept : list expr → tactic unit := λ _, skip)
+(pre_apply : tactic unit := skip)
+(discharger : tactic unit := failed)
 
 /--
-Configuration options for `solve_by_elim`.
+The internal implementation of `solve_by_elim`, with a limiting counter.
+-/
+meta def solve_by_elim_aux (opt : basic_opt)
+  (original_goals : list expr) (lemmas : list expr) : ℕ → tactic unit
+| n := do
+  -- First, check that progress so far is `accept`able.
+  lock_tactic_state (original_goals.mmap instantiate_mvars >>= opt.accept) >>
+  -- Then check if we've finished.
+  (done <|>
+    -- Otherwise, if there's more time left,
+    guard (n > 0) >>
+    -- run the `pre_apply` tactic, then
+    opt.pre_apply >>
+    -- try either applying a lemma and recursing, or
+    ((apply_any lemmas opt.to_apply_any_opt $ solve_by_elim_aux (n-1)) <|>
+    -- if that doesn't work, run the discharger and recurse.
+     (opt.discharger >> solve_by_elim_aux (n-1))))
 
+/--
+Arguments for `solve_by_elim`:
 * By default `solve_by_elim` operates only on the first goal,
   but with `backtrack_all_goals := true`, it operates on all goals at once,
   backtracking across goals as needed,
   and only succeeds if it discharges all goals.
-* `discharger` specifies an additional tactic to apply on subgoals for which no lemma applies.
-  If that tactic succeeds, `solve_by_elim` will continue applying lemmas on resulting goals.
-* `assumptions` generates the list of lemmas to use in the backtracking search.
+* `lemmas` specifies the list of lemmas to use in the backtracking search.
+  If `none`, `solve_by_elim` uses the local hypotheses,
+  along with `rfl`, `trivial`, `congr_arg`, and `congr_fun`.
 * `max_steps` bounds the depth of the search.
 -/
-meta structure by_elim_opt :=
+meta structure opt extends basic_opt :=
 (backtrack_all_goals : bool := ff)
-(discharger : tactic unit := done)
 (lemmas : option (list expr) := none)
 (max_steps : ℕ := 3)
 
 /--
 If no lemmas have been specified, generate the default set
 (local hypotheses, along with `rfl`, `trivial`, `congr_arg`, and `congr_fun`).
 -/
-meta def by_elim_opt.get_lemmas (opt : by_elim_opt) : tactic (list expr) :=
+meta def opt.get_lemmas (opt : opt) : tactic (list expr) :=
 match opt.lemmas with
 | none := mk_assumption_set ff [] []
 | some lemmas := return lemmas
 end
 
+end solve_by_elim
+
+open solve_by_elim
+
 /--
 `solve_by_elim` repeatedly tries `apply`ing a lemma
 from the list of assumptions (passed via the `by_elim_opt` argument),
@@ -87,12 +140,13 @@ If passed an empty list of assumptions, `solve_by_elim` builds a default set
 as per the interactive tactic, using the `local_context` along with
 `rfl`, `trivial`, `congr_arg`, and `congr_fun`.
 -/
-meta def solve_by_elim (opt : by_elim_opt := { }) : tactic unit :=
+meta def solve_by_elim (opt : opt := { }) : tactic unit :=
 do
   tactic.fail_if_no_goals,
   lemmas ← opt.get_lemmas,
-  (if opt.backtrack_all_goals then id else focus1) $
-    solve_by_elim_aux opt.discharger lemmas opt.max_steps
+  (if opt.backtrack_all_goals then id else focus1) $ (do
+    gs ← get_goals,
+    solve_by_elim_aux opt.to_basic_opt gs lemmas opt.max_steps)
 
 open interactive lean.parser interactive.types
 local postfix `?`:9001 := optional
@@ -116,13 +170,14 @@ Optional arguments:
 -/
 meta def apply_assumption
   (lemmas : option (list expr) := none)
+  (opt : apply_any_opt := {})
   (tac : tactic unit := skip) : tactic unit :=
 do
   lemmas ← match lemmas with
   | none := local_context
   | some lemmas := return lemmas
   end,
-  tactic.apply_any lemmas tac
+  tactic.apply_any lemmas opt tac
 
 add_tactic_doc
 { name        := "apply_assumption",
@@ -152,17 +207,27 @@ The assumptions can be modified with similar syntax as for `simp`:
 `solve_by_elim*` tries to solve all goals together, using backtracking if a solution for one goal
 makes other goals impossible.
 
-optional arguments passed via a configuration argument:
-- discharger: a subsidiary tactic to try at each step when no lemmas apply (e.g. `cc` may be helpful)
+optional arguments passed via a configuration argument as `solve_by_elim { ... }`
 - max_steps: number of attempts at discharging generated sub-goals
+- discharger: a subsidiary tactic to try at each step when no lemmas apply (e.g. `cc` may be helpful).
+- pre_apply: a subsidiary tactic to run at each step before applying lemmas (e.g. `intros`).
+- accept: a subsidiary tactic `list expr → tactic unit` that at each step,
+    before any lemmas are applied, is passed the original proof terms
+    as reported by `get_goals` when `solve_by_elim` started
+    (but which may by now have been partially solved by previous `apply` steps).
+    If the `accept` tactic fails,
+    `solve_by_elim` will abort searching the current branch and backtrack.
+    This may be used to filter results, either at every step of the search,
+    or filtering complete results
+    (by testing for the absence of metavariables, and then the filtering condition).
 -/
 meta def solve_by_elim (all_goals : parse $ (tk "*")?) (no_dflt : parse only_flag)
-  (hs : parse simp_arg_list) (attr_names : parse with_ident_list) (opt : by_elim_opt := { }) :
+  (hs : parse simp_arg_list) (attr_names : parse with_ident_list) (opt : solve_by_elim.opt := { }) :
   tactic unit :=
 do lemmas ← mk_assumption_set no_dflt hs attr_names,
    tactic.solve_by_elim
    { backtrack_all_goals := all_goals.is_some ∨ opt.backtrack_all_goals,
-     lemmas := lemmas,
+     lemmas := some lemmas,
      ..opt }
 
 add_tactic_doc

test/solve_by_elim.lean

@@ -108,3 +108,34 @@ begin
   apply le_trans,
   solve_by_elim { backtrack_all_goals := true },
 end
+
+/-
+We now test the `accept` feature of `solve_by_elim`.
+
+Recall that the `accept` parameter has type `list expr → tactic unit`.
+At each branch (not just leaf) of the backtracking search tree,
+`accept` is invoked with the list of metavariables
+reported by `get_goals` when `solve_by_elim` was called
+(which by now may have been partially solved by previous `apply` steps),
+and if it fails this branch of the search is ignored.
+
+Non-leaf nodes of the search tree will contain metavariables,
+so we can test using `expr.has_mvar` when we're only interesting in
+filtering complete solutions.
+
+In this example, we only accept solutions that contain
+a given subexpression.
+-/
+def solve_by_elim_use_b (a b : ℕ) : ℕ × ℕ × ℕ :=
+begin
+  split; [skip, split],
+  (do
+    b ← get_local `b,
+    tactic.solve_by_elim
+    { backtrack_all_goals := tt,
+      -- We require that in some goal, the expression `b` is used.
+      accept := (λ gs, gs.any_of (λ g, guard $ g.contains_expr_or_mvar b)) })
+end
+
+-- We verify that the solution did use `b`.
+example : solve_by_elim_use_b 1 2 = (1, 1, 2) := rfl