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 α⟩

noncomputable def Mathlib.Deriving.Countable.encode {α : Sort u_1} [Countable α] : α → ℕ

Encode a Countable type into the natural numbers using the witness produced by Countable.exists_injective_nat. Used internally by the Countable deriving handler.

Equations

• Mathlib.Deriving.Countable.encode = ⋯.choose

theorem Mathlib.Deriving.Countable.encode_injective {α : Sort u_1} [Countable α] : Function.Injective encode

The encode function is injective. Used internally by the Countable deriving handler.

theorem Mathlib.Deriving.Countable.cons_eq_imp_init {p : Prop} {a b b' : ℕ} (h : b = b' → p) : Nat.pair a b = Nat.pair a b' → p

Initialize the injectivity argument. Pops the constructor tag.

theorem Mathlib.Deriving.Countable.cons_eq_imp {p : Prop} {a b a' b' : ℕ} (h : a = a' → b = b' → p) : Nat.pair a b = Nat.pair a' b' → p

Generic step of the injectivity argument, pops the head of the pairs. Used in the recursive steps where we need to supply an additional injectivity argument.

theorem Mathlib.Deriving.Countable.pair_encode_step {p : Prop} {α : Sort u_1} [Countable α] {a b : α} {m n : ℕ} (h : a = b → m = n → p) : Nat.pair (encode a) m = Nat.pair (encode b) n → p

Specialized step of the injectivity argument, pops the head of the pairs and decodes.

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.