The transfer tactic

transfer α → β => tacs turns a goal about α into the equivalent goal about β along an equivalence e : α ≃ β, then runs tacs on it. The goal is rewritten in place, so closing the transferred goal closes the original one: nothing has to be transferred back explicitly.

For instance, given instance : TransferEquiv ZFNat ℕ := ⟨ringEquivNat.toEquiv⟩,

example (n m : ZFNat) : n + m = m + n := by
  transfer ZFNat → ℕ =>
    rw [Nat.add_comm]

The equivalence is found by instance synthesis on TransferEquiv α β. It may also be given explicitly, either as transfer α → β using e => tacs, or by naming it in place of the two types, as transfer e => tacs, in which case the direction is read off the type of e. A bundled isomorphism (≃+*, ≃*, ≃o, anything with an EquivLike instance) is accepted wherever an equivalence is, and coerced to the equivalence underlying it. Going the other way, as in transfer e.symm => tacs, only makes sense if transfer_simps holds the lemmas for that direction: a simp set oriented the wrong way loops.

Transferring proceeds in three steps:

• every hypothesis whose type mentions α is reverted, and each binder ∀ (x : t), _ of the resulting goal whose type t is built out of α is replaced by ∀ (y : t[β/α]), _ through Equiv.forall_congr_left, which puts E.symm y where x used to be. The equivalence E : t ≃ t[β/α] is built from e by congruence, so that a function f : α → α is transferred to a function β → β, and so on for the type formers congrEquiv knows about;
• the transfer_simps simp set, together with ne_eq and lemmas lifting equalities and binders along the equivalences at hand, pushes them through the goal until no α is left. The lemmas of that simp set are what describes how the operations of α are read in β, e.g. e (a + b) = e a + e b;
• the reverted hypotheses are reintroduced under their original names, and tacs is run on the resulting goal.

def Parser.Attr.transfer_simps_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.transfer_simps : Lean.ParserDescr

Simp set used by the transfer tactic to push an equivalence through a goal. Its lemmas state how the operations of the source type are read in the target type, e.g. e (a + b) = e a + e b for the equivalence e a goal is transferred along.

Equations

• One or more equations did not get rendered due to their size.

class TransferEquiv (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)

TransferEquiv α β bundles an equivalence α ≃ β as a class, so that transfer α → β can find it by instance synthesis.

• equiv : α ≃ β

  The equivalence along which goals are transferred.

Lemmas used to push equivalences through a goal

These are an implementation detail of the tactic, but they have to be public: the tactic looks them up by name in the environment of the file it runs in, and a private declaration is not exported to importing modules at all.

theorem ZFLean.Transfer.arrowCongr_apply {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (f : α₁ → β₁) (x : α₂) : (e₁.arrowCongr e₂) f x = e₂ (f (e₁.symm x))

Applying Equiv.arrowCongr is conjugating.

theorem ZFLean.Transfer.arrowCongr_symm_apply {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (f : α₂ → β₂) (x : α₁) : (e₁.arrowCongr e₂).symm f x = e₂.symm (f (e₁ x))

Applying the inverse of Equiv.arrowCongr is conjugating the other way round. This is Equiv.arrowCongr_symm followed by arrowCongr_apply, but as a single step: rewriting with Equiv.arrowCongr_symm alone would break the E (E.symm x) pattern that collapses an equation between functions.

theorem ZFLean.Transfer.arrowCongr_symm_iterate {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) (f : β → β) (n : ℕ) (x : α) : ((e.arrowCongr e).symm f)^[n] x = e.symm (f^[n] (e x))

Iterating a conjugated function is conjugating the iterate: this is what makes a statement about f^[n] travel, f being a binder of type α → α.

theorem ZFLean.Transfer.prodCongr_apply {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (p : α₁ × β₁) : (e₁.prodCongr e₂) p = (e₁ p.fst, e₂ p.snd)

Applying Equiv.prodCongr is applying both components.

theorem ZFLean.Transfer.prodCongr_symm_apply {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (p : α₂ × β₂) : (e₁.prodCongr e₂).symm p = (e₁.symm p.fst, e₂.symm p.snd)

Applying the inverse of Equiv.prodCongr is applying both inverses.

theorem ZFLean.Transfer.forallLift {α : Sort u} {β : Sort v} (e : α ≃ β) (p : α → Prop) : (∀ (x : α), p x) ↔ ∀ (x : β), p (e.symm x)

Equiv.forall_congr_left, with p explicit so that it can be used as a simp lemma.

theorem ZFLean.Transfer.existsLift {α : Sort u} {β : Sort v} (e : α ≃ β) (p : α → Prop) : (∃ (x : α), p x) ↔ ∃ (x : β), p (e.symm x)

Equiv.exists_congr_left, with p explicit so that it can be used as a simp lemma.

theorem ZFLean.Transfer.eqLift {α : Sort u} {β : Sort v} (e : α ≃ β) (x y : α) : x = y ↔ e x = e y

An equation in α is the equation between the images in β.

Transporting the types of the binders

The tactic itself

def ZFLean.Transfer.transfer : Lean.ParserDescr

transfer α → β => tacs transfers the goal along an equivalence α ≃ β and runs tacs on the transferred goal, which now talks about β instead of α:

example (n m : ZFNat) : n + m = m + n := by
  transfer ZFNat → ℕ =>
    rw [Nat.add_comm]

The equivalence is synthesized from a TransferEquiv α β instance, or given explicitly by transfer α → β using e => tacs. Passing the equivalence alone, as in transfer e => tacs, is also accepted: the direction is then read off the type of e. In both cases e may be a bundled isomorphism, such as a ≃+* or a ≃o.

Equations

• One or more equations did not get rendered due to their size.