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

def Lean.Expr.instReprProdTree.repr : ProdTree → Nat → Format

Equations

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

@[implicit_reducible]

instance Lean.Expr.instReprProdTree : Repr ProdTree

Equations

• Lean.Expr.instReprProdTree = { reprPrec := Lean.Expr.instReprProdTree.repr }

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

The iterated product corresponding to a ProdTree.

Equations

• (Lean.Expr.ProdTree.type a a_1).getType = a
• (a.prod a_1 a_2 a_3).getType = Lean.mkAppN (Lean.Expr.const `Prod [a_2, a_3]) #[a.getType, a_1.getType]

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

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

Equations

• (Lean.Expr.ProdTree.type a a_1).size = 1
• (a.prod a_1 a_2 a_3).size = a.size + a_1.size

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

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

Equations

• (Lean.Expr.ProdTree.type a a_1).components = [a]
• (a.prod a_1 a_2 a_3).components = a.components ++ a_1.components

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Expr.ProdTree.unpack t (Lean.Expr.ProdTree.type a a_1) = pure [t]

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.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Expr.ProdTree.pack [] (Lean.Expr.ProdTree.type a a_1) = Lean.throwError (Lean.toMessageData "Can't pack the empty list.")
• Lean.Expr.ProdTree.pack [a_2] (Lean.Expr.ProdTree.type a a_1) = pure a_2
• Lean.Expr.ProdTree.pack ts (Lean.Expr.ProdTree.type a a_1) = Lean.throwError (Lean.toMessageData "Failed due to size mismatch.")

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.

Equations

• P1.convertTo P2 e = do let __do_lift ← Lean.Expr.ProdTree.unpack e P1 Lean.Expr.ProdTree.pack __do_lift P2

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.

Equations

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

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

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

Equations

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

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.

Equations

• Lean.Expr.prodAssocStx = Lean.ParserDescr.node `Lean.Expr.prodAssocStx 1024 (Lean.ParserDescr.symbol "prod_assoc_internal%")

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

Elaborator for prod_assoc%.

Equations

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

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%

Equations

• Lean.Expr.«termProd_assoc%» = Lean.ParserDescr.node `Lean.Expr.«termProd_assoc%» 1024 (Lean.ParserDescr.symbol "prod_assoc%")