Retype

A small, dependency-free Lean 4 metaprogramming library that rewrites elaborated expressions, definitions and theorems from one type to another — e.g. mathlib's ℝ to Float (to make formulas executable), ℝ to ℂ, Nat to Int, or any other pair you register.

Think of it as a user-extensible generalization of mathlib's @[to_additive] name-replacement machinery, without the Mul/Add hardcoding — and unlike SciLean's isomorph, it introduces no fake isomorphism axioms: this is honest, typechecked code generation. Theorems can be transported too (retype_thm) when the retyping is mathematically meaningful (e.g. ℝ → ℂ): the transported proof is re-checked by the kernel, so success means a genuine proof. For ℝ → Float no theorems transport — a theorem about ℝ is generally false for Float.

Quick start

import Retype

declare_retype NatToFloat : Nat => Float   -- declare a retyping with its type pair

-- term-level: translate an expression in place, addressing it by type pair
def g : Float → Float := retype% Nat => Float (fun x : Nat => (x + 3) / 2)
#eval g 4.0        -- 3.5  (the Nat original gives 3!)

-- inspect a translation
#retype Nat => Float (fun x : Nat => x * 2 + 1)   -- fun x => x * 2 + 1 : Float → Float

-- register extra constant mappings (constants from any imported package)
retype_rule Nat => Float : Nat.halved => Float.halved

-- declaration-level: translate an existing def
def natPoly (x : Nat) : Nat := x * x + 2 * x + 1
retype_def floatPoly := natPoly using Nat => Float
#eval floatPoly 1.5   -- 6.25

Everywhere a retyping is expected you can use either its type pair (Nat => Float) or its name (NatToFloat). Names matter when you declare several strategies for the same pair (say, a fast-approximation and an interval-arithmetic ℝ => Float) — the pair form then reports an ambiguity and you pick one by name.

retype_def also registers natPoly => floatPoly as a rule, so definitions that use natPoly translate automatically afterwards.

The same works as an attribute, on defs and theorems:

@[retype Nat => Float floatCube]
def cube (x : Nat) : Nat := x * x * x

@[retype NatToFloat]            -- default target name: cube2.NatToFloat
def cube2 (x : Nat) : Nat := x * cube x

How it works

This is not a syntactic macro: it transforms the elaborated expression (a macro rewriting the surface syntax would miss implicit type arguments, notation, and literals hidden inside instances). The transformation walks the term and

• replaces every mapped constant by its target,
• drops all instance-implicit arguments and re-synthesizes them against the replaced types (so you never register Real.instAdd or OfNat instances — x + y, numeric literals, 2 * x, … just work),
• re-typechecks the final term before accepting it.

When a constant has no counterpart at the target type, you get an error telling you exactly which retype_rule to add.

The headline use case: mathlib ℝ → Float

This package has no mathlib dependency; in a project that uses mathlib, register the functions you need:

import Retype
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

declare_retype RealToFloat : Real => Float
retype_rule Real => Float : Real.sqrt => Float.sqrt
retype_rule Real => Float : Real.cos  => Float.cos
retype_rule Real => Float : Real.exp  => Float.exp
retype_rule Real => Float : Real.pi   => Float.pi   -- Float.pi ships with Retype

-- a formula written against ℝ …
noncomputable def gauss (x : ℝ) : ℝ :=
  Real.exp (-(x^2) / 2) / Real.sqrt (2 * Real.pi)

-- … made executable
retype_def gaussF := gauss using Real => Float
#eval gaussF 0.0   -- 0.398942…

Retype.Float (imported by Retype) provides HPow Float ℕ Float / HPow Float ℤ Float instances — mathlib powers like x ^ 2 have a ℕ exponent that survives the replacement — plus Float.pi.

ℝ → ℂ

Same mechanism; both types live in mathlib:

declare_retype RealToComplex : Real => Complex
retype_rule Real => Complex : Real.exp => Complex.exp
retype_rule Real => Complex : Real.cos => Complex.cos

noncomputable def realWave (t : ℝ) : ℝ := Real.exp t * Real.cos (2 * t) + t ^ 2
retype_def complexWave := realWave using Real => Complex

example : complexWave = fun t : ℂ => Complex.exp t * Complex.cos (2 * t) + t ^ 2 := rfl

