# 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)`

.

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`

. 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`

).

## Instances For

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 `Sigma`

s anyway.

The `decorateSigma`

function is to wrap the `Sigma`

a decorator such as `Lex`

.
It should yield a definitionally equal type.

## Equations

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

## Instances For

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.

## Equations

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

## Instances For

Construct the `Sum`

expression, using `decorateSum`

to adjust each `Sum`

.

## Equations

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

## Instances For

Navigates into the sum type that we create in `mkCType`

for the given constructor index.

## Equations

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

## Instances For

Default configuration. Defines `proxyType`

and `proxyTypeEquiv`

in the namespace
of the inductive type. Uses `Unit`

, `PLift`

, `Sigma`

, `Empty`

, and `Sum`

.

## Equations

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

## Instances For

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.

## Equations

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

## Instances For

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`

.

## Equations

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

## Instances For

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

## Equations

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

## Instances For

Elaborator for `proxy_equiv%`

.

## Equations

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