Document Open Access Logo

An Extensible User Interface for Lean 4

Authors Wojciech Nawrocki , Edward W. Ayers , Gabriel Ebner

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.24.pdf
  • Filesize: 1.46 MB
  • 20 pages

Document Identifiers

Author Details

Wojciech Nawrocki
  • Carnegie Mellon University, Pittsburgh, PA, USA
Edward W. Ayers
  • Carnegie Mellon University, Pittsburgh, PA, USA
Gabriel Ebner
  • Microsoft Research, Redmond, WA, USA

Funding

  • Nawrocki, Wojciech: Hoskinson Center for Formal Mathematics.
  • Ayers, Edward W.: Hoskinson Center for Formal Mathematics.

Acknowledgements

The Lean team at MSR and KIT: Leonardo de Moura and Sebastian Ullrich for extensive discussions, code review, and improvements to the system, Daniel Selsam for suggesting traces, and Daniel Fabian for input on RPC design. The Penrose team: Wode Ni and Sam Estep for considerable help and implementing several features which made our use possible. Jeremy Avigad and Patrick Massot for suggestions, advice, and feedback on a draft of the paper. Tomáš Skřivan, Joachim Breitner, and Sina Hazratpour for trying our systems and suggesting improvements. Chris Lovett and Mariana Alanis for working on vscode-lean4. The Lean Zulip community for technical help and ideas.

Cite AsGet BibTex

Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An Extensible User Interface for Lean 4. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.24

Abstract

Contemporary proof assistants rely on complex automation and process libraries with millions of lines of code. At these scales, understanding the emergent interactions between components can be a serious challenge. One way of managing complexity, long established in informal practice, is through varying external representations. For instance, algebraic notation facilitates term-based reasoning whereas geometric diagrams invoke spatial intuition. Objects viewed one way become much simpler than when viewed differently. In contrast, modern general-purpose ITP systems usually only support limited, textual representations. Treating this as a problem of human-computer interaction, we aim to demonstrate that presentations - UI elements that store references to the objects they are displaying - are a fruitful way of thinking about ITP interface design. They allow us to make headway on two fronts - introspection of prover internals and support for diagrammatic reasoning. To this end we have built an extensible user interface for the Lean 4 prover with an associated ProofWidgets 4 library of presentation-based UI components. We demonstrate the system with several examples including type information popups, structured traces, contextual suggestions, a display for algebraic reasoning, and visualizations of red-black trees. Our interface is already part of the core Lean distribution.

Subject Classification

ACM Subject Classification
  • Human-centered computing → Visualization systems and tools
  • Software and its engineering → Functional languages
