fix(solve_by_elim): handle multiple goals with different hypotheses (#…

…4519)

Previously `solve_by_elim*` would operate on multiple goals (only succeeding if it could close all of them, and performing backtracking across goals), however it would incorrectly only use the local context from the main goal. If other goals had different sets of hypotheses, ... various bad things could happen!

This PR arranges so that `solve_by_elim*` inspects the local context later, so it picks up the correct hypotheses.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/tactic/equiv_rw.lean

@@ -132,6 +132,7 @@ do
   { use_symmetry := false,
     use_exfalso := false,
     lemma_thunks := some (pure eq :: equiv_congr_lemmas),
+    ctx_thunk := pure [],
     max_depth := cfg.max_depth,
     -- Subgoals may contain function types,
     -- and we want to continue trying to construct equivalences after the binders.

src/tactic/solve_by_elim.lean

@@ -26,7 +26,8 @@ namespace tactic
 
 namespace solve_by_elim
 /--
-`mk_assumption_set` builds a collection of lemmas for use in the backtracking search in `solve_by_elim`.
+`mk_assumption_set` builds a collection of lemmas for use in
+the backtracking search in `solve_by_elim`.
 
 * By default, it includes all local hypotheses, along with `rfl`, `trivial`, `congr_fun` and
   `congr_arg`.
@@ -35,10 +36,22 @@ namespace solve_by_elim
   and can be used to add, or remove, lemmas or expressions from the set.
 * The argument `attr : list name` adds all lemmas tagged with one of a specified list of attributes.
 
-`mk_assumption_set` returns not a `list expr`, but a `list (tactic expr)`.
-The problem here is that we may generate lemmas that have as yet unspecified implicit arguments,
-and these implicit arguments would be filled in by metavariables if we created the actual `expr`
-objects now.
+`mk_assumption_set` returns not a `list expr`, but a `list (tactic expr) × tactic (list expr)`.
+There are two separate problems that need to be solved.
+
+### Relevant local hypotheses
+
+`solve_by_elim*` works with multiple goals,
+and we need to use separate sets of local hypotheses for each goal.
+The second component of the returned value provides these local hypotheses.
+(Essentially using `local_context`, along with some filtering to remove hypotheses
+that have been explicitly removed via `only` or `[-h]`.)
+
+### Stuck metavariables
+
+Lemmas with implicit arguments would be filled in with metavariables if we created the
+`expr` objects immediately, so instead we return thunks that generate the expressions
+on demand. This is the first component, with type `list (tactic expr)`.
 
 As an example, we have `def rfl : ∀ {α : Sort u} {a : α}, a = a`, which on elaboration will become
 `@rfl ?m_1 ?m_2`.
@@ -55,7 +68,7 @@ As an optimisation, after we build the list of `tactic expr`s, we actually run t
 that do not in fact produce metavariables with a simple `return` tactic.
 -/
 meta def mk_assumption_set (no_dflt : bool) (hs : list simp_arg_type) (attr : list name) :
-  tactic (list (tactic expr)) :=
+  tactic (list (tactic expr) × tactic (list expr)) :=
 -- We lock the tactic state so that any spurious goals generated during
 -- elaboration of pre-expressions are discarded
 lock_tactic_state $
@@ -76,14 +89,15 @@ do
   hs ← (hs ++ m).mfilter $ λ h, (do h ← h, return $ expr.const_name h ∉ gex),
   let hs := if no_dflt then hs else
     ([`rfl, `trivial, `congr_fun, `congr_arg].map (λ n, (mk_const n))) ++ hs,
-  hs ← if ¬ no_dflt ∨ all_hyps then do
+  let locals : tactic (list expr) := if ¬ no_dflt ∨ all_hyps then do
     ctx ← local_context,
     -- Remove local exceptions specified in `hex`:
-    return $ hs.append ((ctx.filter (λ h : expr, h.local_uniq_name ∉ hex)).map return)
-  else return hs,
+    return $ ctx.filter (λ h : expr, h.local_uniq_name ∉ hex)
+  else return [],
   -- Finally, run all of the tactics: any that return an expression without metavariables can safely
   -- be replaced by a `return` tactic.
-  hs.mmap (λ h, do e ← h, if e.has_meta_var then return h else return (return e))
+  hs ← hs.mmap (λ h : tactic expr, do e ← h, if e.has_meta_var then return h else return (return e)),
+  return (hs, locals)
 
 /--
 Configuration options for `solve_by_elim`.
@@ -144,7 +158,7 @@ else
 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 (tactic expr)) : ℕ → tactic unit
