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

• ⊢ α to ⊢ β,
• ⊢ option α to ⊢ option β
• ⊢ {a // P} to {b // P (⇑(equiv.symm e) b)}

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

• equiv.arrow_congr',
• equiv.subtype_equiv_of_subtype',
• equiv.sigma_congr_left', and
• equiv.Pi_congr_left'.

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.

A list of lemmas used for constructing congruence equivalences.

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 α)).

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.

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

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

The simpset equiv_rw_simp is used by the tactic equiv_rw to simplify applications of equivalences and their inverses.

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

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

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

Rewrite the goal using an equiv e.

equiv_rw e at h, where h : α is a hypothesis, and e : α ≃ β, will attempt to transport 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 will also try rewriting under (equiv_)functors, so 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}.

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