The peano_bin_nat flagship, first-order slice

The Trocq flagship example (peano_bin_nat.v) transfers facts across the binary-vs-unary natural-number equivalence N ≃ nat. The paper's headline is that this needs no univalence. It splits into two parts of very different difficulty; this module realizes the tractable one and describes the harder one.

Mathlib's binary naturals are Num (with PosNum), and the cast Num → ℕ (Num.toNat) is a ring homomorphism that is injective (Num.to_nat_inj) — i.e. a ReprEmbeddingClass Num ℕ in the relation hierarchy. So:

First-order arithmetic transfer (this file)

Every first-order arithmetic theorem over Num transfers from its ℕ counterpart across the embedding: reflect the goal f a b = g a b through Num.to_nat_inj, apply the cast with the homomorphism lemmas (Num.add_to_nat/Num.mul_to_nat, the registered @[transfer] realizations), and close with the ℕ fact. Commutativity, associativity and distributivity on Num derive this way — the univalence-free first-order flagship the Trocq paper stresses needs no UA. These are Num theorems with no Num arithmetic done by hand; the work is entirely the transfer.

The induction principle, manually transferred (this file)

The flagship's headline is transferring the induction principle ∀ P : Num → Prop, P 0 → (∀ n, P n → P (n+1)) → ∀ n, P n across the equivalence. This file derives it as binNatInduction : BinNatInductionTarget, by transfer along the bijection Num ≃ ℕ: to prove ∀ n : Num, P n, rewrite n = Num.ofNat' (n : ℕ) (the round-trip Num.of_to_nat'), generalize (n : ℕ) and run Nat's recursor, mapping each ℕ step back to Num through the decoder (num_ofNat'_succ : Num.ofNat' (k+1) = Num.ofNat' k + 1). This is the recursor pulled back along the equivalence — the manual instance of what the flagship automates. It needs the full bijection, registered below as instance : ReprEquivClass Num ℕ (Trocq's top equiv level, which Num/ℕ reach because the cast is bijective, unlike the crypto byte encodings).

What is not done here is the MetaM motive synthesis that produces this transfer automatically for an arbitrary dependent motive P : Num → Type. That quantifies over a motive with both covariant and contravariant occurrences, so the automatic route needs the relation on Num → Type (a parametricity Param of types) and the (m,n) level inference that computes the minimal relation level each subterm requires. That engine is not implemented here (no Lean/Mathlib precedent). This file provides the manual recursor transfer; BinNatInductionTarget records its statement.

The embedding Num ↪ ℕ as a relation-hierarchy instance

@[instance_reducible]

instance Transfer.PeanoBinNat.instReprEmbeddingClassNumNat : ReprEmbeddingClass Num ℕ

The binary naturals embed into the unary naturals via the (injective) cast (↑· : Num → ℕ). This is a ReprEmbeddingClass — the level at which a decidable equality transfers in both directions.

Equations

• Transfer.PeanoBinNat.instReprEmbeddingClassNumNat = { enc := fun (m : Num) => ↑m, enc_inj := @Transfer.PeanoBinNat.instReprEmbeddingClassNumNat._proof_1 }

First-order arithmetic on Num, transferred from ℕ (no Num algebra by hand)

Each proof reflects through Num.to_nat_inj, applies the cast with the homomorphism lemmas, and closes with the corresponding ℕ fact.

theorem Transfer.PeanoBinNat.num_add_comm (a b : Num) : a + b = b + a

Commutativity of + on Num, transferred from Nat.add_comm.

theorem Transfer.PeanoBinNat.num_mul_comm (a b : Num) : a * b = b * a

Commutativity of * on Num, transferred from Nat.mul_comm.

theorem Transfer.PeanoBinNat.num_add_assoc (a b c : Num) : a + b + c = a + (b + c)

Associativity of + on Num, transferred from Nat.add_assoc.

theorem Transfer.PeanoBinNat.num_mul_assoc (a b c : Num) : a * b * c = a * (b * c)

Associativity of * on Num, transferred from Nat.mul_assoc.

theorem Transfer.PeanoBinNat.num_mul_add (a b c : Num) : a * (b + c) = a * b + a * c

Left distributivity on Num, transferred from Nat.mul_add.

theorem Transfer.PeanoBinNat.num_add_mul (a b c : Num) : (a + b) * c = a * c + b * c

Right distributivity on Num, transferred from Nat.add_mul.

theorem Transfer.PeanoBinNat.num_zero_add (a : Num) : 0 + a = a

Left identity for + on Num, transferred from Nat.zero_add.

theorem Transfer.PeanoBinNat.num_add_zero (a : Num) : a + 0 = a

Right identity for + on Num, transferred from Nat.add_zero.

theorem Transfer.PeanoBinNat.num_le_iff_to_nat_le (a b : Num) : a ≤ b ↔ ↑a ≤ ↑b

The Num order transferred from the ℕ order across the embedding: a ≤ b on Num iff (a:ℕ) ≤ (b:ℕ). The embedding Num ↪ ℕ is an order embedding, so ≤-facts transfer just like the equational ones.

theorem Transfer.PeanoBinNat.num_le_trans {a b c : Num} (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c

Transitivity of ≤ on Num, transferred from Nat.le_trans through the order embedding.

The full equivalence Num ≃ ℕ as the top hierarchy level

The embedding above is in fact a bijection: Num.ofNat' decodes ℕ → Num and round-trips on the encoding (Num.of_to_nat'). So — unlike the crypto byte encodings, which are injective-but-not-surjective and therefore bottom out at ReprEmbeddingClass — Num ↪ ℕ reaches Trocq's top equiv-level relation. This is the structure the peano_bin_nat flagship's automatic recursor transfer is built over.

@[instance_reducible]

instance Transfer.PeanoBinNat.instReprEquivClassNumNat : ReprEquivClass Num ℕ

Num ≃ ℕ registered at the equivalence level of the hierarchy: enc is the cast Num → ℕ, dec is Num.ofNat' : ℕ → Num, and dec_enc is the round-trip Num.of_to_nat'. The top level the SIP/univalence route uses; Num/ℕ reach it because the cast is a bijection.

Equations

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

The induction principle: statement, then the manual recursor transfer

BinNatInductionTarget names the Num induction principle as a proposition; binNatInduction below proves it by transferring Nat's recursor across the Num ≃ ℕ equivalence. The library does not synthesize this proof automatically for an arbitrary dependent motive (the Trocq peano_bin_nat one-liner); that requires the relation on Num → Type and an (m,n) level inference that transfer does not perform.

def Transfer.PeanoBinNat.BinNatInductionTarget : Prop

The Num induction principle, named as a proposition. Proved below as binNatInduction by the manual recursor transfer across Num ≃ ℕ.

Equations

• Transfer.PeanoBinNat.BinNatInductionTarget = ∀ (P : Num → Prop), P 0 → (∀ (n : Num), P n → P (n + 1)) → ∀ (n : Num), P n

theorem Transfer.PeanoBinNat.num_ofNat'_succ (k : ℕ) : Num.ofNat' (k + 1) = Num.ofNat' k + 1

Round-trip helper: Num.ofNat' (the ℕ → Num decoder) maps through successor, Num.ofNat' (k+1) = Num.ofNat' k + 1. Via Num.ofNat'_eq (Num.ofNat' n = ↑n) this is Nat.cast-of-successor in Num.

theorem Transfer.PeanoBinNat.binNatInduction : BinNatInductionTarget