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', andequiv.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.
- max_depth : ℕ
Configuration structure for equiv_rw.
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.
equiv_rw_type e t rewrites the type t using the equivalence e : α ≃ β,
returning a new equivalence t ≃ t'.
Attempt to replace the hypothesis with name x
by transporting it along the equivalence in e : α ≃ β.
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: