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

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

instance Lean.Expr.instReprProdTree : Repr Lean.Expr.ProdTree

Equations

• Lean.Expr.instReprProdTree = { reprPrec := Lean.Expr.reprProdTree✝ }

def Lean.Expr.ProdTree.getType : Lean.Expr.ProdTree → Lean.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 : Lean.Expr.ProdTree → ℕ

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 : Lean.Expr.ProdTree → List Lean.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 : Lean.Expr) : Lean.MetaM Lean.Expr.ProdTree

Make a ProdTree out of an Expr.

def Lean.Expr.ProdTree.unpack (t : Lean.Expr) : Lean.Expr.ProdTree → Lean.MetaM (List Lean.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 Lean.Expr) : Lean.Expr.ProdTree → Lean.MetaM Lean.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 : Lean.Expr.ProdTree) (e : Lean.Expr) : Lean.MetaM Lean.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 let __do_lift ← Lean.Expr.ProdTree.pack __do_lift P2 pure __do_lift

def Lean.Expr.mkProdFun (a b : Lean.Expr) : Lean.MetaM Lean.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 : Lean.Expr) : Lean.MetaM Lean.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 : Lean.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 : Lean.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%» : Lean.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%")