Counting Types with Lean

FiniteTypes.Lean

import MIL.Common
import Mathlib.Data.Nat.Pairing

--  Let's define a type that represents all finite types
--  Taken from (A Universe of Finite Types - Functional Programming in Lean)
--    https://lean-lang.org/functional_programming_in_lean/dependent-types/universe-pattern.html
inductive FiniteType where
  | unit : FiniteType
  | bool : FiniteType
  | pair : FiniteType → FiniteType → FiniteType
  | arr : FiniteType → FiniteType → FiniteType
  deriving Repr, BEq

-- Let's create a constructor to the space of all finite types
-- by mapping the natural numbers to finite types
def Nat.toFiniteT: Nat → FiniteType
  | 0 => FiniteType.unit
  | 1 => FiniteType.bool
  | n + 2 =>
      let t := n % 2
      let np := n / 2
      let p := Nat.unpair np   --  See:  https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Nat/Pairing.lean
      let a := p.1
      let b := p.2
      have h1 : a < n + 2 := by sorry -- TODO: Prove this
      have h2 : b < n + 2 := sorry    -- TODO: Prove this
      let a := toFiniteT a
      let b := toFiniteT b
      if t == 0 then FiniteType.pair a b else FiniteType.arr a b
  termination_by toFiniteT n => n

#eval Nat.toFiniteT 0  -- unit
#eval Nat.toFiniteT 1  -- bool
#eval Nat.toFiniteT 2  -- pair unit unit
#eval Nat.toFiniteT 25 -- arr (pair (unit) (unit))
                       --     (arr (unit) (unit))

--  Let's define a function that converts the finite type t
--  to it's orignal natural number
def FiniteType.toNat : FiniteType → Nat :=
  fun f => match f with
  | FiniteType.unit => 0
  | FiniteType.bool => 1
  | FiniteType.pair a b =>
      let a := a.toNat
      let b := b.toNat
      let z := Nat.pair a b   --  See:  https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Nat/Pairing.lean
      2 * z + 2
  | FiniteType.arr a b =>
      let a := a.toNat
      let b := b.toNat
      let z := Nat.pair a b
      2 * z + 3

#eval (FiniteType.arr
  (FiniteType.pair (FiniteType.unit) (FiniteType.unit))
  (FiniteType.arr (FiniteType.unit) (FiniteType.unit))).toNat -- 25


--  Now, let's define a function that converts a finite type to an actual type
abbrev FiniteType.toType : FiniteType → Type
  | FiniteType.unit => Unit
  | FiniteType.bool => Bool
  | FiniteType.pair a b => (FiniteType.toType a × FiniteType.toType b)
  | FiniteType.arr a b => (FiniteType.toType a → FiniteType.toType b)

--  Let's create a constructor that converts a natural number to a type
abbrev TypeNum (n: Nat) := (n.toFiniteT).toType

-- Definitions in Lean are of the form
-- def <id> : <type> := <value>
def ex1 : Unit → Bool := fun () => true

-- Like Count von Count, but with types
def t0 : TypeNum 0 := ()             -- Unit, Ah ah ah
def t1 : TypeNum 1 := false          -- Bool, Ah ah ah
def t2 : TypeNum 2 := ((), ())       -- Unit × Unit, Ah ah ah
def t3 : TypeNum 3 := fun () => ()   -- Unit → Unit, Ah ah ah
def t4 : TypeNum 4 := ((), true)     -- Unit × Bool, Ah ah ah
def t5 : TypeNum 5 := fun () => true -- Unit → Bool, Ah ah ah