Countable deriving handler

Adds a deriving handler for the Countable class.

Theory

We use the Nat.pair function to encode an inductive type in the natural numbers, following a pattern similar to the tagged s-expressions used in Scheme/Lisp. We develop a little theory to make constructing the injectivity functions very straightforward.

This is easiest to explain by example. Given a type

inductive T (α : Type)
  | a (n : α)
  | b (n m : α) (t : T α)

the deriving handler constructs the following three declarations:

noncomputable def T.toNat (α : Type) [Countable α] : T α → ℕ
  | a n => Nat.pair 0 (Nat.pair (encode n) 0)
  | b n m t => Nat.pair 1 (Nat.pair (encode n) (Nat.pair (encode m) (Nat.pair t.toNat 0)))

theorem T.toNat_injective (α : Type) [Countable α] : Function.Injective (T.toNat α) := fun
  | a .., a .. => by
    refine cons_eq_imp_init ?_
    refine pair_encode_step ?_; rintro ⟨⟩
    intro; rfl
  | a .., b .. => by refine cons_eq_imp ?_; rintro ⟨⟩
  | b .., a .. => by refine cons_eq_imp ?_; rintro ⟨⟩
  | b .., b .. => by
    refine cons_eq_imp_init ?_
    refine pair_encode_step ?_; rintro ⟨⟩
    refine pair_encode_step ?_; rintro ⟨⟩
    refine cons_eq_imp ?_; intro h; cases T.toNat_injective α h
    intro; rfl

instance (α : Type) [Countable α] : Countable (T α) := ⟨_, T.toNat_injective α⟩

Implementation

Constructing the toNat functions.

def Mathlib.Deriving.Countable.mkToNatFuns (ctx : Lean.Elab.Deriving.Context) (toNatFnNames : Array Lean.Name) : Lean.Elab.TermElabM (Lean.TSyntax `command)

Constructs a function from the inductive type to Nat.

Equations

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

Constructing the injectivity proofs for these toNat functions.

def Mathlib.Deriving.Countable.mkInjThms (ctx : Lean.Elab.Deriving.Context) (toNatFnNames : Array Lean.Name) : Lean.Elab.TermElabM (Lean.TSyntax `command)

Constructs a proof that the functions created by mkToNatFuns are injective.

Equations

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

Assembling the Countable instances.

def Mathlib.Deriving.Countable.mkCountableInstance (declNames : Array Lean.Name) : Lean.Elab.Command.CommandElabM Bool

The deriving handler for the Countable class. Handles non-nested non-reflexive inductive types. They can be mutual too — in that case, there is an optimization to re-use all the generated functions and proofs.

Equations

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