Structural Recursion for ToString Instance

Stream: new members

[Mark Fischer]

As a sort fun exercise, I thought I'd try to work my way through the Natural Numbers Game, but rather than use Peano's Axioms, I'd try it with a base-two representation. I pretty much got myself stuck immediately when trying to define a ToString instance for my new inductive type.

I suspect that I'm just not familiar enough with Lean.

namespace NatB

inductive ℕb where
  | One: ℕb
  | T2: ℕb → ℕb
  | P1: ℕb → ℕb

inductive ℕ where
  | Zero: ℕ
  | Binary: ℕb → ℕ

instance : ToString ℕb where
  toString: ℕb → String
    | ℕb.One => "1"
    | ℕb.T2 n => s!"{n}0"
    | ℕb.P1 n => s!"{n}1"

instance : ToString ℕ where
  toString: ℕ → String
    | ℕ.Zero => "0"
    | ℕ.Binary n => s!"{n}"

end NatB

The Error I get is that I failed to synthesize instance ToString ℕb. I feel like I'm missing something simple.

[Kyle Miller]

You can make a separate def first and then use it to make the instance

[Kevin Buzzard]

ha ha I have also done this exercise :-) You'll want

instance foo : ToString ℕb where
  toString: ℕb → String
    | ℕb.One => "1"
    | ℕb.T2 n => -- something involving `foo`

[Kevin Buzzard]

PS associativity of addition is fun :-) The game becomes impossible after some point -- e.g. associativity of multiplication. The way I did it was that I proved a bijection between binary nat and unary nat, and transported the proof over.

[Mark Fischer]

Ah, that for the tip! very helpful :)

[Kyle Miller]

@Kevin Buzzard I might have slipped in before you (hence the :racecar:) but your solution ends up being a bit different. The compiler will inline your definition wherever toString is used, but if you split out a separate def then it won't (or rather it won't unfold the body of that definition).

[Mark Fischer]

Kevin Buzzard said:

PS associativity of addition is fun :-) The game becomes impossible after some point -- e.g. associativity of multiplication. The way I did it was that I proved a bijection between binary nat and unary nat, and transported the proof over.

This feels surprising to me! I suppose I'll get there soon enough but somehow my intuition was that the representation would convolute things but not preclude any of the proofs possible with the unary representation. Though I suppose transporting proofs sort of makes that intuition hold. I'm sure I'll learn something in the attempt!

[Kevin Buzzard]

I have seen textbooks which define the reals to be decimal expansions that don't end in ...999999... and I used to think that this was a feasible definition which makes the least upper bound axiom easy to prove, but now I'm extremely skeptical about whether this is feasible because of issues like associativity of multiplication (which for decimals will be much worse than binary naturals). You don't have to biject with the unary naturals, the thing which you really find you need (or at least I found I needed) is the usual induction principle, which you can attempt to prove for binary nats directly.

[Kevin Buzzard]

The bottom line is that if you're trying to prove a statement about (possibly several) binary naturals via the induction principle that comes with them, then you can't always get from knowing it for a to knowing it for 2a+1 because +1 might not cancel and you might end up with needing some auxiliary fact for x+1 and only having it for x: "+1" is not a primitive operation for binary naturals.

[Kevin Buzzard]

By the way, when I did it I didn't add zero until much later: binary naturals naturally start at 1 and you can develop the NNG theory for these instead -- the "British natural numbers".

[Yakov Pechersky]

https://www.sciencedirect.com/science/article/pii/138572587690055X

[Yakov Pechersky]

branch#de-brujin-reals-no-rationals

[Yakov Pechersky]

I'm in the middle of section 12, everything beforehand is proven

[Yakov Pechersky]

We'll see how the multiplication part goes :)

[Kevin Buzzard]

Whilst de Bruijn spends several pages on addition, he says (in section 9) "the prospects of introducing multiplication and division by their algorithms do not seem to be very good at this point" and his sketch (just 10 or so lines) of another approach can perhaps be interpreted as "I don't know how to do associativity of multiplication on binary naturals directly".

[Mario Carneiro]

Note that mathlib plays the binary natural number game in file#Mathlib/Data/Num/Lemmas

[Mario Carneiro]

but it also "cheats" and uses transfer from Nat to prove mul_assoc

[Mario Carneiro]

Coq also plays the binary natural number game, I'll go see what they did

[Mario Carneiro]

Ha! They kind of also "cheat", but in a slightly different way: they prove that binary natural numbers satisfy the unary natural induction principle and then prove mul_assoc that way. (In fact they prove hundreds of theorems this way, by using Coq modules to describe the property of "looking like Nat" and then proving a bunch of theorems about them, then instantiating both binary and unary naturals using this module)

[Kevin Buzzard]

Right, those are the two ways I know. I'll leave it to Yakov to explain the third way (I don't know if the techniques in section 14 of the de Bruijn paper will work for naturals)

[Yakov Pechersky]

The de Bruijn paper also uses unary induction:
image.png
image.png

[Yakov Pechersky]

Where the induction is more of a Z (Integer) like, over some base.

[Mario Carneiro]

it does sound like an interesting challenge though

[Mark Fischer]

Mario Carneiro said:

prove that binary natural numbers satisfy the unary natural induction principle

Because induction is implemented in terms of recursion, does this look a bit like moving from structural recursion to well-founded recursion by proving something like that predecessor is a well founded recursive relation?

[Mario Carneiro]

I think the core of it is the fact that you can construct a Nat from a Num, in fact an exponentially larger one, which is done by iterating the 2*n and 2*n+1 functions on Nat (which are themselves defined by recursion on Nat)

[Mario Carneiro]

that gives you a very large element of an inductive type which you can then use to power the induction down to zero using binary successor

[Mario Carneiro]

which shows that every element of Num is accessible by applying enough binary successors to zero

[Mario Carneiro]

There is surely a way to recast that proof such that it doesn't use the type Nat directly