Encodable deriving handler

Adds a deriving handler for the Encodable class.

The resulting Encodable instance should be considered to be opaque. The specific encoding used is an implementation detail.

Theory

The idea is that every encodable inductive type can be represented as a tree of natural numbers. Inspiration for this is s-expressions used in Lisp/Scheme.

inductive S : Type where
  | nat (n : ℕ)
  | cons (a b : S)

We start by constructing an equivalence S ≃ ℕ using the Nat.pair function.

Here is an example of how this module constructs an encoding.

Suppose we are given the following type:

inductive T (α : Type) where
  | a (x : α) (y : Bool) (z : T α)
  | b

The deriving handler constructs the following declarations:

def encodableT_toS {α} [Encodable α] (x : T α) : S :=
  match x with
  | T.a a a_1 a_2 =>
    S.cons (S.nat 0)
      (S.cons (S.nat (Encodable.encode a))
        (S.cons (S.nat (Encodable.encode a_1)) (S.cons (encodableT_toS a_2) (S.nat 0))))
  | T.b => S.cons (S.nat 1) (S.nat 0)

private def encodableT_fromS {α} [Encodable α] : S → Option (T α) := fun
  | S.cons (S.nat 0) (S.cons (S.nat a) (S.cons (S.nat a_1) (S.cons a_2 (S.nat 0)))) =>
    match Encodable.decode a, Encodable.decode a_1, encodableT_fromS a_2 with
    | some a, some a_1, some a_2 => some <| T.a a a_1 a_2
    | _, _, _ => none
  | S.cons (S.nat 1) (S.nat 0) => some <| T.b
  | _ => none

private theorem encodableT {α} [Encodable α] (x : @T α) :
    encodableT_fromS (encodableT_toS x) = some x := by
  cases x <;> (unfold encodableT_toS encodableT_fromS; simp only [Encodable.encodek, encodableT])

instance {α} [Encodable α] : Encodable (@T α) :=
  Encodable.ofLeftInjection encodableT_toS encodableT_fromS encodableT

The idea is that each constructor gets encoded as a linked list made of S.cons constructors that is tagged with the constructor index.

Implementation

Constructing the toS encoding functions.

Constructing the fromS functions.

Constructing the proofs that the fromS functions are left inverses of the toS functions.

Assembling the Encodable instances.

def Mathlib.Deriving.Encodable.mkEncodableInstance (declNames : Array Lean.Name) : Lean.Elab.Command.CommandElabM Bool

The deriving handler for the Encodable 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.