We present Untangle, a Lean4 extension for Visual Studio Code that displays string diagrams for morphisms inside monoidal categories, allowing users to rewrite expressions by clicking on natural transformations and morphisms in the string diagram. When the the user manipulates the string diagram by clicking on natural transformations in the Graphical User Interface, it attempts to generate relevant tactics to apply which it then inserts into the editor, allowing the user to prove equalities visually by diagram rewriting.
@InProceedings{ezeh:LIPIcs.ITP.2024.41, author = {Ezeh, Sam}, title = {{Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {41:1--41:8}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.41}, URN = {urn:nbn:de:0030-drops-207690}, doi = {10.4230/LIPIcs.ITP.2024.41}, annote = {Keywords: Interactive theorem proving, Lean4, Graphical User Interface} }
Feedback for Dagstuhl Publishing