Factorial number system (xkcd 2835)

Stream: Is there code for X?

[Malvin Gattinger]

I was expecting someone would already have asked for this now: https://xkcd.com/2835/ - are those numbers in mathlib?
My very newbie attempt would be the following (sub)types, but I guess there is a more elegant way.

import tactic

def digit (n : ℕ) := subtype (λ k : ℕ, k ≤ n)

def factorial : Type := Σ N, Π n ≤ N, digit n

def zero : factorial :=
begin
  refine ⟨0,(λ k hyp, ⟨0,_⟩)⟩,
  omega,
end

def plusOne : factorial → factorial :=
begin
  intro f,
  cases f,
  sorry,
end

[Kyle Miller]

I don't see anything about factoriadics in mathlib or in the Zulip search.

[Kyle Miller]

A few thoughts:

• Instead of digit, you can use docs3#fin
• Using a sigma type like that means that numbers have multiple representations, which isn't great if you want equivalent numbers to be equal. An alternative is to define a structure where the first field is a dependent function Π n, fin (n + 1) and the second is the proposition that this function for large enough n is constant 0. Mathlib has the equivalent docs3#finsupp for setting this up in a slightly different way using finsets.
• Mathlib has been ported to Lean 4, so you might consider switching over to Lean 4 too :smile:

[Yaël Dillies]

Pretty sure I had a Lean 3 version at some point somewhere. I think it's a good exercise to work it out!

[Ruben Van de Velde]

Yaël, since you seem to have proofs for everything lying around, do you happen to have FLT hidden somewhere? :sweat_smile: