Associativity of products

This file constructs a term elaborator for "obvious" equivalences between iterated products. For example,

(prod_assoc% : (α × β) × (γ × δ) ≃ α × (β × γ) × δ)

gives the "obvious" equivalence between (α × β) × (γ × δ) and α × (β × γ) × δ.

inductive Lean.Expr.ProdTree : Type

A helper type to keep track of universe levels and types in iterated products.

• type (tp : Expr) (l : Level) : ProdTree
• prod (fst snd : ProdTree) (lfst lsnd : Level) : ProdTree

instance Lean.Expr.instReprProdTree : Repr ProdTree

def Lean.Expr.ProdTree.getType : ProdTree → Expr

The iterated product corresponding to a ProdTree.

def Lean.Expr.ProdTree.size : ProdTree → ℕ

The number of types appearing in an iterated product encoded as a ProdTree.

def Lean.Expr.ProdTree.components : ProdTree → List Expr

The components of an iterated product, presented as a ProdTree.

partial def Lean.Expr.mkProdTree (e : Expr) : MetaM ProdTree

Make a ProdTree out of an Expr.

def Lean.Expr.ProdTree.unpack (t : Expr) : ProdTree → MetaM (List Expr)

Given P : ProdTree representing an iterated product and e : Expr which should correspond to a term of the iterated product, this will return a list, whose items correspond to the leaves of P (i.e. the types appearing in the product), where each item is the appropriate composition of Prod.fst and Prod.snd applied to e resulting in an element of the type corresponding to the leaf.

For example, if P corresponds to (X × Y) × Z and t : (X × Y) × Z, then this should return [t.fst.fst, t.fst.snd, t.snd].

def Lean.Expr.ProdTree.pack (ts : List Expr) : ProdTree → MetaM Expr

This function should act as the "reverse" of ProdTree.unpack, constructing a term of the iterated product out of a list of terms of the types appearing in the product.

def Lean.Expr.ProdTree.convertTo (P1 P2 : ProdTree) (e : Expr) : MetaM Expr

Converts a term e in an iterated product P1 into a term of an iterated product P2. Here e is an Expr representing the term, and the iterated products are represented by terms of ProdTree.

def Lean.Expr.mkProdFun (a b : Expr) : MetaM Expr

Given two expressions corresponding to iterated products of the same types, associated in possibly different ways, this constructs the "obvious" function from one to the other.

def Lean.Expr.mkProdEquiv (a b : Expr) : MetaM Expr

Construct the equivalence between iterated products of the same type, associated in possibly different ways.

def Lean.Expr.prodAssocStx : ParserDescr

IMPLEMENTATION: Syntax used in the implementation of prod_assoc%. This elaborator postpones if there are metavariables in the expected type, and to propagate the fact that this elaborator produces an Equiv, the prod_assoc% macro sets things up with a type ascription. This enables using prod_assoc% with, for example Equiv.trans dot notation.

def Lean.Expr.elabProdAssoc : Elab.Term.TermElab

Elaborator for prod_assoc%.

def Lean.Expr.«termProd_assoc%» : ParserDescr

prod_assoc% elaborates to the "obvious" equivalence between iterated products of types, regardless of how the products are parenthesized. The prod_assoc% term uses the expected type when elaborating. For example, (prod_assoc% : (α × β) × (γ × δ) ≃ α × (β × γ) × δ).

The elaborator can handle holes in the expected type, so long as they eventually get filled by unification.

example : (α × β) × (γ × δ) ≃ α × (β × γ) × δ :=
  (prod_assoc% : _ ≃ α × β × γ × δ).trans prod_assoc%