mathlib3 documentation

tactic.equiv_rw

The equiv_rw tactic transports goals or hypotheses along equivalences. #

The basic syntax is equiv_rw e, where e : α ≃ β is an equivalence. This will try to replace occurrences of α in the goal with β, for example transforming

The tactic can also be used to rewrite hypotheses, using the syntax equiv_rw e at h.

Implementation details #

The main internal function is equiv_rw_type e t, which attempts to turn an expression e : α ≃ β into a new equivalence with left hand side t. As an example, with t = option α, it will generate functor.map_equiv option e.

This is achieved by generating a new synthetic goal %%t ≃ _, and calling solve_by_elim with an appropriate set of congruence lemmas. To avoid having to specify the relevant congruence lemmas by hand, we mostly rely on equiv_functor.map_equiv and bifunctor.map_equiv along with some structural congruence lemmas such as

The main equiv_rw function, when operating on the goal, simply generates a new equivalence e' with left hand side matching the target, and calls apply e'.inv_fun.

When operating on a hypothesis x : α, we introduce a new fact h : x = e.symm (e x), revert this, and then attempt to generalize, replacing all occurrences of e x with a new constant y, before introing and substing h, and renaming y back to x.

Future improvements #

In a future PR I anticipate that derive equiv_functor should work on many examples, (internally using transport, which is in turn based on equiv_rw) and we can incrementally bootstrap the strength of equiv_rw.

An ambitious project might be to add equiv_rw!, a tactic which, when failing to find appropriate equiv_functor instances, attempts to derive them on the spot.

For now equiv_rw is entirely based on equiv, but the framework can readily be generalised to also work with other types of equivalences, for example specific notations such as ring equivalence (≃+*), or general categorical isomorphisms (≅).

This will allow us to transport across more general types of equivalences, but this will wait for another subsequent PR.

source
meta def tactic.equiv_congr_lemmas  :
list (tactic expr)

A list of lemmas used for constructing congruence equivalences.

source
meta structure tactic.equiv_rw_cfg  :
Type
  • max_depth : ℕ

