[Merged by Bors] - feat: term elaborator for associativity equivalences between iterated products. #8551
Conversation
adamtopaz
added
WIP
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
There was a problem hiding this comment.
Something that occurred to me is that we could have probably used the coherence theorem for monoidal categories and the coherence tactic to do all this "for free" (you're using List to strictify the products after all 😄) but I believe you're generating much much better code, if this elaborator gets used in programming.
I don't see any obvious bugs, so let's just merge
bors r+
There's one suggested efficiency improvement, but the arrays involved are so small we'd probably not detect the difference, though it would make the code look cleaner. I figure it can be a follow-up.
|
|
||
| /-- 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 ProdTree.pack (ts : List Expr) : ProdTree → MetaM Expr |
There was a problem hiding this comment.
I believe you could make this take an Subarray Expr, which would save you needing to do these to-and-from-array conversions.
There was a problem hiding this comment.
Good idea! I'll implement this in a follow up PR.
leanprover-community-mathlib4-bot
added
ready-to-merge
… products. (#8551) For example, ```lean (prod_assoc% : (α × β) × (γ × δ) ≃ α × (β × γ) × δ) ``` gives the "obvious" equivalence between `(α × β) × (γ × δ)` and `α × (β × γ) × δ`. Special thanks to @kmill for help getting the expected type to work in the elaborator! Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
|
@kmill the coherence stuff would have worked great if all the types had the same universe level. This approach doesn't have such a restriction 😁 |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
… products. (#8551) For example, ```lean (prod_assoc% : (α × β) × (γ × δ) ≃ α × (β × γ) × δ) ``` gives the "obvious" equivalence between `(α × β) × (γ × δ)` and `α × (β × γ) × δ`. Special thanks to @kmill for help getting the expected type to work in the elaborator! Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
… products. (#8551) For example, ```lean (prod_assoc% : (α × β) × (γ × δ) ≃ α × (β × γ) × δ) ``` gives the "obvious" equivalence between `(α × β) × (γ × δ)` and `α × (β × γ) × δ`. Special thanks to @kmill for help getting the expected type to work in the elaborator! Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
For example,
gives the "obvious" equivalence between
(α × β) × (γ × δ)andα × (β × γ) × δ.Special thanks to @kmill for help getting the expected type to work in the elaborator!