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.

meta def tactic.interactive.equiv_rw_hyp_aux (hyp : name) (cfg : tactic.equiv_rw_cfg) (permissive : bool := bool.ff) :

Auxiliary function to call equiv_rw_hyp on a list pexpr recursively.

Auxiliary function to call equiv_rw_target on a list pexpr recursively.

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}.

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}.

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


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