Configuration structure for equiv_rw.

  • max_depth bounds the search depth for equivalences to rewrite along. The default value is 10. (e.g., if you're rewriting along e : α ≃ β, and max_depth := 2, you can rewrite option (option α)) but not option (option (option α)).
source
meta def tactic.equiv_rw_type_core (eq : expr) (cfg : tactic.equiv_rw_cfg) :
tactic unit

Implementation of equiv_rw_type, using solve_by_elim. Expects a goal of the form t ≃ _, and tries to solve it using eq : α ≃ β and congruence lemmas.

source
meta def tactic.equiv_rw_type (eqv ty : expr) (cfg : tactic.equiv_rw_cfg) :
tactic expr

equiv_rw_type e t rewrites the type t using the equivalence e : α ≃ β, returning a new equivalence t ≃ t'.

source
meta def tactic.equiv_rw_hyp (x : name) (e : expr) (cfg : tactic.equiv_rw_cfg := {max_depth := 10}) :
tactic unit

Attempt to replace the hypothesis with name x by transporting it along the equivalence in e : α ≃ β.

source
meta def tactic.equiv_rw_target (e : expr) (cfg : tactic.equiv_rw_cfg := {max_depth := 10}) :
tactic unit

Rewrite the goal using an equiv e.

source
meta def tactic.interactive.equiv_rw_hyp_aux (hyp : name) (cfg : tactic.equiv_rw_cfg) (permissive : bool := bool.ff) :
list expr → tactic.interactive.itactic

Auxiliary function to call equiv_rw_hyp on a list pexpr recursively.

source
meta def tactic.interactive.equiv_rw_target_aux (cfg : tactic.equiv_rw_cfg) (permissive : bool) :
list expr → tactic.interactive.itactic

Auxiliary function to call equiv_rw_target on a list pexpr recursively.

source
meta def tactic.interactive.equiv_rw (l : interactive.parse interactive.types.pexpr_list_or_texpr) (locat : interactive.parse interactive.types.location) (cfg : tactic.equiv_rw_cfg := {max_depth := 10}) :
tactic.interactive.itactic

equiv_rw e at h₁ h₂ ⋯, where each hᵢ : α is a hypothesis, and e : α ≃ β, will attempt to transport each hᵢ along e, producing a new hypothesis hᵢ : β, with all occurrences of hᵢ in other hypotheses and the goal replaced with e.symm hᵢ.

equiv_rw e will attempt to transport the goal along an equivalence e : α ≃ β. In its minimal form it replaces the goal ⊢ α with ⊢ β by calling apply e.inv_fun.

equiv_rw [e₁, e₂, ⋯] at h₁ h₂ ⋯ is equivalent to { equiv_rw [e₁, e₂, ⋯] at h₁, equiv_rw [e₁, e₂, ⋯] at h₂, ⋯ }.

equiv_rw [e₁, e₂, ⋯] at * will attempt to apply equiv_rw [e₁, e₂, ⋯] on the goal and on each expression available in the local context (except on the eᵢs themselves), failing silently when it can't. Failing on a rewrite for a certain eᵢ at a certain hypothesis h doesn't stop equiv_rw from trying the other equivalences on the list at h. This only happens for the wildcard location.

equiv_rw will also try rewriting under (equiv_)functors, so it can turn a hypothesis h : list α into h : list β or a goal ⊢ unique α into ⊢ unique β.

The maximum search depth for rewriting in subexpressions is controlled by equiv_rw e {max_depth := n}.

source
def tactic_doc.tactic.equiv_rw  :
tactic_doc_entry

equiv_rw e at h₁ h₂ ⋯, where each hᵢ : α is a hypothesis, and e : α ≃ β, will attempt to transport each hᵢ along e, producing a new hypothesis hᵢ : β, with all occurrences of hᵢ in other hypotheses and the goal replaced with e.symm hᵢ.

equiv_rw e will attempt to transport the goal along an equivalence e : α ≃ β. In its minimal form it replaces the goal ⊢ α with ⊢ β by calling apply e.inv_fun.

equiv_rw [e₁, e₂, ⋯] at h₁ h₂ ⋯ is equivalent to { equiv_rw [e₁, e₂, ⋯] at h₁, equiv_rw [e₁, e₂, ⋯] at h₂, ⋯ }.

equiv_rw [e₁, e₂, ⋯] at * will attempt to apply equiv_rw [e₁, e₂, ⋯] on the goal and on each expression available in the local context (except on the eᵢs themselves), failing silently when it can't. Failing on a rewrite for a certain eᵢ at a certain hypothesis h doesn't stop equiv_rw from trying the other equivalences on the list at h. This only happens for the wildcard location.

equiv_rw will also try rewriting under (equiv_)functors, so it can turn a hypothesis h : list α into h : list β or a goal ⊢ unique α into ⊢ unique β.

The maximum search depth for rewriting in subexpressions is controlled by equiv_rw e {max_depth := n}.

source
meta def tactic.interactive.equiv_rw_type (e : interactive.parse interactive.types.texpr) (cfg : tactic.equiv_rw_cfg := {max_depth := 10}) :
tactic.interactive.itactic

Solve a goal of the form t ≃ _, by constructing an equivalence from e : α ≃ β. This is the same equivalence that equiv_rw would use to rewrite a term of type t.

A typical usage might be:

have e' : option α ≃ option β := by equiv_rw_type e
source
def tactic_doc.tactic.equiv_rw_type  :
tactic_doc_entry

Solve a goal of the form t ≃ _, by constructing an equivalence from e : α ≃ β. This is the same equivalence that equiv_rw would use to rewrite a term of type t.

A typical usage might be:

have e' : option α ≃ option β := by equiv_rw_type e