Keywords
  • user interfaces
  • human-computer interaction
  • Lean

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich. Deductive Software Verification - The KeY Book. Lecture Notes in Computer Science. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-49812-6.
  2. Ahmed Amerkad, Yves Bertot, Loïc Pottier, and Laurence Rideau. Mathematics and Proof Presentation in Pcoq. Technical Report RR-4313, INRIA, November 2001. URL: https://hal.inria.fr/inria-00072274.
  3. Emilio Jesús Gallego Arias, Benoît Pin, and Pierre Jouvelot. jscoq: Towards hybrid theorem proving interfaces. In Serge Autexier and Pedro Quaresma, editors, Proceedings of the 12th Workshop on User Interfaces for Theorem Provers, UITP 2016, Coimbra, Portugal, 2nd July 2016, volume 239 of EPTCS, pages 15-27, 2016. URL: https://doi.org/10.4204/EPTCS.239.2.
  4. David Aspinall. Proof general: A generic tool for proof development. In Susanne Graf and Michael I. Schwartzbach, editors, International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 1785 of Lecture Notes in Computer Science, pages 38-43. Springer, Springer, 2000. URL: https://doi.org/10.1007/3-540-46419-0_3.
  5. Edward W. Ayers, Mateja Jamnik, and William T. Gowers. A graphical user interface framework for formal verification. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), volume 193 of LIPIcs, pages 4:1-4:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.4.
  6. Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: an online proof assistant for higher-dimensional rewriting. In Leibniz International Proceedings in Informatics, volume 52, pages 34:1-34:11, 2016. URL: http://ncatlab.org/nlab/show/Globular.
  7. Jon Barwise and John Etchemendy. Hyperproof: Logical reasoning with diagrams. In Working Notes of the AAAI Spring Symposium on Reasoning with Diagrammatic Representations, 1992. URL: https://www.aaai.org/Papers/Symposia/Spring/1992/SS-92-02/SS92-02-016.pdf.
  8. Yves Bertot. The ctcoq system: Design and architecture. Formal Aspects Comput., 11(3):225-243, 1999. URL: https://doi.org/10.1007/s001650050049.
  9. Yves Bertot, Frédérique Guilhot, and Loic Pottier. Visualizing geometrical statements with geoview. In David Aspinall and Christoph Lüth, editors, Proceedings of the User Interfaces for Theorem Provers Workshop, UITP@TPHOLs 2003, Rome, Italy, September 8, 2003, volume 103 of Electronic Notes in Theoretical Computer Science, pages 49-65. Elsevier, 2003. URL: https://doi.org/10.1016/j.entcs.2004.09.013.
  10. Yves Bertot, Gilles Kahn, and Laurent Théry. Proof by pointing. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings, volume 789 of Lecture Notes in Computer Science, pages 141-160. Springer, 1994. URL: https://doi.org/10.1007/3-540-57887-0_94.
  11. Yves Bertot and Laurent Théry. A generic approach to building user interfaces for theorem provers. J. Symb. Comput., 25(2):161-194, 1998. URL: https://doi.org/10.1006/jsco.1997.0171.
  12. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending sledgehammer with SMT solvers. J. Autom. Reason., 51(1):109-128, 2013. URL: https://doi.org/10.1007/s10817-013-9278-5.
  13. R. Braden. Requirements for internet hosts - communication layers. RFC 1122, RFC Editor, October 1989. URL: https://www.rfc-editor.org/rfc/rfc1122.txt.
  14. Joachim Breitner. Visual theorem proving with the incredible proof machine. In Jasmin Christian Blanchette and Stephan Merz, editors, International Conference on Interactive Theorem Proving, pages 123-139. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-43144-4_8.
  15. Niklas Bülow. Proof visualization for the lean 4 theorem prover, April 2022. Google Scholar
  16. David Christiansen, David Darais, and Weixi Ma. The final pretty printer, 2016. URL: https://web.archive.org/web/20230219222209/https://davidchristiansen.dk/drafts/final-pretty-printer-draft.pdf.
  17. Eugene Charles Ciccarelli. Presentation based user interfaces. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1984. URL: https://hdl.handle.net/1721.1/15346.
  18. Bob Coecke and Ross Duncan. Interacting quantum observables. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II - Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations, volume 5126 of Lecture Notes in Computer Science, pages 298-310. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70583-3_25.
  19. 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 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 625-635. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  20. Silvia de Toffoli. Chasing the diagram-the use of visualizations in algebraic reasoning. Review of Symbolic Logic, 10(1):158-186, 2017. URL: https://doi.org/10.1017/s1755020316000277.
  21. R.A. Dean. Elements of Abstract Algebra. Wiley international edition. Wiley, 1966. URL: https://books.google.com/books?id=kmulxmBgkxoC.
  22. Pablo Donato, Pierre-Yves Strub, and Benjamin Werner. A drag-and-drop proof tactic. In Andrei Popescu and Steve Zdancewic, editors, CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pages 197-209. ACM, 2022. URL: https://doi.org/10.1145/3497775.3503692.
  23. Douglas C. Engelbart. Augmenting human intellect: A conceptual framework. Technical report, Stanford Research Institute, October 1962. URL: https://web.archive.org/web/20230220110343/https://dougengelbart.org/pubs/augment-3906.html.
  24. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, CADE, volume 9195 of LNCS, pages 527-538. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_36.
  25. Adele Goldberg. Smalltalk-80 - the interactive programming environment. Addison-Wesley, 1984. Google Scholar
  26. André Joyal and Ross Street. The geometry of tensor calculus, i. Advances in mathematics, 88(1):55-112, 1991. Google Scholar
  27. Joomy Korkut and David Thrane Christiansen. Extensible type-directed editing. In Richard A. Eisenberg and Niki Vazou, editors, Proceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2018, St. Louis, MO, USA, September 27, 2018, pages 38-50. ACM, 2018. URL: https://doi.org/10.1145/3240719.3241791.
  28. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving. CoRR, abs/2205.11491, 2022. URL: https://doi.org/10.48550/arXiv.2205.11491.
  29. Jill H. Larkin and Herbert A. Simon. Why a diagram is (sometimes) worth ten thousand words. Cognitive Science, 11(1):65-100, 1987. URL: https://doi.org/10.1111/j.1551-6708.1987.tb00863.x.
  30. Helen Lowe and David Duncan. Xbarnacle: Making theorem provers more accessible. In William McCune, editor, Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings, volume 1249 of Lecture Notes in Computer Science, pages 404-407. Springer, 1997. URL: https://doi.org/10.1007/3-540-63104-6_39.
  31. Zhaohui Luo and Robert Pollack. Lego proof development system: User’s manual. Technical report, LFCS, Edinburgh University, 1992. URL: https://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-211/.
  32. Christoph Lüth and Martin Ring. A web interface for isabelle: The next generation. In Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, and Wolfgang Windsteiger, editors, Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings, volume 7961 of Lecture Notes in Computer Science, pages 326-329. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39320-4_22.
  33. Hannes Mehnert and David Christiansen. Tool demonstration: An ide for programming and proving in idris, 2014. URL: https://davidchristiansen.dk/pubs/dtp2014-idris-mode.pdf.
  34. Guillaume Melquiond. Plotting in a formally verified way. In José Proença and Andrei Paskevich, editors, Proceedings of the 6th Workshop on Formal Integrated Development Environment, F-IDE@NFM 2021, Held online, 24-25th May 2021, volume 338 of EPTCS, pages 39-45, 2021. URL: https://doi.org/10.4204/EPTCS.338.6.
  35. Robert B Miller. Response time in man-computer conversational transactions. In Proceedings of the December 9-11, 1968, fall joint computer conference, part I, pages 267-277, 1968. Google Scholar
  36. Julien Narboux. A graphical user interface for formal proofs in geometry. J. Autom. Reason., 39(2):161-180, 2007. URL: https://doi.org/10.1007/s10817-007-9071-4.
  37. Chris Okasaki. Red-black trees in a functional setting. J. Funct. Program., 9(4):471-477, 1999. URL: https://doi.org/10.1017/s0956796899003494.
  38. Lawrence C. Paulson. Thoughts on user interfaces for theorem provers, December 2022. URL: https://web.archive.org/web/20230219221749/https://lawrencecpaulson.github.io/2022/12/14/User_interfaces.html.
  39. Clément Pit-Claudel. Untangling mechanized proofs. In Ralf Lämmel, Laurence Tratt, and Juan de Lara, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, Virtual Event, USA, November 16-17, 2020, pages 155-174. ACM, 2020. URL: https://doi.org/10.1145/3426425.3426940.
  40. Kurt Reidemeister. Knot theory. BCS Associates, 1983. Google Scholar
  41. David Reutter and Jamie Vicary. High-level methods for homotopy construction in associative n-categories. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '19. IEEE Press, 2021. Google Scholar
  42. Valentin Robert. Front-end tooling for building and maintaining dependently-typed functional programs. PhD thesis, University of California, San Diego, USA, 2018. URL: http://www.escholarship.org/uc/item/9q3490fh.
  43. Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura. Tabled Typeclass Resolution. CoRR, 2020. URL: https://arxiv.org/abs/2001.04301v2.
  44. Jörg Siekmann, Stephan Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Armin Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Martin Pollet, and Volker Sorge. Loui: Lovely omega user interface. Formal Aspects of Computing, 11(3):326-342, 1999. URL: https://doi.org/10.1007/s001650050053.
  45. Aaron Stockdill, Daniel Raggi, Mateja Jamnik, Grecia Garcia Garcia, and Peter C.-H. Cheng. Considerations in representation selection for problem solving: A review. In Amrita Basu, Gem Stapleton, Sven Linker, Catherine Legg, Emmanuel Manalo, and Petrucio Viana, editors, Diagrammatic Representation and Inference, pages 35-51, Cham, 2021. Springer International Publishing. Google Scholar
  46. Makarius Wenzel. Asynchronous user interaction and tool integration in isabelle/pide. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 515-530. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_33.
  47. Katherine Ye, Wode Ni, Max Krieger, Dor Ma'ayan, Jenna Wise, Jonathan Aldrich, Joshua Sunshine, and Keenan Crane. Penrose: from mathematical notation to beautiful diagrams. ACM Trans. Graph., 39(4):144, 2020. URL: https://doi.org/10.1145/3386569.3392375.
  48. Bohua Zhan, Zhenyan Ji, Wenfan Zhou, Chaozhu Xiang, Jie Hou, and Wenhui Sun. Design of point-and-click user interfaces for proof assistants. In Yamine Aït Ameur and Shengchao Qin, editors, Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings, volume 11852 of Lecture Notes in Computer Science, pages 86-103. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-32409-4_6.
  49. Jiaje Zhang and Donald A. Norman. Representations in distributed cognitive tasks. Cognitive Science, 18(1):87-122, 1994. URL: https://doi.org/10.1016/0364-0213(94)90021-3.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact