LIPIcs.ITP.2024.41.pdf
- Filesize: 0.7 MB
- 8 pages
Document
Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper)
Author
Sam Ezeh 
-
Part of:
Volume:
15th International Conference on Interactive Theorem Proving (ITP 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-09-02
File
Document Identifiers
Author Details
Cite As Get BibTex
Sam Ezeh. Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 41:1-41:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.41
Abstract
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Interactive proof systems
- Human-centered computing → Graphical user interfaces
Keywords
- Interactive theorem proving
- Lean4
- Graphical User Interface
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
John Baez and Mike Stay. Physics, topology, logic and computation: a Rosetta Stone. Springer, 2011.
-
Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: an online proof assistant for higher-dimensional rewriting. Logical Methods in Computer Science, 14, 2018.
-
Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory ii: Rewriting with symmetric monoidal structure. Mathematical Structures in Computer Science, 32(4):511-541, 2022.
-
Cole Comfort, Antonin Delpeuch, and Jules Hedges. Sheet diagrams for bimonoidal categories. arXiv preprint arXiv:2010.13361, 2020.
-
Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary. homotopy.io: a proof assistant for finitely-presented globular n-categories. arXiv preprint arXiv:2402.13179, 2024.
-
Antonin Delpeuch and Jamie Vicary. Normalization for planar string diagrams and a quadratic equivalence algorithm. Logical Methods in Computer Science, 18, 2022.
- Sam Ezeh. Dignissimus/untangle: Graphical rewriting for diagrammatic reasoning in monoidal categories in lean4, 2024. Software (visited on 2024-08-19). URL: https://github.com/dignissimus/Untangle.
- André Joyal and Ross Street. The geometry of tensor calculus, i. Advances in Mathematics, 88(1):55-112, 1991. URL: https://doi.org/10.1016/0001-8708(91)90003-P.
-
Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning. In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 326-336. Springer, 2015.
-
Daniel Marsden. Category theory using string diagrams. arXiv preprint arXiv:1401.7220, 2014.
- Yuma Mizuno. Feat: String diagram widget by yuma-mizuno (pull request #10581) leanprover-community/mathlib4, February 2024. URL: https://github.com/leanprover-community/mathlib4/pull/10581.
-
Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28, pages 625-635, Cham, 2021. Springer International Publishing.
- Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An Extensible User Interface for Lean 4. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving (ITP 2023), volume 268 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:20, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.24.
-
Katherine Ye, Wode Ni, Max Krieger, Dor Ma'ayan, Jenna Wise, Jonathan Aldrich, Jonathan Sunshine, and Keenan Crane. Penrose: From mathematical notation to beautiful diagrams. ACM Trans. Graph., 39(4), 2020.