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 α × (β × γ) × δ
.
A helper type to keep track of universe levels and types in iterated produts.
- type: Lean.Expr → Lean.Level → Lean.Expr.ProdTree
- prod: Lean.Expr.ProdTree → Lean.Expr.ProdTree → Lean.Level → Lean.Level → Lean.Expr.ProdTree
Instances For
Equations
- Lean.Expr.instReprProdTree = { reprPrec := Lean.Expr.reprProdTree✝ }
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]
Instances For
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
Instances For
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
Instances For
Make a ProdTree
out of an 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]
Instances For
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.")
Instances For
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
Instances For
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.
Instances For
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.
Instances For
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%")
Instances For
Elaborator for prod_assoc%
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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%")