feat(tactic/rewrite_search): Automatically searching for chains of re…

…writes (#4841)

This pull request is based on a branch originally developed by @semorrison , @khoek , and @jcommelin . The idea of rewrite_search is a tactic that will search through chains of potential rewrites to prove the goal, when the goal is an equality or iff statement. There are three key components: `discovery.lean` finds a bunch of rules that can be used to generate rewrites, `search.lean` runs a breadth-first-search algorithm on the two sides of the quality to find a path that connects them, and `explain.lean` generates Lean code from the resulting proof, so that you can replace the call to `rewrite_search` with the explicit steps for it.

I removed some functionality from the rewrite_search branch and simplified the data structures somewhat in order to get this pull request small enough to be reviewed. If there is functionality from that branch that people particularly wanted, let me know and I can either include it in this PR or in a subsequent one. In particular, most of the configuration options are omitted.

For data structures, the whole `table` data structure is gone, replaced by a `buffer` and `rb_map` for efficient lookup. Write access to the buffer is also append-only for efficiency. This seems to be a lot faster, although I haven't created specific performance benchmarks.

Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Keeley Hoek <keeley@hoek.io>

src/data/buffer/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 
-Traversable instance for buffers.
+General utility functions for buffers.
 -/
 import data.buffer
 import data.array.lemmas
@@ -62,4 +62,11 @@ equiv.traversable list_equiv_buffer
 instance : is_lawful_traversable buffer :=
 equiv.is_lawful_traversable list_equiv_buffer
 
+/--
+A convenience wrapper around `read` that just fails if the index is out of bounds.
+-/
+meta def read_t (b : buffer α) (i : ℕ) : tactic α :=
+if h : i < b.size then return $ b.read (fin.mk i h)
+else tactic.fail "invalid buffer access"
+
 end buffer

src/meta/expr_lens.lean

@@ -5,7 +5,7 @@ Authors: Johan Commelin, Keeley Hoek, Scott Morrison
 -/
 import meta.expr
 /-!
-# A lens for zoming into nested `expr` applications
+# A lens for zooming into nested `expr` applications
 
 A "lens" for looking into the subterms of an expression, tracking where we've been, so that
 when we "zoom out" after making a change we know exactly which order of `congr_fun`s and
@@ -37,8 +37,8 @@ namespace expr_lens
 that represent the function-part `f` and arg-part `a` of an application `f a`. They specify the
 directions in which an `expr_lens` should zoom into an `expr`.
 
-This type is used in the development of rewriting tactics such as
-`nth_rewrite`, and `rewrite_search` (not currently in mathlib). -/
+This type is used in the development of rewriting tactics such as `nth_rewrite` and
+`rewrite_search`. -/
 @[derive [decidable_eq, inhabited]]
 inductive dir
 | F

src/tactic/nth_rewrite/congr.lean

@@ -68,16 +68,10 @@ do
 
 /-- List of all rewrites of an expression `e` by `r : expr × bool`.
 Here `r.1` is the substituting expression and `r.2` flags the direction of the rewrite. -/
-meta def nth_rewrite (e : expr) (r : expr × bool) (cfg : nth_rewrite.cfg := {}) :
+meta def all_rewrites (e : expr) (r : expr × bool) (cfg : nth_rewrite.cfg := {}) :
   tactic (list tracked_rewrite) :=
 e.app_map (rewrite_at_lens cfg r)
 
-/-- Lazy list of all rewrites of an expression `e` by `r : expr × bool`.
-Here `r.1` is the substituting expression and `r.2` flags the direction of the rewrite. -/
-meta def nth_rewrite_lazy (e : expr) (r : expr × bool) (cfg : nth_rewrite.cfg := {}) :
-  mllist tactic tracked_rewrite :=
-mllist.squash $ mllist.of_list <$> nth_rewrite e r cfg
-
 end nth_rewrite.congr
 
 end tactic

src/tactic/nth_rewrite/default.lean

@@ -14,7 +14,7 @@ that give the user more control over where to perform a rewrite.
 
 ## Main definitions
 
-* `nth_write n rules`: performs only the `n`th possible rewrite using the `rules`.
+* `nth_rewrite n rules`: performs only the `n`th possible rewrite using the `rules`.
 * `nth_rewrite_lhs`: as above, but only rewrites on the left hand side of an equation or iff.
 * `nth_rewrite_rhs`: as above, but only rewrites on the right hand side of an equation or iff.
 
@@ -56,7 +56,7 @@ do r ← to_expr p.rule tt ff,
 /-- Get the `n`th rewrite of rewrite rules `q` in expression `e`,
 or fail if there are not enough such rewrites. -/
 meta def get_nth_rewrite (n : ℕ) (q : rw_rules_t) (e : expr) : tactic tracked_rewrite :=
-do rewrites ← q.rules.mmap $ λ r, unpack_rule r >>= nth_rewrite e,
+do rewrites ← q.rules.mmap $ λ r, unpack_rule r >>= all_rewrites e,
    rewrites.join.nth n <|> fail "failed: not enough rewrites found"
 
 /-- Rewrite the `n`th occurrence of the rewrite rules `q` of (optionally after zooming into) a

src/tactic/rewrite_search/default.lean

@@ -0,0 +1 @@
+import tactic.rewrite_search.frontend

src/tactic/rewrite_search/discovery.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2020 Kevin Lacker, Keeley Hoek, Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Lacker, Keeley Hoek, Scott Morrison
+-/
+import tactic.nth_rewrite
+import tactic.rewrite_search.types
+
+/-!
+# Generating a list of rewrites to use as steps in rewrite search.
+-/
+
+namespace tactic.rewrite_search
+
+open tactic tactic.interactive tactic.rewrite_search
+
+/--
+Convert a list of expressions into a list of rules. The difference is that a rule
+includes a flag for direction, so this simply includes each expression twice,
+once in each direction.
+-/
+private meta def rules_from_exprs (l : list expr) : list (expr × bool) :=
+l.map (λ e, (e, ff)) ++ l.map (λ e, (e, tt))
+
+/-- Returns true if expression is an equation or iff. -/
+private meta def is_acceptable_rewrite : expr → bool
+| (expr.pi n bi d b) := is_acceptable_rewrite b
+| `(%%a = %%b)       := tt
+| `(%%a ↔ %%b)       := tt
+| _                  := ff
+
+/-- Returns true if the expression is an equation or iff and has no metavariables. -/
+private meta def is_acceptable_hyp (r : expr) : tactic bool :=
+do t ← infer_type r >>= whnf, return $ is_acceptable_rewrite t ∧ ¬t.has_meta_var
+
+/-- Collect all hypotheses in the local context that are usable as rewrite rules. -/
+private meta def rules_from_hyps : tactic (list (expr × bool)) :=
+do hyps ← local_context,
+  rules_from_exprs <$> hyps.mfilter is_acceptable_hyp
+
+/-- Use this attribute to make `rewrite_search` use this definition during search. -/
+@[user_attribute]
+meta def rewrite_search_attr : user_attribute :=
+{ name := `rewrite,
+  descr := "declare that this definition should be considered by `rewrite_search`" }
+
+/-- Gather rewrite rules from lemmas explicitly tagged with `rewrite. -/
+private meta def rules_from_rewrite_attr : tactic (list (expr × bool)) :=
+do names ← attribute.get_instances `rewrite,
+  rules_from_exprs <$> names.mmap mk_const
+
+/--
+Collect rewrite rules to use from the environment.
+-/
+meta def collect_rules : tactic (list (expr × bool)) :=
+do from_attr    ← rules_from_rewrite_attr,
+  from_hyps     ← rules_from_hyps,
+  return $ from_attr ++ from_hyps
+
+open tactic.nth_rewrite tactic.nth_rewrite.congr
+
+/--
+Constructing our rewrite structure from the `tracked_rewrite` provided by `nth_rewrite`.
+rule_index is the index of the rule used from the rules provided.
+tracked is an (index, tracked_rewrite) pair for the element of `all_rewrites exp rule` we used.
+-/
+private meta def from_tracked (rule_index : ℕ) (tracked : ℕ × tracked_rewrite) : rewrite :=
+do let (rw_index, rw) := tracked,
+  let h : how := ⟨rule_index, rw_index, rw.addr⟩,
+  ⟨rw.exp, rw.proof, h⟩
+
+/--
+Get all rewrites that start at the given expression and use the given rewrite rule.
+-/
+private meta def rewrites_for_rule (exp : expr) (cfg : config) (numbered_rule: ℕ × expr × bool) :
+  tactic (list rewrite) :=
+do let (rule_index, rule) := numbered_rule,
+  tracked ← all_rewrites exp rule cfg.to_cfg,
+  return (list.map (from_tracked rule_index) tracked.enum)
+
+/--
+Get all rewrites that start at the given expression and use one of the given rewrite rules.
+-/
+meta def get_rewrites (rules : list (expr × bool)) (exp : expr) (cfg : config) :
+  tactic (buffer rewrite) :=
+do lists ← list.mmap (rewrites_for_rule exp cfg) rules.enum,
+  return (list.foldl buffer.append_list buffer.nil lists)
+
+end tactic.rewrite_search