transport tactic #
transport attempts to move an
s : S α expression across an equivalence
e : α ≃ β to solve
a goal of the form
S β, by building the new object field by field, taking each field of
and rewriting it along
e using the
transport_simps is used by the tactic
to simplify certain expressions involving application of equivalences,
It's probably best not to adjust it without understanding the algorithm used by
Given a goal
⊢ S β for some type class
S, and an equivalence
e : α ≃ β.
transport using e will look for a hypothesis
s : S α,
and attempt to close the goal by transporting
s across the equivalence
You can specify the object to transport using
transport s using e.
transport works by attempting to copy each of the operations and axiom fields of
rewriting them using
equiv_rw e and defining a new structure using these rewritten fields.
If it fails to fill in all the new fields,
transport will produce new subgoals.
It's probably best to think about which missing
simp lemmas would have allowed
to finish, rather than solving these goals by hand.
(This may require looking at the implementation of
tranport to understand its algorithm;
there are several examples of "transport-by-hand" at the end of
transport is an abstraction of.)