Generating "proxy types"

This module gives tools to create an equivalence between a given inductive type and a "proxy type" constructed from Unit, PLift, Sigma, Empty, and Sum. It works for any non-recursive inductive type without indices.

The intended use case is for pulling typeclass instances across this equivalence. This reduces the problem of generating typeclass instances to that of writing typeclass instances for the above five types (and whichever additional types appear in the inductive type).

The main interface is the proxy_equiv% elaborator, where proxy_equiv% t gives an equivalence between the proxy type for t and t. See the documentation for proxy_equiv% for an example.

For debugging information, do set_option Elab.ProxyType true.

It is possible to reconfigure the machinery to generate other types. See ensureProxyEquiv and look at how it is used in proxy_equiv%.

Implementation notes

For inductive types with n constructors, the proxy_equiv% elaborator creates a proxy type of the form C₁ ⊕ (C₂ ⊕ (⋯ ⊕ Cₙ)). The equivalence then needs to handle n - 1 levels of Sum constructors, which is a source of quadratic complexity.

An alternative design could be to generate a C : Fin n → Type* function for the proxy types for each constructor and then use (i : Fin n) × ULift (C i) for the total proxy type. However, typeclass inference is not good at finding instances for such a type even if there are instances for each C i. One seems to need to add, for example, an explicit [∀ i, Fintype (C i)] instance given ∀ i, Fintype (C i).

structure Mathlib.ProxyType.ProxyEquivConfig : Type

Configuration used by mkProxyEquiv.

• proxyName : Lean.Name

  Name to use for the declaration for a type that is Equiv to the given type.

• proxyEquivName : Lean.Name

  Name to use for the declaration for the equivalence proxyType ≃ type.

• mkCtorProxyType : List (Lean.Expr × Lean.Name) → Lean.Elab.TermElabM (Lean.Expr × Lean.Term)

  Returns a proxy type for a constructor and a pattern to use to match against it, given a list of fvars for the constructor arguments and pattern names to use for the arguments. The proxy type is expected to be a Type*.

• mkProxyType : Array (Lean.Name × Lean.Expr × Lean.Term) → Lean.Elab.TermElabM (Lean.Expr × Array Lean.Term × Lean.TSyntax `tactic)

  Given (constructor name, proxy constructor type, proxy constructor pattern) triples constructed using mkCtorProxyType, return (1) the total proxy type (a Type*), (2) patterns to use for each constructor, and (3) a proof to use to prove left_inv for proxy_type ≃ type (this proof starts with intro x).

def Mathlib.ProxyType.defaultMkCtorProxyType (xs : List (Lean.Expr × Lean.Name)) (decorateSigma : Lean.Expr → Lean.Elab.TermElabM Lean.Expr := pure) : Lean.Elab.TermElabM (Lean.Expr × Lean.Term)

Returns a proxy type for a constructor and a pattern to use to match against it.

Input: a list of pairs associated to each argument of the constructor consisting of (1) an fvar for this argument and (2) a name to use for this argument in patterns.

For example, given #[(a, x), (b, y)] with x : Nat and y : Fin x, then this function returns Sigma (fun x => Fin x) and ⟨a, b⟩.

Always returns a Type*. Uses Unit, PLift, and Sigma. Avoids using PSigma since the Fintype instances for it go through Sigmas anyway.

The decorateSigma function is to wrap the Sigma a decorator such as Lex. It should yield a definitionally equal type.

def Mathlib.ProxyType.defaultMkProxyType (ctors : Array (Lean.Name × Lean.Expr × Lean.Term)) (decorateSum : Lean.Expr → Lean.Elab.TermElabM Lean.Expr := pure) : Lean.Elab.TermElabM (Lean.Expr × Array Lean.Term × Lean.TSyntax `tactic)

Create a Sum of types, mildly optimized to not have a trailing Empty.

The decorateSum function is to wrap the Sum with a function such as Lex. It should yield a definitionally equal type.

def Mathlib.ProxyType.ProxyEquivConfig.default (indVal : Lean.InductiveVal) : ProxyEquivConfig

Default configuration. Defines proxyType and proxyTypeEquiv in the namespace of the inductive type. Uses Unit, PLift, Sigma, Empty, and Sum.

def Mathlib.ProxyType.ensureProxyEquiv (config : ProxyEquivConfig) (indVal : Lean.InductiveVal) : Lean.Elab.TermElabM Unit

Generates a proxy type for the inductive type and an equivalence from the proxy type to the type.

If the declarations already exist, there is a check that they are correct.

def Mathlib.ProxyType.elabProxyEquiv (type : Lean.Term) (expectedType? : Option Lean.Expr) : Lean.Elab.TermElabM (Lean.Expr × Lean.InductiveVal)

Helper function for proxy_equiv% type : expectedType elaborators.

Elaborate type and get its InductiveVal. Uses the expectedType, where the expected type should be of the form _ ≃ type.

def Mathlib.ProxyType.proxy_equiv : Lean.ParserDescr

The term elaborator proxy_equiv% α for a type α elaborates to an equivalence β ≃ α for a "proxy type" β composed out of basic type constructors Unit, PLift, Sigma, Empty, and Sum.

This only works for inductive types α that are neither recursive nor have indices. If α is an inductive type with name I, then as a side effect this elaborator defines I.proxyType and I.proxyTypeEquiv.

The elaborator makes use of the expected type, so (proxy_equiv% _ : _ ≃ α) works.

For example, given this inductive type

inductive foo (n : Nat) (α : Type)
  | a
  | b : Bool → foo n α
  | c (x : Fin n) : Fin x → foo n α
  | d : Bool → α → foo n α

the proxy type it generates is Unit ⊕ Bool ⊕ (x : Fin n) × Fin x ⊕ (_ : Bool) × α and in particular we have that

proxy_equiv% (foo n α) : Unit ⊕ Bool ⊕ (x : Fin n) × Fin x ⊕ (_ : Bool) × α ≃ foo n α

def Mathlib.ProxyType.elab_proxy_equiv : Lean.Elab.Term.TermElab

Elaborator for proxy_equiv%.