+  (original_goals : list expr) (lemmas : list (tactic expr)) (ctx : tactic (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),
@@ -157,7 +171,8 @@ meta def solve_by_elim_aux (opt : basic_opt)
     opt.pre_apply,
     -- try either applying a lemma and recursing,
     (on_success, on_failure) ← trace_hooks (opt.max_depth - n),
-    (apply_any_thunk lemmas opt.to_apply_any_opt (solve_by_elim_aux (n-1))
+    ctx_lemmas ← ctx,
+    (apply_any_thunk (lemmas ++ (ctx_lemmas.map return)) opt.to_apply_any_opt (solve_by_elim_aux (n-1))
       on_success on_failure) <|>
     -- or if that doesn't work, run the discharger and recurse.
      (opt.discharger >> solve_by_elim_aux (n-1)))
@@ -173,22 +188,25 @@ Arguments for `solve_by_elim`:
   along with `rfl`, `trivial`, `congr_arg`, and `congr_fun`.
 * `lemma_thunks` provides the lemmas as a list of `tactic expr`,
   which are used to regenerate the `expr` objects to avoid binding metavariables.
+  It should not usually be specified by the user.
   (If both `lemmas` and `lemma_thunks` are specified, only `lemma_thunks` is used.)
+* `ctx_thunk` is for internal use only: it returns the local hypotheses which will be used.
 * `max_depth` bounds the depth of the search.
 -/
 meta structure opt extends basic_opt :=
 (backtrack_all_goals : bool := ff)
 (lemmas : option (list expr) := none)
 (lemma_thunks : option (list (tactic expr)) := lemmas.map (λ l, l.map return))
+(ctx_thunk : tactic (list expr) := local_context)
 
 /--
 If no lemmas have been specified, generate the default set
 (local hypotheses, along with `rfl`, `trivial`, `congr_arg`, and `congr_fun`).
 -/
-meta def opt.get_lemma_thunks (opt : opt) : tactic (list (tactic expr)) :=
+meta def opt.get_lemma_thunks (opt : opt) : tactic (list (tactic expr) × tactic (list expr)) :=
 match opt.lemma_thunks with
 | none := mk_assumption_set ff [] []
-| some lemma_thunks := return lemma_thunks
+| some lemma_thunks := return (lemma_thunks, opt.ctx_thunk)
 end
 
 end solve_by_elim
@@ -223,10 +241,10 @@ See also the simpler tactic `apply_rules`, which does not perform backtracking.
 meta def solve_by_elim (opt : opt := { }) : tactic unit :=
 do
   tactic.fail_if_no_goals,
-  lemmas ← opt.get_lemma_thunks,
+  (lemmas, ctx_lemmas) ← opt.get_lemma_thunks,
   (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_depth <|>
+    solve_by_elim_aux opt.to_basic_opt gs lemmas ctx_lemmas opt.max_depth <|>
     fail ("`solve_by_elim` failed.\n" ++
       "Try `solve_by_elim { max_depth := N }` for `N > " ++ (to_string opt.max_depth) ++ "`\n" ++
       "or use `set_option trace.solve_by_elim true` to view the search."))
@@ -292,7 +310,8 @@ makes other goals impossible.
 
 optional arguments passed via a configuration argument as `solve_by_elim { ... }`
 - max_depth: 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).
+- 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
@@ -307,10 +326,11 @@ optional arguments passed via a configuration argument as `solve_by_elim { ... }
 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 : solve_by_elim.opt := { }) :
   tactic unit :=
-do lemma_thunks ← mk_assumption_set no_dflt hs attr_names,
+do (lemma_thunks, ctx_thunk) ← mk_assumption_set no_dflt hs attr_names,
    tactic.solve_by_elim
    { backtrack_all_goals := all_goals.is_some ∨ opt.backtrack_all_goals,
      lemma_thunks := some lemma_thunks,
+     ctx_thunk := ctx_thunk,
      ..opt }
 
 add_tactic_doc

src/tactic/suggest.lean

@@ -366,9 +366,9 @@ You can also use `suggest with attr` to include all lemmas with the attribute `a
 meta def suggest (n : parse (with_desc "n" small_nat)?)
   (hs : parse simp_arg_list) (attr_names : parse with_ident_list) (opt : opt := { }) :
   tactic unit :=
-do asms ← mk_assumption_set ff hs attr_names,
+do (lemma_thunks, ctx_thunk) ← mk_assumption_set ff hs attr_names,
    L ← tactic.suggest_scripts (n.get_or_else 50)
-     { lemma_thunks := return asms, ..opt },
+     { lemma_thunks := some lemma_thunks, ctx_thunk := ctx_thunk, ..opt },
   if is_trace_enabled_for `silence_suggest then
     skip
   else
@@ -444,10 +444,11 @@ You can also use `library_search with attr` to include all lemmas with the attri
 meta def library_search (semireducible : parse $ optional (tk "!"))
   (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
   (opt : opt := { }) : tactic unit :=
-do asms ← mk_assumption_set ff hs attr_names,
+do (lemma_thunks, ctx_thunk) ← mk_assumption_set ff hs attr_names,
    (tactic.library_search
      { backtrack_all_goals := tt,
-       lemma_thunks := return asms,
+       lemma_thunks := some lemma_thunks,
+       ctx_thunk := ctx_thunk,
        md := if semireducible.is_some then
          tactic.transparency.semireducible else tactic.transparency.reducible,
        ..opt } >>=

test/solve_by_elim.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Scott Morrison
 -/
 import tactic.solve_by_elim
+import tactic.rcases
+import tactic.interactive
 
 example {a b : Prop} (h₀ : a → b) (h₁ : a) : b :=
 begin
@@ -157,3 +159,15 @@ end
 
 -- We verify that the solution did use `b`.
 example : solve_by_elim_use_b 1 2 = (1, 1, 2) := rfl
+
+-- Test that `solve_by_elim*`, which works on multiple goals,
+-- successfully uses the relevant local hypotheses for each goal.
+example (f g : ℕ → Prop) : (∃ k : ℕ, f k) ∨ (∃ k : ℕ, g k) ↔ ∃ k : ℕ, f k ∨ g k :=
+begin
+  dsimp at *,
+  fsplit,
+  rintro (⟨n, fn⟩ | ⟨n, gn⟩),
+  swap 3,
+  rintro ⟨n, hf | hg⟩,
+  solve_by_elim* [or.inl, or.inr, Exists.intro] { max_depth := 20 },
+end