mathlib3 documentation

tactic.nth_rewrite.default

Advanced rewriting tactics #

This file provides three interactive tactics that give the user more control over where to perform a rewrite.

Main definitions #

Implementation details #

There are two alternative backends, provided by .congr and .kabstract. The kabstract backend is not currently available through mathlib.

The kabstract backend is faster, but if there are multiple identical occurrences of the same rewritable subexpression, all are rewritten simultaneously, and this isn't always what we want. (In particular, rewrite_search is much less capable on the category_theory library.)

source
meta def tactic.target_or_hyp_type  :
option expr → tactic expr

Returns the target of the goal when passed none, otherwise, return the type of h in some h.

source
meta def tactic.replace_in_state  :
option expr → expr → expr → tactic unit

Replace the target, or a hypothesis, depending on whether none or some h is given as the first argument.

source
meta def tactic.get_nth_rewrite (n : ℕ) (q : tactic.interactive.rw_rules_t) (e : expr) :
tactic tactic.nth_rewrite.tracked_rewrite

Get the nth rewrite of rewrite rules q in expression e, or fail if there are not enough such rewrites.

source
meta def tactic.get_nth_rewrite_with_zoom (n : ℕ) (q : tactic.interactive.rw_rules_t) (path : list expr_lens.dir) (h : option expr) :
tactic tactic.nth_rewrite.tracked_rewrite

Rewrite the nth occurrence of the rewrite rules q of (optionally after zooming into) a hypothesis or target h which is an application of a relation.

source
meta def tactic.nth_rewrite_core (path : list expr_lens.dir) (n : interactive.parse lean.parser.small_nat) (q : interactive.parse tactic.interactive.rw_rules) (l : interactive.parse interactive.types.location) :
tactic unit

Rewrite the nth occurrence of the rewrite rules q (optionally on a side) at all the locations loc.

source
meta def tactic.interactive.nth_rewrite (n : interactive.parse lean.parser.small_nat) (q : interactive.parse tactic.interactive.rw_rules) (l : interactive.parse interactive.types.location) :
tactic unit

nth_rewrite n rules performs only the nth possible rewrite using the rules. The tactics nth_rewrite_lhs and nth_rewrite_rhs are variants that operate on the left and right hand sides of an equation or iff.

Note: n is zero-based, so nth_rewrite 0 h will rewrite along h at the first possible location.

In more detail, given rules = [h1, ..., hk], this tactic will search for all possible locations where one of h1, ..., hk can be rewritten, and perform the nth occurrence.

Example: Given a goal of the form a + x = x + b, and hypothesis h : x = y, the tactic nth_rewrite 1 h will change the goal to a + x = y + b.

The core rewrite has a occs configuration setting intended to achieve a similar purpose, but this doesn't really work. (If a rule matches twice, but with different values of arguments, the second match will not be identified.)

source
meta def tactic.interactive.nth_rewrite_lhs (n : interactive.parse lean.parser.small_nat) (q : interactive.parse tactic.interactive.rw_rules) (l : interactive.parse interactive.types.location) :
tactic unit

nth_rewrite n rules performs only the nth possible rewrite using the rules. The tactics nth_rewrite_lhs and nth_rewrite_rhs are variants that operate on the left and right hand sides of an equation or iff.

Note: n is zero-based, so nth_rewrite 0 h will rewrite along h at the first possible location.

In more detail, given rules = [h1, ..., hk], this tactic will search for all possible locations where one of h1, ..., hk can be rewritten, and perform the nth occurrence.

Example: Given a goal of the form a + x = x + b, and hypothesis h : x = y, the tactic nth_rewrite 1 h will change the goal to a + x = y + b.

The core rewrite has a occs configuration setting intended to achieve a similar purpose, but this doesn't really work. (If a rule matches twice, but with different values of arguments, the second match will not be identified.)

source
meta def tactic.interactive.nth_rewrite_rhs (n : interactive.parse lean.parser.small_nat) (q : interactive.parse tactic.interactive.rw_rules) (l : interactive.parse interactive.types.location) :
tactic unit

nth_rewrite n rules performs only the nth possible rewrite using the rules. The tactics nth_rewrite_lhs and nth_rewrite_rhs are variants that operate on the left and right hand sides of an equation or iff.

Note: n is zero-based, so nth_rewrite 0 h will rewrite along h at the first possible location.

In more detail, given rules = [h1, ..., hk], this tactic will search for all possible locations where one of h1, ..., hk can be rewritten, and perform the nth occurrence.

Example: Given a goal of the form a + x = x + b, and hypothesis h : x = y, the tactic nth_rewrite 1 h will change the goal to a + x = y + b.

The core rewrite has a occs configuration setting intended to achieve a similar purpose, but this doesn't really work. (If a rule matches twice, but with different values of arguments, the second match will not be identified.)

source
def tactic_doc.tactic.nth_rewrite / nth_rewrite_lhs / nth_rewrite_rhs  :
tactic_doc_entry

nth_rewrite n rules performs only the nth possible rewrite using the rules. The tactics nth_rewrite_lhs and nth_rewrite_rhs are variants that operate on the left and right hand sides of an equation or iff.

Note: n is zero-based, so nth_rewrite 0 h will rewrite along h at the first possible location.

In more detail, given rules = [h1, ..., hk], this tactic will search for all possible locations where one of h1, ..., hk can be rewritten, and perform the nth occurrence.

Example: Given a goal of the form a + x = x + b, and hypothesis h : x = y, the tactic nth_rewrite 1 h will change the goal to a + x = y + b.

The core rewrite has a occs configuration setting intended to achieve a similar purpose, but this doesn't really work. (If a rule matches twice, but with different values of arguments, the second match will not be identified.)