(retype_def detects that the result uses noncomputable constants and marks it noncomputable automatically.)

Theorem transport

For meaningful retypings like ℝ → ℂ, retype_thm transports the statement and the proof. Generic algebra (mul_comm, congrArg, even whole ring-generated proof terms) re-instantiates at the target type via instance re-synthesis; only source-specific lemmas need a rule:

retype_rule Real => Complex : Real.exp_add => Complex.exp_add

theorem realExpAdd (x y : ℝ) : Real.exp (x + y) = Real.exp x * Real.exp y :=
  Real.exp_add x y

retype_thm complexExpAdd := realExpAdd using Real => Complex
-- complexExpAdd : ∀ (x y : ℂ), Complex.exp (x + y) = Complex.exp x * Complex.exp y

-- even `ring` proofs transport:
@[retype Real => Complex complexSqExpand]
theorem realSqExpand (x : ℝ) : (x + 1) ^ 2 = x ^ 2 + 2 * x + 1 := by ring

There is no magic and no axiom: the transported proof term is re-checked by the kernel. If the statement is false at the target (e.g. anything using ℝ's order on ℂ), some constant will fail to translate and you get an error — never a bogus theorem.

Commands

Command	Purpose
declare_retype T : Src => Tgt	declare a named retyping with its principal type pair (pair optional: declare_retype T)
retype_rule ⟨T | Src => Tgt⟩ : src => tgt	register a constant mapping (constants may come from any imported package; universe parameter counts must match)
retype% ⟨T | Src => Tgt⟩ e	term elaborator: e with the retyping applied
#retype ⟨T | Src => Tgt⟩ e	print the translation of e and its type
retype_def new := old using ⟨T | Src => Tgt⟩	translate a definition, register old => new
retype_thm new := old using ⟨T | Src => Tgt⟩	transport a theorem statement + proof (kernel-checked)
@[retype ⟨T | Src => Tgt⟩ name?]	attribute form of the above, for defs and theorems; also usable post-hoc via attribute [retype ...] foo

Rules are stored in a persistent environment extension: register them in one module and they are visible everywhere it is imported.

Limitations (v1)

• Float has different semantics (rounding, no associativity, …) — extracted code is an approximation by design, and no theorem transports to Float. Theorem transport (retype_thm) is only useful for mathematically faithful retypings like ℝ → ℂ, and succeeds exactly when every source-specific lemma in the proof has a registered counterpart (the kernel re-checks everything).
• Definitions compiled by pattern matching / well-founded recursion generate auxiliary declarations (match_1, brecOn, …) that are not translated; retype_def works best on equation-free bodies. Translate helpers bottom-up with retype_def (each one auto-registers its rule).
• Occurrences of the source type are replaced everywhere: e.g. under Nat => Float, a ℕ exponent also becomes Float. Heterogeneous operations whose instance doesn't exist at the target produce an error naming the constant to map.
• Structures/inductives themselves are not translated — map their constants (Prod.fst, your own accessors) instead. Expr.proj field indices are assumed to align when you map a structure name.
• Mapped constants must have the same number of universe parameters.

Development

lake build   # library
lake test    # core-only tests (Nat → Int, Nat → Float)

Licensed under Apache 2.0.

Lean v4.32.0, no dependencies. Fully worked mathlib examples (verified against mathlib v4.32.0) live in examples/mathlib/ — build with cd examples/mathlib && lake exe cache get && lake build:

• RealDemo.lean — ℝ → Float and ℝ → ℂ, incl. theorem transport of a ring proof.

• ZetaDemo.lean — the Riemann ζ Dirichlet term written over mathlib's ℂ (Complex.cpow), retyped to a Float-backed ComplexF with a single rule (Complex => ComplexF; literals, Nat.cast and + * / ^ re-synthesize automatically), then evaluated with Borwein acceleration: #guards check ζ(2) = π²/6 to 1e−10 and |ζ(½ + 14.1347…i)| < 1e−6 (the first nontrivial zero). ZetaGrid.lean dumps a 220×560 grid of the critical strip for domain-coloring visualization (lake env lean --run ZetaGrid.lean, ~30 s interpreted):

  

  Hue = arg ζ(s), lightness = |ζ(s)|; the dark vortices on Re = ½ are the first five nontrivial zeros, the bright spot at the bottom is the pole at s = 1.