A Tool for Producing Verified, Explainable Proofs.
Edward William Ayers
Corpus Christi College
University of Cambridge
Submission Date: 2021-09-06
This thesis is submitted for the degree of Doctor of Philosophy.
This thesis is the result of my own work and includes nothing which is the outcome of work done in collaboration except as declared in the preface and specified in the text. It is not substantially the same as any work that has already been submitted before for any degree or other qualification except as declared in the preface and specified in the text. It does not exceed the prescribed word limit for the Mathematics Degree Committee.
Abstract
Mathematicians are reluctant to use interactive theorem provers. In this thesis I argue that this is because proof assistants don't emphasise explanations of proofs; and that in order to produce good explanations, the system must create proofs in a manner that mimics how humans would create proofs. My research goals are to determine what constitutes a human-like proof and to represent human-like reasoning within an interactive theorem prover to create formalised, understandable proofs. Another goal is to produce a framework to visualise the goal states of this system.
To demonstrate this, I present HumanProof: a piece of software built for the Lean 3 theorem prover. It is used for interactively creating proofs that resemble how human mathematicians reason. The system provides a visual, hierarchical representation of the goal and a system for suggesting available inference rules. The system produces output in the form of both natural language and formal proof terms which are checked by Lean's kernel. This is made possible with the use of a structured goal state system which interfaces with Lean's tactic system which is detailed in Chapter 3.
In Chapter 4, I present the subtasks automation planning subsystem, which is used to produce equality proofs in a human-like fashion. The basic strategy of the subtasks system is break a given equality problem in to a hierarchy of tasks and then maintain a stack of these tasks in order to determine the order in which to apply equational rewriting moves. This process produces equality chains for simple problems without having to resort to brute force or specialised procedures such as normalisation. This makes proofs more human-like by breaking the problem into a hierarchical set of tasks in the same way that a human would.
To produce the interface for this software, I also created the ProofWidgets system for Lean 3. This system is detailed in Chapter 5. The ProofWidgets system uses Lean's metaprogramming framework to allow users to write their own interactive, web-based user interfaces to display within the VSCode editor and in an online web-editor. The entire tactic state is available to the rendering engine, and hence expression structure and types of subexpressions can be explored interactively. The ProofWidgets system also allows the user interface to interactively edit the proof document, enabling a truly interactive modality for creating proofs; human-like or not.
In Chapter 6, the system is evaluated by asking real mathematicians about the output of the system, and what it means for a proof to be understandable to them. The user group study asks participants to rank and comment on proofs created by HumanProof alongside natural language and pure Lean proofs. The study finds that participants generally prefer the HumanProof format over the Lean format. The verbal responses collected during the study indicate that providing intuition and signposting are the most important properties of a proof that aid understanding.
My first contact with the ideas of formalised mathematics came from reading the anonymously authored QED Manifesto[Ano94[Ano94]AnonymousThe QED manifesto (1994)Automated Deduction--CADE(link)]In this thesis, shortened citation references will appear in the sidebar, a full bibliography with all reference details is provided at the end of the document. Some sidebar citations will be omitted if there is not enough space. which envisions a 'QED system' in which all mathematical knowledge is stored in a single, computer-verified repository.
This idea dizzied me: perhaps review of mathematics will amount to remarking on style and interest, with checking of proofs performed automatically from a machine readable document.
The general term that I will use for software that works towards this vision is proof assistant or Interactive Theorem Prover ITP. A proof assistant at its most general is a piece of software that allows users to create and verify mathematical proofs. In Section 2.1 I will provide more detail how proof assistants are generally constructed.
In 2007, Freek Wiedijk [Wie07[Wie07]Wiedijk, FreekThe QED manifesto revisited (2007)Studies in Logic, Grammar and Rhetoric(link)] pronounced the QED project to have "not been a success (yet)", citing not enough people working on formalised mathematics and the severe differences between formalised and 'real' mathematics, both at a syntactic level (formalised mathematics resembles source code) and at a foundational level (formalised mathematics is usually constructive and procedural as opposed to classical and declarative).
Similarly, Alan Bundy [Bun11[Bun11]Bundy, AlanAutomated theorem provers: a practical tool for the working mathematician? (2011)Annals of Mathematics and Artificial Intelligence(link)] notes that although mathematicians have readily adopted computational tools such as TEX[Knu86[Knu86]Knuth, Donald E.The TeXbook (1986)publisher Addison-Wesley] and computer algebra systemsA computer algebra system (CAS) is a tool for symbolic manipulation of formulae and expressions, without necessarily having a formalised proof that the manipulation is sound. Examples of CASes include Maple and Mathematica., computer aided proving has had very little impact on the workflow of a working mathematician. Bundy cites several reasons for this which will be discussed in Section 1.1.
Now, a decade later, the tide may be turning.
In 2021, proof assistants are pretty good. There are several well-supported large-scale systems such as Isabelle[Pau89], Coq[Coq], Lean[MKA+15], HOL Light[Har09], Agda[Nor08], Mizar[GKN15], PVS[SORS01] and many more. These systems are used to define and prove mathematical facts in a variety of logics (e.g. FOL, HOL, CIC, univalent foundations). These systems are bridged to powerful, automated reasoning systems (e.g. Vampire[RV02], Z3[MB08], E[SCV19] and Leo-III[SB18a]. Within these systems, many theorems big and small (4-colour theorem [Gon08], Feit-Thompson theorem [GAA+13], Kepler conjecture [HAB+17]) have been proved in a variety of fields, accompanied by large mathematical libraries (Isabelle's Archive of Formal Proofs, Lean's mathlib, Coq's Mathematical Components, Mizar's Formalized Mathematics) whose intersection with undergraduate and research level mathematics is steadily growingSee, for example, the rate of growth of the Lean 3 mathematical library https://leanprover-community.github.io/mathlib_stats.html..
However, in spite of these advances, we are still yet to see widespread adoption of ITP by mathematicians outside of some (growing) cliques of enthusiasts.
In this thesis I wish to address this problem through engaging with how mathematicians use and understand proofs to create new ways of interacting with formalised proof.
Let's first expand on the problem a little more and then use this to frame the research questions that I will tackle for the remainder of the thesis.
1.1. Mathematicians and proof assistants
Here I offer 3 possible explanations for why mathematicians have not adopted proof assistants.
Many have commented on these before: Bundy [Bun11] summarises the main challenges well.
1. Differing attitudes towards correctness and errors.
Mathematicians don't worry about mistakes in the same way as proof assistants doI will present some evidence for this in Section 2.5..
Mathematicians care deeply about correctness, but historically the dynamics determining whether a result is considered to be true are also driven by sociological mechanisms such as peer-review; informal correspondences; 'folk' lemmas and principles; reputation of authors; and so on [MUP79[MUP79]de Millo, Richard A; Upton, Richard J; Perlis, Alan JSocial processes and proofs of theorems and programs (1979)Communications of the ACM(link)].
A proxy for trustworthiness of a result is the number of other mathematicians that have scrutinized the work.
That is, if the proof is found on an undergraduate curriculum, you can predict with a high degree of confidence that any errors in the proof will be brought to the lecturer's attention.
In contrast, a standalone paper that has not yet been used for any subsequent work by others is typically treated with some degree of caution.
2. High cost.
Becoming proficient in an ITP system such as Isabelle or Coq can require a lot of time.
And then formalising an area of maths can take around ten times the amount of time required to write a corresponding paper or textbook on the topic.
This time quickly balloons if it is also necessary to write any underlying assumed knowledge of the topic (e.g., measure theory first requires real analysis).
This 'loss factor' of the space cost of developing a formalised proof over that of a natural language proof was first noted by de Bruijn in relation to his AUTOMATH prover [DeB80[DeB80]De Bruijn, Nicolaas GovertA survey of the project AUTOMATH (1980)To H.B.Curry: Essays on Combinatory Logic,Lambda Calculus and Formalism(link)]. De Bruijn estimates a factor of 20 for AUTOMATH, and Wiedijk later estimates this factor to be closer to three or four in Mizar[Wie00[Wie00]Wiedijk, FreekThe de Bruijn Factor (2000)http://www.cs.ru.nl/F.Wiedijk/factor/factor.pdf]. There are costs other than space too, the main one of concern here being the time to learn to use the tools and the amount of work required per proof.
3. Low reward.
What does a mathematician have to gain from formalising their research? In many cases, there is little to gain other than confirming something the researcher knew to be true anyway. The process of formalisation may bring to light 'bugs' in the work: perhaps there is a trivial case that wasn't accounted for or an assumption needs to be strengthened.
Sometimes the reward is high enough that there is a clear case for formalisation, particularly when the proof involves some computer-generated component.
This is exemplified by Hales' proof [Hal05[Hal05]Hales, Thomas CA proof of the Kepler conjecture (2005)Annals of mathematics(link)] and later formalised proof [HAB+17[HAB+17]Hales, Thomas C; Adams, Mark; Bauer, Gertrud; et al.A formal proof of the Kepler conjecture (2017)Forum of Mathematics, Pi(link)] of the Kepler conjecture. The original proof involved lengthy computer generated steps that were difficult for humans to check, and so Hales led the Flyspeck project to formalise it, taking 21 collaborators around a decade to complete.
Another celebrated example is Gonthier's formalisation of the computer-generated proof of the four-colour theorem [Gon08[Gon08]Gonthier, GeorgesFormal proof--the four-color theorem (2008)Notices of the AMS(link)].
Formalisation is also used regularly in formalising expensive hardware and safety-critical computer software (e.g., [KEH+09[KEH+09]Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; et al.seL4: Formal verification of an OS kernel (2009)Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles(link), Pau98[Pau98]Paulson, Lawrence CThe inductive approach to verifying cryptographic protocols (1998)Journal of Computer Security(link)]).
The economics of the matter are such that the gains of using ITP are too low compared to the benefits for the majority of cases. Indeed, since mathematicians have a different attitude to correctness, there are sometimes no benefits to formalisation.
As ITP developers, we can improve the situation by either decreasing the learning cost or increasing the utility.
How can we make ITP easier to learn?
One way is to teach it in undergraduate mathematics curricula (not just computer science).
An example of such a course is Massot's Introduction aux mathématiques formalisées taught at the Université Paris Sud.
Another way is to improve the usability of the user interface for the proof assistant; I will consider this point in more detail in Chapter 5.
How can we increase the utility that mathematicians gain from using a proof assistant?
In this thesis I will argue that one way to help with these three issues is to put more emphasis on interactive theorem provers providing explanations rather than a mere guarantee of correctness.
We can see that explanations are important because mathematicians care about new proofs of old results that treat the problem in a new way.
Proofs from the Book[AZHE10[AZHE10]Aigner, Martin; Ziegler, Günter M; Hofmann, Karl H; et al.Proofs from the Book (2010)publisher Springer(link)] catalogues some particularly lovely examples of this.
Can computers also provide informal proofs with more emphasis on explanations?
Gowers [Gow10[Gow10]Gowers, W. T.Rough structure and classification (2010)Visions in Mathematics(link) §2] presents an imagined interaction between a mathematician and a proof assistant of the future.
An interesting feature of this conversation is that the status of the formal correctness of any of the statements conveyed by the computer is not mentioned.
Similar notions are brought to light in the work of Corneli et al.[CMM+17[CMM+17]Corneli, Joseph; Martin, Ursula; Murray-Rust, Dave; et al.Modelling the way mathematics is actually done (2017)Proceedings of the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Design(link)] in their modelling of informal mathematical dialogues and exposition.
Why not have both explanatory and verified proofs? I suspect that if an ITP system is to be broadly adopted by mathematicians, it must concisely express theorems and their proofs in a way similar to that which a mathematician would communicate with fellow mathematicians.
This not only requires constructing human-readable explanations, but also a reimagining of how the user can interact with the prover.
In this thesis, I will focus on problems that are considered 'routine' for a mathematician.
That is, problems that a mathematician would typically do 'on autopilot' or by 'following their nose' For example, showing that (a+b)2=a2+2ab+b2 from the ring axioms..
I choose to focus on this class of problem because I believe it is an area where ITP could produce proofs that explain why they are true rather than merely provide a certificate of correctness. The typical workflow when faced with a problem like this is to either meticulously provide a low-level proof or apply automation such as Isabelle's auto, or an automation orchestration tool such as Isabelle's Sledgehammer [BN10[BN10]Böhme, Sascha; Nipkow, TobiasSledgehammer: judgement day (2010)International Joint Conference on Automated Reasoning(link)]. In the case of using an automation tacticBroadly, a tactic is a program for creating proofs. I will drill down on how this works in Chapter 2. like auto the tactic will either fail or succeed, leaving the user with little feedback on why the result is true.
There are some tools for producing intelligible proofs from formalised ones, for example, the creation of Isar [Wen99[Wen99]Wenzel, MarkusIsar - A Generic Interpretative Approach to Readable Formal Proof Documents (1999)Theorem Proving in Higher Order Logics(link)] proofs from Sledgehammer by Blanchette et al.[BBF+16[BBF+16]Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; et al.Semi-intelligible Isar proofs from machine-generated proofs (2016)Journal of Automated Reasoning(link)].
However, gaining an intuition for a proof will be easier if the proof is generated in a way that reflects how a human would solve the problem, and so translating a machine proof to a proof which a human will extract meaning from is an uphill battle.
1.1.1. Types of understandability
The primary motivation of the work in this thesis is to help make ITP systems more appealing to mathematicians.
The approach I chosen to take towards this is to research ways of making ITP systems more understandable.
There are many components of ITP that I consider with respect to understandability:
interaction: is the way in which the user interacts and creates a proof easy to understand?
system-output: is the final proof rendered to the user easy to understand?
underlying representations: is the way in which the proof is stored similar to the user's understanding of the proof?
automation: if a proof is generated automatically, is it possible for a user to follow it?
The different parts of my thesis will address different sets of these ways in which a proof assistant can be understandable.
With respect to the automation and underlying-representation aspects of understandability, we will see in Section 2.6 that there is some debate over whether prover automation needs to be easy to follow for a human or not (machine-like vs. human-like).
In this thesis I take a pragmatic stance that the understandability of automation and underlying-representation need not be human-like provided that the resulting interaction and output is understandable. However, as I investigate in Chapter 4, there may be ways of creating automation that are more conducive to creating understandable output and interaction.
1.2. Research questions
In the context of these facets of an understandable ITP system, there arise some key research questions that I seek to study.
Question 1. What constitutes a human-like, understandable proof?
Objectives:
Identify what 'human-like' and 'understandable' mean to different people.
Distinguish between human-like and machine-like proofs in the context of ITP.
Merge these strands to determine a working definition of human-like proof.
Question 2. How can human-like reasoning be represented within an interactive theorem prover to produce formalised, understandable proofs?
Objectives:
Form a calculus of representing goal states and inference steps that act at the abstraction layer that a human uses when solving proofs.
Create a system for producing natural language proofs from this calculus.
Evaluate the resulting system by performing a study on real mathematicians.
Question 3. How can this mode of human-like reasoning be presented to the user in an interactive, multimodal way?
Objectives:
Investigate new ways of interacting with proof objects.
Make it easier to create novel graphical user interfaces (GUIs) for interactive theorem provers.
Produce an interactive interface for a human-like reasoning system.
1.3. Contributions
This thesis presents a number of contributions towards the above research questions:
An abstract calculus for developing human-like proofs (Chapter 3).
An interface between this abstraction layer and a metavariable-driven tactic state, as is used in theorem provers such as Coq and Lean, producing formally verified proofs (Chapter 3 and Appendix A).
A procedure for generating natural language proofs from this calculus (Section 3.6).
The 'subtasks' algorithm, a system for automating the creation of chains of equalities and inequalities. This work has been published in [AGJ19[AGJ19]Ayers, E. W.; Gowers, W. T.; Jamnik, MatejaA human-oriented term rewriting system (2019)KI 2019: Advances in Artificial Intelligence - 42nd German Conference on AI(link)] (Chapter 4).
A graphical user interface framework for interactive theorem provers (Chapter 5). This has been published in [AJG21[AJG21]Ayers, E. W.; Jamnik, Mateja; Gowers, W. T.A graphical user interface framework for formal verification (2021)Interactive Theorem Proving(link)].
An implementation of all of the above contributions in the Lean 3 theorem prover.
A study assessing the impact of natural language proofs with practising mathematicians (Chapter 6).
The implementations for these contributions can be found at the following links:
An implementation of the ProofWidgets code has been incorporated in to the leanprover-community fork of the Lean theorem prover. The relevant pull requests are:
In Chapter 2, I will provide an overview of the background material needed for the remaining chapters.
Next, in Chapter 3, I introduce the HumanProof software for producing human-like proofs within the Lean proof assistant.
I provide motivation of the design in Section 3.1, an overview of the system in Section 3.2 and then dive in to the details of how the system is designed, including the natural-language generation engine in Section 3.6.
Chapter 4 discusses a system for producing equational reasoning proofs called the subtask algorithm.
Chapter 5 details the ProofWidgets system, which is used to produce the user interface of HumanProof.
Chapter 6 provides the design and results of a user study that I conducted on mathematicians to determine whether HumanProof really does provide understandable proofs.
Finally, Chapter 7 wraps things up with some reflection on my progress and a look ahead to future work.
There are also four appendices:
Appendix A presents some additional technical detail on interfacing HumanProof with Lean.
The work in Chapter 3 is my own, although the box calculus presented is inspired through many sessions of discussion with W.T. Gowers and the design of Gowers' previous collaboration with Ganesalingam [GG17[GG17]Ganesalingam, Mohan; Gowers, W. T.A fully automatic theorem prover with human-style output (2017)Journal of Automated Reasoning(link)]. More on this will be given when it is surveyed in Section 2.6 and Section 3.3.5.
The work in Chapter 4 is previously published at KI 2019 [AGJ19[AGJ19]Ayers, E. W.; Gowers, W. T.; Jamnik, MatejaA human-oriented term rewriting system (2019)KI 2019: Advances in Artificial Intelligence - 42nd German Conference on AI(link)].
The work presented in Chapter 5 is pending publication in ITP 2021 [AJG21[AJG21]Ayers, E. W.; Jamnik, Mateja; Gowers, W. T.A graphical user interface framework for formal verification (2021)Interactive Theorem Proving(link)] and is also merged in to the Lean 3 community repository. The design is strongly influenced by Elm and React; however, there are a number of novel architectural contributions necessitated by the unique challenges of implementing a portable framework within a proof assistant.
The user study presented in Chapter 6 is all my own work with a lot of advisory help from Mateja Jamnik, Gem Stapleton and Aaron Stockdill on designing the study.
1.6. Acknowledgements
I thank my supervisors W. T. Gowers and Mateja Jamnik for their ideas, encouragement and support and for letting me work on such a wacky topic.
I thank Gabriel Ebner and Brian Gin-ge Chen for reading through my ProofWidgets PRs. I thank Patrick Massot, Kevin Buzzard and the rest of the Lean Prover community for complaining about my PRs after the fact.
I thank Jeremy Avigad for taking the time to introduce me to Lean at the Big Proof conference back in 2017.
I thank Bohua Zhan, Chris Sangwin, and Makarius Wenzel and many more for the enlightening conversations on automation for mathematicians at Big Proof and beyond.
I thank Peter Koepke for being so generous in inviting me to Bonn to investigate Naproche/SAD with Steffan Frerix and Andrei Paskevich.
I thank Larry Paulson and the ALEXANDRIA team for letting me crash their weekly meetings.
I thank my parents for letting me write up in the house during lockdown.
I thank my friends and colleagues in the CMS. Andrew, Eric, Sammy P, Sven, Ferdia, Mithuna, Kasia, Sam O-T, Bhavik, Wojciech, and many more.
In parallel, the Computer Laboratory: Chaitanya, Botty, Duo, Daniel, Aaron, Angeliki, Yiannos, Wenda, Zoreh.
I decided to typeset this thesis as HTML-first, print second.
The digital copy may be found at https://edayers.com/thesis.
The printed version of this thesis was generated by printing out the website version and concatenating.
I was able to create the thesis in this way thanks to many open-source projects.
I will acknowledge the main ones here. React, Gatsby, Tachyons, PrismJS. Thanks to Titus Woormer for remarkJS and also adding my feature request in less than 24 hours!
The code font is PragmataPro created by Fabrizio Schiavi.
The style of the site is a modified version of the Edward Tufte Handout style.
The syntax colouring style is based on the VS theme by Andrew Lock.
I also use some of the vscode-icons icons.
Chapter 2
Background
In this chapter I will provide a variety of background material that will be used in later chapters.
Later chapters will include links to the relevant sections of this chapter.
I cover a variety of topics:
Section 2.1 gives an overview of how proof assistants are designed. This provides some context to place this thesis within the field of ITP.
Section 2.2 contains some preliminary definitions and notation for types, terms, datatypes and functors that will be used throughout the document.
Section 2.3 contains some additional features of inductive datatypes that I will make use of in various places throughout the text.
Section 2.4 discusses the way in which metavariables and tactics work within the Lean theorem prover, the system in which the software I write is implemented.
Section 2.5 asks what it means for a person to understand or be confident in a proof. This is used to motivate the work in Chapter 3 and Chapter 4. It is also used to frame the user study I present in Chapter 6.
Section 2.6 explores what the automated reasoning literature has to say on how to define and make use of 'human-like reasoning'. This includes a survey of proof planning (Section 2.6.2).
Section 2.7 surveys the topic of natural language generation of mathematical texts, used in Section 3.6.
2.1. The architecture of proof assistants
In this section I am going to provide an overview of the designs of proof assistants for non-specialist.
The viewpoint I present here is largely influenced by the viewpoint that Andrej Bauer expresses in a MathOverflow answer [Bau20[Bau20]Bauer, AndrejWhat makes dependent type theory more suitable than set theory for proof assistants? (2020)https://mathoverflow.net/q/376973].
The essential purpose of a proof assistant is to represent mathematical theorems, definitions and proofs in a language that can be robustly checked by a computer. This language is called the foundation language equipped with a set of derivation rules. The language defines the set of objects that formally represent mathematical statements and proofs, and the inference rules and axioms provide the valid ways in which these objects can be manipulatedAt this point, we may raise a number of philosophical objections such as whether the structures and derivations 'really' represent mathematical reasoning.
The reader may enjoy the account given in the first chapter of Logic for Mathematicians by J. Barkley Rosser [Ros53]..
Some examples of foundations are first-order logic (FOL), higher-order logic (HOL), and various forms of dependent type theory (DTT) [Mar84, CH88, PP89, Pro13].
A component of the software called the kernel checks proofs in the foundation.
There are numerous foundations and kernel designs.
Finding new foundations for mathematics is an open research area but FOL, HOL and DTT mentioned above are the most well-established for performing mathematics.
I will categorise kernels as being either 'checkers' or 'builders'.
A 'checker' kernel takes as input a proof expression and outputs a yes/no answer to whether the term is a valid proof.
An example of this is the Lean 3 kernel [MKA+15[MKA+15]de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; et al.The Lean theorem prover (system description) (2015)International Conference on Automated Deduction(link)].
A 'builder' kernel provides a fixed set of partial functions that can be used to build proofs.
Anything that this set of functions accepts is considered as valid.
This is called an LCF architecture, originated by Milner [Mil72[Mil72]Milner, RobinLogic for computable functions description of a machine implementation (1972)Technical Report(link), Gor00[Gor00]Gordon, MikeFrom LCF to HOL: a short history (2000)Proof, language, and interaction(link)]. The most widely used 'builder' is the Isabelle kernel by Paulson [Pau89[Pau89]Paulson, Lawrence CThe foundation of a generic theorem prover (1989)Journal of Automated Reasoning(link)].
Most kernels stick to a single foundation or family of foundations. The exception is Isabelle, which instead provides a 'meta-foundation' for defining foundations, however the majority of work in Isabelle uses the HOL foundation.
2.1.1. The need for a vernacular
One typically wants the kernel to be as simple as possible, because any bugs in the kernel may result in 'proving' a false statement
An alternative approach is to 'bootstrap' increasingly complex kernels from simpler ones. An example of this is the
Milawa theorem prover for ACL2 [Dav09]..
For the same reason, the foundation language should also be as simple as possible.
However, there is a trade-off between kernel simplicity and the usability and readability of the foundation language;
a simplified foundation language will lack many convenient language features such as implicit arguments and pattern matching, and as a result will be more verbose.
If the machine-verified definitions and lemmas are tedious to read and write, then the prover will not be adopted by users.
Proof assistant designers need to bridge this gap between a human-readable, human-understandable proof and a machine-readable, machine-checkable proof.
A common approach is to use a second language called the vernacular (shown on Figure 2.5).
The vernacular is designed as a human-and-machine-readable compromise that is converted to the foundation language through a process called elaboration (e.g., [MAKR15[MAKR15]de Moura, Leonardo; Avigad, Jeremy; Kong, Soonho; et al.Elaboration in Dependent Type Theory (2015)CoRR(link)]).
The vernacular typically includes a variety of essential features such as implicit arguments and some form of type inference, as well as high-level programming features such as pattern matching.
Optionally, there may be a compiler (see Figure 2.5) for the vernacular to also produce runnable code, for example Lean 3 can compile vernacular to bytecode [EUR+17[EUR+17]Ebner, Gabriel; Ullrich, Sebastian; Roesch, Jared; et al.A metaprogramming framework for formal verification (2017)Proceedings of the ACM on Programming Languages(link)].
I discuss some work on provers with the vernacular being a restricted form of natural language as one might find in a textbook in Section 2.7.2.
2.1.2. Programs for proving
Using a kernel for checking proofs and a vernacular structure for expressing theorems, we now need to be able to construct proofs of these theorems.
An Automated Theorem Prover (ATP) is a piece of software that produces proofs for a formal theorem statement automatically with a minimal amount of user input as to how to solve the proof, examples include Z3, E and Vampire.
Interactive Theorem Proving (ITP) is the process of creating proofs incrementally through user interaction with a prover.
I will provide a review of user interfaces for ITP in Section 5.1.
Most proof assistants incorporate various automated and interactive theorem proving components. Examples of ITPs include Isabelle[Pau89], Coq[Coq], Lean[MKA+15], HOL Light[Har09], Agda[Nor08], Mizar[GKN15], PVS[SORS01].
A common modality for allowing the user to interactively construct proofs is with the proof script (Figure 2.1), this is a sequence of textual commands, written by the user to invoke certain proving programs called tactics that manipulate a state representing a partially constructed proof.
An example of a tactic is the assume tactic in Figure 2.1, which converts a goal-state of the form ⊢ X → Y to X ⊢ Y.
Some of these tactics my invoke various ATPs to assist in constructing proofs.
Proof scripts may be purely linear as in Figure 2.1 or have a hierarchical structure such as in Isar [Wen99[Wen99]Wenzel, MarkusIsar - A Generic Interpretative Approach to Readable Formal Proof Documents (1999)Theorem Proving in Higher Order Logics(link)] or HiProof [ADL10[ADL10]Aspinall, David; Denney, Ewen; Lüth, ChristophTactics for hierarchical proof (2010)Mathematics in Computer Science(link)].
An alternative to a proof script is for the prover to generate an auxiliary proof object file that holds a representation of the proof that is not intended to be human readable.
This is the approach taken by PVS [SORS01[SORS01]Shankar, Natarajan; Owre, Sam; Rushby, John M; et al.PVS prover guide (2001)Computer Science Laboratory, SRI International, Menlo Park, CA(link)] although I will not investigate this approach further in this thesis because most of the ITP systems use the proof-script approach.
In the process of proving a statement, a prover must keep track of partially built proofs.
I will refer to these representations of partially built proofs as development calculi. I will return to development calculi in Section 2.4.
2.1.3. Foundation
A foundation for a prover is built from the following pieces:
A language: defining inductive trees of data that we wish to talk about and also syntax for these trees.
The judgements: meta-level predicates over the above trees.
The inference rules: a generative set of rules for deriving judgements from other judgements.
To illustrate, the language of simply typed lambda calculus would be expressed as in (2.2).
In (2.2), the purple greek and italicised letters (𝑥, 𝑦, α, ...) are called nonterminals.
They say: "You can replace me with any of the |-separated items on the right-hand-side of my ::=".
So, for example, "α" can be replaced with either a member of A or "α → β".
The green words in the final column give a natural language noun to describe the 'kind' of the syntax.
In general terms, contextsΓ perform the role of tracking which variables are currently in scope.
To see why contexts are needed, consider the expression 𝑥+𝑦; its resulting type depends on the types of the variables 𝑥 and 𝑦.
If 𝑥 and 𝑦 are both natural numbers, 𝑥+𝑦 will be a natural number, but if 𝑥 and 𝑦 have different types (e.g, vectors, strings, complex numbers) then 𝑥+𝑦 will have a different type too.
The correct interpretation of 𝑥+𝑦 depends on the context of the expression.
Next, define the judgements for our system in (2.3). Judgements are statements about the language.
Then define the natural deduction rules (2.4) for inductively deriving these judgements.
And from this point, it is possible to start exploring the theoretical properties of the system.
For example: is Γ ⊢ 𝑠:α decidable?
Foundations such as the example above are usually written down in papers as a BNF grammar and a spread of gammas, turnstiles and lines as illustrated in (2.2), (2.3) and (2.4).
LISP pioneer Steele calls it Computer Science Metanotation[Ste17[Ste17]Steele Jr., Guy L.It's Time for a New Old Language (2017)http://2017.clojure-conj.org/guy-steele/].
In implementations of proof assistants, the foundation typically doesn't separate quite as cleanly in to the above pieces.
The language is implemented with a number of optimisations such as de Bruijn indexing [deB72[deB72]de Bruijn, Nicolaas GovertLambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem (1972)Indagationes Mathematicae (Proceedings)(link)] for the sake of efficiency.
Judgements and rules are implicitly encoded in algorithms such as type checking, or appear in forms different from that in the corresponding paper.
This is primarily for efficiency and extensibility.
In this thesis the formalisation language that I focus on is the calculus of inductive constructions (CIC)
Calculus of Inductive Constructions. Inductive datastructures (Section 2.2.3) for the Calculus of Constructions [CH88] were first introduced by Pfenning et al[PP89].
This is the the type theory used by Lean 3 as implemented by de Moura et al and formally documented by Carneiro [Car19[Car19]Carneiro, MarioLean's Type Theory (2019)Masters' thesis (Carnegie Mellon University)(link)].
A good introduction to mathematical formalisation with dependent type theory is the first chapter of the HoTT Book[Pro13[Pro13]The Univalent Foundations ProgramHomotopy Type Theory: Univalent Foundations of Mathematics (2013)publisher Institute for Advanced Study(link) ch. 1].
Other foundations are also available: Isabelle's foundation is two-tiered [Pau89[Pau89]Paulson, Lawrence CThe foundation of a generic theorem prover (1989)Journal of Automated Reasoning(link)]: there is a meta-level foundation upon which many foundations can be implemented. A lot of the work in this thesis is independent of foundation and so I will try to indicate how the contributions can be augmented to work in other foundations.
A typical architecture of a modern, full-fledged checker-style proof assistant is given in Figure 2.5.
2.2. Preliminaries
This section contains a set of quick preliminary definitions for the concepts and notation that I will be using later.
In this thesis I will be using a pseudo-language which should be familiar to functional programming enthusiasts.
This pseudo-language is purely presentational and is used to represent algorithms and datastructures for working with theorem provers.
2.2.1. Some notation for talking about type theory and algorithms
The world is built of types and terms.
New variables are introduced as "𝑥:A"; 𝑥 is the variable and it has the type A.
Lots of variables with the same type can be introduced as 𝑥𝑦𝑧:A.
Types ABC:Type start with an uppercase letter and are coloured turquoise. Type is a special 'type of types'.
Meanwhile terms start with a lowercase letter and term variables are purple and italicised.
A → B is the function type. → is right associative which means that 𝑓:A → B → C should be read as 𝑓:A → (B → C).
This is called a curried function, we may consider A and B to be the input arguments of 𝑓 and C to be its return type.
Given 𝑎:A we may apply𝑓 to 𝑎 by writing 𝑓𝑎:B → C.
Functions are introduced using maps-to notation (𝑎:A) ↦ (𝑏:B) ↦ 𝑓𝑎𝑏.
Write the identity function 𝑥 ↦ 𝑥 as 𝟙 :X → X.
Given 𝑓:A → B, 𝑔:B → C, write function composition as 𝑔 ∘ 𝑓:A → C.
Function application is left associative, so 𝑓𝑎𝑏 should be read as (𝑓(𝑎))(𝑏).
The input types of functions may optionally be given argument names, such as: (𝑎:A) → (𝑏:B) → C.
We also allow 'dependent types' where the return value C is allowed to depend on these arguments: (𝑎:A) → 𝒞 𝑎 where 𝒞 :A → Type is a type-valued function.
Empty is the empty type.
Unit is the type containing a single element ().
Bool is the boolean type ranging over values true and false.
OptionX is the type taking values some𝑥 for 𝑥:X or none. some will usually be suppressed. That is, 𝑥:X will be implicitly cast to some𝑥:OptionX in the name of brevity.
ListX is the type of finite lists of X. Given 𝑥𝑦:X and 𝑙₁𝑙₂:ListX, we can write 𝑥::𝑙₁ for list cons and 𝑙₁++𝑙₂ for concatenating (i.e, appending) two lists. For list construction and pattern matching, list spreads will be used. For example[..𝑙₁,𝑥,𝑦,..𝑙₂] denotes the list formed by concatenating 𝑙₁, [𝑥,𝑦] and 𝑙₂. Python-style list comprehensions are also used: [𝑖² for𝑖in1..20] is a list of the first 20 square numbers.
ℕ is the type of natural numbers. Individual numbers can be used as types: 𝑥:3 means that 𝑥 is a natural number taking any value 𝑥<3, i.e, 𝑥 ∈ {0,1,2}.
A × B is the type of tuples over A and B.
Elements are written as (a,b):A × B.
As usual we have projections π₁ (𝑎,𝑏):=𝑎 and π₂ (𝑎,𝑏):=𝑏.
Members of tuples may be given names as (a:A) × (b:B).
In this case, supposing p:(a:A) × (b:B), we can write p.a and p.b instead of π₁ p and π₂ p.
Similarly to above, we can have a dependent tuple or 'sigma type' (a:A) × (b:B(a)).
A+B is the discriminated union of A and B with constructors inl:A → A+B and inr:B → A+B.
2.2.2. Functors and monads
I will assume that the readers are already familiar with the motivation behind functors and monads in category theory and as used in e.g. Haskell but I will summarise them here for completeness.
I refer the unfamiliar reader to the Haskell Typeclassopediahttps://wiki.haskell.org/Typeclassopedia.
Definition 2.6 (functor): A functor is a type-valued function F:Type → Type equipped with a function mapper F(𝑓:A → B):FA → FBHere, the word 'functor' is used to mean the special case of category-theoretical functors with the domain and codomain category being the category of Type..
I always assume that the functor is lawful, which here means it obeys the functor laws (2.7).
Definition 2.8 (natural function): A natural functiona:F ⇒ G between functors FG:Type → Type is a family of functions a[A]:FA → GA indexed by A:Type such that a[B] ∘ Ff=Gf ∘ a[A] for all f:A → B. Often the type argument to a will be suppressed.
It is quick to verify that the functors and natural functors over them form a category.
Definition 2.9 (monad): A monadFor learning about programming with monads, see https://wiki.haskell.org/All_About_MonadsM:Type → Type is a functor equipped with two natural functions pure: 𝟙 ⇒ M and join:MM ⇒ M obeying the monad laws (2.10). Write 𝑚>>=𝑓:=join(M𝑓𝑚) for 𝑚:MA and 𝑓:A → MB.
do notation is used in placeshttps://wiki.haskell.org/Keywords#do.
Definition 2.11 (applicative): An applicative functor[MP08[MP08]McBride, Conor; Paterson, RossApplicative programming with effects (2008)J. Funct. Program.(link) §2]M:Type → Type is equipped with pure:A → MA and seq:M(A → B) → MA → MB.
Write 𝑓<*>𝑎:=seq𝑓𝑥<*> is left associative: 𝑢<*>𝑣<*>𝑤=(𝑢<*>𝑣)<*>𝑤. and 𝑎*>𝑏:=seq(_ ↦ 𝑎)𝑏. Applicative functors obey the laws given in (2.12).
In cases where it is obvious which constructor is being used, the tag names are suppressed.
Function definitions with pattern matching use the syntax given in (2.14).
One can express inductive datatypes D as fixpoints of functors D=FixP where FixP:=P(FixP).
Depending on the underlying category, FixP may not exist for all PSmyth and Plotkin are the first to place some conditions on when the fixpoint exists [SP82], see Adámek et al for a survey [AMM18].[SP82]Smyth, Michael B; Plotkin, Gordon DThe category-theoretic solution of recursive domain equations (1982)SIAM Journal on Computing(link)[AMM18]Adámek, Jiří; Milius, Stefan; Moss, Lawrence SFixed points of functors (2018)Journal of Logical and Algebraic Methods in Programming(link).
Definition 2.15 (base functor): When a D:Type is written as FixP for some P (and there is no Q such that P=Q ∘ Q ∘ ... ∘ Q), P is called the base functor for D.
This conceptualisation is useful because we can use the base functor to make related types without needing to explicitly write down the constructors for the modified versions. For example we can make the list lazy with LazyPX:=Fix((X ↦ Unit → X) ∘ P).
2.3. Inductive gadgets
For the rest of this thesis, I will make use of a few motifs for discussing inductive datastructures, particularly in Section 2.4, Chapter 3, Appendix A and Appendix C.
In this section I will lay some background material for working with inductive datatypes.
2.3.1. Traversable functors
Given a monad M, a common task is performing a monad-map with f:A → MB over a list of objects l:ListX.
This is done with the help of a function called mmap(2.16).
But we can generalise List to some functor T:Type → Type; when can we equip an analogous mmap to T?
For example, in the case of binary trees (2.17).
Definition 2.18 (traversable): A functor T:Type → Type is traversable when for all applicative functors (Definition 2.11) M:Type → Type,
there is a natural function d[M]:(T ∘ M) ⇒ (M ∘ T).
That is, for each X:Type we have d[M][X]:T(MX) → M(TX).
In addition to being natural, d must obey the traversal laws given in (2.19)[JR12[JR12]Jaskelioff, Mauro; Rypacek, OndrejAn Investigation of the Laws of Traversals (2012)Proceedings Fourth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2012, Tallinn, Estonia(link) Definition 3.3].
Given a traversable functor T and a monad M, we can recover mmap:(A → MB) → TA → M(TB) as mmap𝑓𝑡:=d[M][B](T𝑓𝑡).
2.3.2. Functors with coordinates
Bird et al[BGM+13[BGM+13]Bird, Richard; Gibbons, Jeremy; Mehner, Stefan; et al.Understanding idiomatic traversals backwards and forwards (2013)Proceedings of the 2013 ACM SIGPLAN symposium on Haskell(link)] prove that (in the category of sets) the traversable functors are equivalent to a class of functors called finitary containers.
Their theorem states that there is a type ShapeT𝑛:TypeAn explicit definition of ShapeT𝑛 is the pullback of children[1]:TUnit ⟶ ListUnit and !𝑛:Unit ⟶ ListUnit, the list with 𝑛 elements. for each traversable T and 𝑛:ℕ such that that each 𝑡:TX is isomorphic to an object called a finitary container on ShapeT shown in (2.20).
map and traverse may be defined for the finitary container as map and traverse over the children vector.
Since 𝑡:TX has 𝑡.length child elements, the children of 𝑡 can be indexed by the numbers {𝑘:ℕ|𝑘<length}.
We can then define operations to get and set individual elements according to this index 𝑘.
Usually, however, this numerical indexing of the children of 𝑡:TX loses the semantics of the datatype.
As an example; consider the case of a binary tree Tree in (2.21). A tree 𝑡:TreeX with 𝑛branch components will have length 𝑛 and a corresponding children:Vec𝑛X, but indexing via numerical indices {𝑘|𝑘<𝑛} loses information about where the particular child 𝑥:X can be found in the tree.
Now I will introduce a new way of indexing the members of children for the purpose of reasoning about inductive datatypes.
This idea has been used and noted before many times, the main one being paths in universal algebra [BN98[BN98]Baader, Franz; Nipkow, TobiasTerm rewriting and all that (1998)publisher Cambridge University Press(link) Dfn. 3.1.3].
However, I have not seen an explicit account of this idea in the general setting of traversable functors and later to general inductive datatypes (Section 2.3.3).
Definition 2.22 (coordinates): A traversable functor Thas coordinates when equipped with a type C:Type and a function coords[𝑛]:ShapeT𝑛 → Vec𝑛C.
The coords function amounts to a labelling of the 𝑛 children of a particular shape with members of C.
Often when using traversals, working with the children list Vec(length𝑡)X for each shape of T can become unwieldy, so it is convenient to instead explicitly provide a pair of functions get and set(2.23) for manipulating particular children of a given 𝑡:TX.
C is not unique, and in general should be chosen to have some semantic value for thinking about the structure of T.
Here are some examples of functors with coordinates:
List has coordinates ℕ. coords𝑙 for 𝑙:ListX returns a list [0, ⋯,𝑙.length-1]. get𝑖𝑙 is some𝑙[𝑖] and set𝑖𝑙𝑥 returns a new list with the 𝑖th element set to be 𝑥.
Vecn, lists of length n, has coordinates {k:ℕ|k<n} with the same methods as for List above.
Option has coordinates Unit. coords(some𝑥):=[()] and coordsnone:=[]. get_𝑜:=𝑜 and set replaces the value of the option.
Binary trees have coordinates ListD as shown in (2.24).
2.3.3. Coordinates on initial algebras of traversable functors
Given a functor F with coordinates C, we can induce coordinates on the free monad FreeF:Type → Type of F.
The free monad is defined concretely in (2.25).
We can write FreeFX as the fixpoint of A ↦ X+FAAs mentioned in Section 2.2.3, these fixpoints may not exist. However for the purposes of this thesis the Fs of interest are always polynomial functors..
FreeF has coordinates ListC with methods defined in (2.26).
In a similar manner, ListC can be used to reference particular subtrees of an inductive datatype D which is the fixpoint of a traversable functor D=FD.
Let F have coordinates C.
D here is not a functor, but we can similarly define coords:D → List(ListC), get:ListC → OptionD and set:ListC → D → D → D.
The advantage of using coordinates over some other system such as optics[FGM+07[FGM+07]Foster, J Nathan; Greenwald, Michael B; Moore, Jonathan T; et al.Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem (2007)ACM Transactions on Programming Languages and Systems (TOPLAS)(link)] or other apparati for working with datatypes [LP03[LP03]Lämmel, Ralf; Peyton Jones, SimonScrap Your Boilerplate (2003)Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27-29, 2003, Proceedings(link)] is that they are much simpler to reason about.
A coordinate is just an address of a particular subtree.
Another advantage is that the choice of C can convey some semantics on what the coordinate is referencing (for example, C=left|right in (2.24)), which can be lost in other ways of manipulating datastructures.
2.4. Metavariables
Now with a way of talking about logical foundations, we can resume from Section 2.1.2 and consider the problem of how to represent partially constructed terms and proofs given a foundation.
This is the purpose of a development calculus: to take some logical system L and produce some new system DL such that one can incrementally build terms and proofs in a way that provides feedback at intermediate points and ensures that various judgements hold for these intermediate terms.
In Chapter 3, I will create a new development calculus for building human-like proofs, and in Appendix A this system will be connected to Lean.
First we look at how Lean's current development calculus behaves.
Since I will be using Lean 3 in this thesis and performing various operations over its expressions, I will follow the same general setup as is used in Lean 3.
The design presented here was first developed by Spiwack [Spi11[Spi11]Spiwack, ArnaudVerified computing in homological algebra, a journey exploring the power and limits of dependent type theory (2011)PhD thesis (INRIA)(link)] first released in Coq 8.5.
It was built to allow for a type-safe treatment of creating tactics with metavariables in a dependently-typed foundation.
2.4.1. Expressions and types
In this section I will introduce the expression foundation language that will be used for the remainder of the thesis.
The system presented here is typical of expression structures found in DTT-based provers such as Lean 3 and Coq. I will not go into detail on induction schema and other advanced features because the work in this thesis is independent of them.
Definition 2.27 (expression): A Lean expression is a recursive datastructure Expr defined in (2.28).
In (2.28), Level can be thought of as expressions over some signature that evaluate to natural numbers.
They are used to stratify Lean's types so that one can avoid Girard's paradox [Hur95[Hur95]Hurkens, Antonius J. C.A simplification of Girard's paradox (1995)International Conference on Typed Lambda Calculi and Applications(link)].
Name is a type of easily distinguishable identifiers;
in the case of Lean Names are lists of strings or numbers.
I sugar lambda𝑥α𝑏 as λ (𝑥 ∶ α),𝑏, pi𝑥α𝑏 as Π (𝑥 ∶ α),𝑏, app𝑓𝑎 as 𝑓𝑎 and omit var and const when it is clear what the appropriate constructor is.
Using ExprBase, define pure expressions Expr:=FixExprBase as in Section 2.2.3.
Note that it is important to distinguish between the meta-level type system introduced in Section 2.2 and the object-level type system where the 'types' are merely instances of ExprThis distinction can always be deduced from syntax, but to give a subtle indication of this distinction, object-level type assignment statements such as (𝑥 ∶ α) are annotated with a slightly smaller variant of the colon ∶ as opposed to : which is used for meta-level statements.. That is, 𝑡:Expr is a meta-level statement indicating that 𝑡 is an expression, but ⊢ 𝑡 ∶ α is an object-level judgement about expressions stating that 𝑡 has the type α, where α:Expr and ⊢ α ∶ sort.
Definition 2.29 (variable binding): Variables may be bound by λ and Π expressions. For example, in λ (𝑥 ∶ α),𝑡, we say that the expression binds𝑥 in 𝑡.
If 𝑡 contains variables that are not bound, these are called free variables.
Now, given a partial map σ:Name ⇀ Expr and a term 𝑡:Expr, we define a substitutionsubstσ𝑡:Expr as in (2.30).
This will be written as σ𝑡 for brevity.
I will denote substitutions as a list of Name ↦ Expr pairs. For example, ⦃𝑥 ↦ 𝑡,𝑦 ↦ 𝑠⦄ where 𝑥𝑦:Name are the variables which will be substituted for terms 𝑡𝑠:Expr respectively.
Substitution can easily lead to badly-formed expressions if there are variable naming clashes.
I need only note here that we can always perform a renaming of variables in a given expression to avoid clashes upon substitution.
These clashes are usually avoided within prover implementations with the help of de-Bruijn indexing [deB72].
2.4.2. Assignable datatypes
Given an expression structure Expr and 𝑡:Expr, we can define a traversal over all of the immediate subexpressions of 𝑡.
The function child_traverse defined in (2.31) is different from a normal traversal of a datatructure because the mapping function 𝑓 is also passed a context Γ indicating the current variable context of the subexpression. Thus when exploring a λ-binder, 𝑓 can take into account the modified context. This means that we can define context-aware expression manipulating tools such as counting the number of free variables in an expression (fv in (2.32)).
The idea here is to generalise child_traverse to include any datatype that may involve expressions.
Frequently when building systems for proving, one has to make custom datastructures. For example, one might wish to create a 'rewrite-rule' structure (2.33) for modelling equational reasoning (as will be done in Chapter 4).
Definition 2.34 (telescope): Another example might be a telescope of binders Δ:ListBinder a list of binders is defined as a telescope in Γ:Context when each successive binder is defined in the context of the binders before it. That is, [] is a telescope and [(𝑥∶α),..Δ] is a telescope in Γ if Δ is a telescope in [..Γ,(𝑥∶α)] and Γ ⊢ 𝑥 ∶ α.
But now if we want to perform a variable instantiation or count the number of free variables present in 𝑟:RewriteRule, we have to write custom definitions to do this.
The usual traversal functions from Section 2.3.1 are not adequate for telescopes, because we may need to take into account a binder structure. Traversing a telescope as a simple list of names and expressions will produce the wrong output for fv, because some of the variables are bound by previous binders in the context.
Definition 2.35 (assignable): To avoid having to write all of this boilerplate, let's make a typeclass assignable(2.36) on datatypes that we need to manipulate the expressions in.
The expr_traverse method in (2.36) traverses over the child expressions of a datatype (e.g., the lhs and rhs of a RewriteRule or the type expressions in a telescope). expr_traverse also includes a Context object to enable traversal of child expressions which may be in a different context to the parent datatype.
Now, provided expr_traverse is defined for X: fv, instantiate and other expression-manipulating operations such as those in (2.32) can be modified to use expr_traverse instead of child_traverse.
This assignable regime becomes useful when using de-Bruijn indices to represent bound variables [deB72] because the length of Γ can be used to determine the binder depth of the current expression.
Examples of implementations of assignable and expression-manipulating operations that can make use of assignable can be found in my Lean implementation of this concepthttps://github.com/leanprover-community/mathlib/pull/5719.
2.4.3. Lean's development calculus
In the Lean source code, there are constructors for Expr other than those in (2.30).
Some are for convenience or efficiency reasons (such as Lean 3 macros), but others are part of the Lean development calculus.
The main development calculus construction is mvar or a metavariable, sometimes also called a existential variable or schematic variable.
An mvar ?m acts as a 'hole' for an expression to be placed in later.
There is no kernel machinery to guarantee that an expression containing a metavariable is correct; instead, they are used for the process of building expressions.
As an example, suppose that we needed to prove P ∧ Q for some propositions PQ ∶ Prop.
The metavariable-based approach to proving this would be to declare a new metavariable ?𝑡 ∶ P ∧ Q.
Then, a prover constructs a proof term for P ∧ Q in two steps; declare two new metavariables ?𝑡₁ ∶ P and ?𝑡₂ ∶ Q; and then assign?𝑡 with the expression and.make?𝑡₁?𝑡₂ where and.make ∶ P → Q → P ∧ Q is the constructor for ∧.
After this, ?𝑡₁ and ?𝑡₂ themselves are assigned with p ∶ P and q ∶ Q.
In this way, the proof term can be built up slowly as ?𝑡 ⟿ and.make?𝑡₁?𝑡₂ ⟿ and.makep?𝑡₂ ⟿ and.makepq.
This process is more convenient for building modular programs that construct proofs than requiring that a pure proof term be made all in one go because a partially constructed proof is represented as a proof term where certain subexpressions are metavariables.
Lean comes with a development calculus that uses metavariables.
This section can be viewed as a more detailed version of the account originally given by de Moura et al[MAKR15[MAKR15]de Moura, Leonardo; Avigad, Jeremy; Kong, Soonho; et al.Elaboration in Dependent Type Theory (2015)CoRR(link) §3.2] with the additional details sourced from inspecting the Lean source code.
Lean's metavariable management system makes use of a stateful global 'metavariable context' with carefully formed rules governing valid assignments of metavariables.
While all automated provers make use of some form of metavariables, this specific approach to managing them for use with tactics was first introduced in Spiwack's thesis [Spi11], where the tactic monad for Coq was augmented with a stateful global metavariable context.
The implementation of Lean allows another Expr constructor for metavariables:
Metavariables are 'expression holes' and are denoted as ?𝑥 where 𝑥:Name.
They are placeholders into which we promise to substitute a valid pure expression later.
Similarly to fv(𝑡) being the free variables in 𝑡:Expr, we can define mv(𝑡) to be the set of metavariables present in 𝑡.
However, we still need to be able to typecheck and reduce expressions involving metavariables and so we need to have some additional structure on the context.
The idea is that in addition to a local context Γ, expressions are inspected and created within the scope of a second context called the metavariable context𝑀:MvarContext.
The metavariable context is a dictionary MvarContext:=Name ⇀ MvarDecl where each metavariable declaration 𝑑:MvarDecl has the following information:
identifier:Name A unique identifier for the metavariable.
type:Expr The type of the metavariable.
context:Context The local context of the metavariable.
This determines the set of local variables that the metavariable is allowed to depend on.
assignment:OptionExpr An optional assignment expression. If assignment is not none, we say that the metavariable is assigned.
The metavariable context can be used to typecheck an expression containing metavariables by assigning each occurrence ?𝑥 with the type given by the corresponding declaration 𝑀[𝑥].type in 𝑀.
The assignment field of MvarDecl is used to perform instantiation. We can interpret 𝑀 as a substitution.
As mentioned in Section 2.1.2, the purpose of the development calculus is to represent a partially constructed proof or term.
The kernel does not need to check expressions in the development calculus (which here means expressions containing metavariables), so there is no need to ensure that an expression using metavariables is sound in the sense that declaring and assigning metavariables will be compatible with some set of inference rules such as those given in (2.4).
However, in Appendix A.1, I will provide some inference rules for typing expressions containing metavariables to assist in showing that the system introduced in Chapter 3 is compatible with Lean.
2.4.4. Tactics
A partially constructed proof or term in Lean is represented as a TacticState object.
For our purposes, this can be considered as holding the following data:
The result field is the final expression that will be returned when the tactic completes.
goals is a list of metavariables that are used to denote what the tactic state is currently 'focussing on'.
Both goals and result are in the context of mctx.
Tactics may perform actions such as modifying the goals or performing assignments of metavariables.
In this way, a user may interactively build a proof object by issuing a stream of tactics.
2.5. Understandability and confidence
This section is a short survey of literature on what it means for a mathematical proof to be understandable. This is used in Chapter 6 to evaluate my software and to motivate the design of the software in Chapter 3 and Chapter 4.
2.5.1. Understandability of mathematics in a broader context
What does it mean for a proof to be understandable?
An early answer to this question comes from the 19th century philosopher Spinoza.
Spinoza [Spi87[Spi87]Spinoza, BenedictThe chief works of Benedict de Spinoza (1887)publisher Chiswick Press(link)] supposes 'four levels' of a student's understanding of a given mathematical principle or rule, which are:
mechanical: The student has learnt a recipe to solve the problem, but no more than that.
inductive: The student has verified the correctness of the rule in a few concrete cases.
rational: The student comprehends a proof of the rule and so can see why it is true generally.
intuitive: The student is so familiar and immersed in the rule that they cannot comprehend it not being true.
For the purposes of this thesis I will restrict my attention to type 3 understanding.
That is, how the student digests a proof of a general result.
If the student is at level 4, and treats the result like a fish treats water, then there seems to be little an ITP system can offer other than perhaps forcing any surprising counterexamples to arise when the student attempts to formalise it.
Edwina Michener's Understanding Understanding Mathematics[Mic78[Mic78]Michener, Edwina RisslandUnderstanding understanding mathematics (1978)Cognitive science(link)] provides a wide ontology of methods for understanding mathematics.
Michener (p. 373) proposes that "understanding is a complementary process to problem solving" and incorporates Spinoza's 4-level model.
She also references Poincaré's thoughts on understanding [Poi14[Poi14]Poincaré, HenriScience and method (1914)publisher Amazon (out of copyright)(link) p. 118], from which I will take an extended quote from the original:
What is understanding? Has the word the same meaning for everybody? Does understanding the demonstration of a theorem consist in examining each of the syllogisms of which it is composed and being convinced that it is correct and conforms to the rules of the game? ...
Yes, for some it is; when they have arrived at the conviction, they will say, I understand. But not for the majority... They want to know not only whether the syllogisms are correct, but why there are linked together in one order rather than in another. As long as they appear to them engendered by caprice, and not by an intelligence constantly conscious of the end to be attained, they do not think they have understood.
In a similar spirit; de Millo, Lipton and Perlis [MUP79[MUP79]de Millo, Richard A; Upton, Richard J; Perlis, Alan JSocial processes and proofs of theorems and programs (1979)Communications of the ACM(link)] write referring directly to the nascent field of program verification (here referred to 'proofs of software')
Mathematical proofs increase our confidence in the truth of mathematical statements only after they have been subjected to the social mechanisms of the mathematical community.
These same mechanisms doom the so-called proofs of software, the long formal verifications that correspond, not to the working mathematical proof, but to the imaginary logical structure that the mathematician conjures up to describe his feeling of belief.
Verifications are not messages; a person who ran out into the hall to communicate his latest verification would rapidly find himself a social pariah.
Verifications cannot really be read; a reader can flay himself through one of the shorter ones by dint of heroic effort, but that's not reading.
Being unreadable and - literally - unspeakable, verifications cannot be internalized, transformed, generalized, used, connected to other disciplines, and eventually incorporated into a community consciousness.
They cannot acquire credibility gradually, as a mathematical theorem does; one either believes them blindly, as a pure act of faith, or not at all.
Poincaré's concern is that a verified proof is not sufficient for understanding.
De Millo et al question whether a verified proof is a proof at all!
Even if a result has been technically proven, mathematicians care about the structure and ideas behind the proof itself.
If this were not the case, then it would be difficult to explain why new proofs of known results are valued by mathematicians.
I explore the question of what exactly they value in Chapter 6.
Many studies investigating mathematical understanding within an educational context exist, see the work of Sierpinska [Sie90[Sie90]Sierpinska, AnnaSome remarks on understanding in mathematics (1990)For the learning of mathematics(link), Sie94[Sie94]Sierpinska, AnnaUnderstanding in mathematics (1994)publisher Psychology Press(link)] for a summary. See also Pólya's manual on the same topic [Pól62[Pól62]Pólya, GeorgeMathematical Discovery (1962)publisher John Wiley & Sons(link)].
2.5.2. Confidence
Another line of inquiry suggested by Poincaré's quote is distinguishing confidence in a proof from a proof being understandable.
By confidence in a proof, I do not mean confidence in the result being true, but instead confidence in the given script actually being a valid proof of the result.
As an illustrative example, I will give my own impressions on some proofs of the Jordan curve theorem which states that any non-intersecting continuous loop in the 2D Euclidean plane has an interior region and an exterior region.
Formal and informal proofs of this theorem are discussed by Hales [Hal07[Hal07]Hales, Thomas CThe Jordan curve theorem, formally and informally (2007)The American Mathematical Monthly(link)].
I am confident that the proof of the Jordan curve theorem formalised by Hales in the HOL Light proof assistant is correct although I can't claim to understand it in full.
Contrast this with the diagrammatic proof sketch (Figure 2.39) given in Hales' paper (originating with Thomassen [Tho92[Tho92]Thomassen, CarstenThe Jordan-Schönflies theorem and the classification of surfaces (1992)The American Mathematical Monthly(link)]). This sketch is more understandable to me but I am less confident in it being a correct proof (e.g., maybe there is some curious fractal curve that causes the diagrammatic proofs to stop being obvious...).
In the special case of the curve C being a polygon, the proof involves "walking along a simple polygonal arc (close to C but not intersecting C)" and Hales notes:
Nobody doubts the correctness of this argument. Every mathematician knows how to walk without running in to walls. Detailed figures indicating how to "walk along a simple polygonal arc" would be superfluous, if not downright insulting.
Yet, it is quite another matter altogether to train a computer to run around a maze-like polygon without collisions...
These observations demonstrate how one's confidence in a mathematical result is not merely a formal affair, but includes ostensibly informal arguments of correctness. This corroborates the attitude taken by De Millo et al in Section 2.5.1. Additionally, as noted in Section 1.1, confidence in results also includes a social component: a mathematician will be more confident that a result is correct if that result is well established within the field.
There has also been some empirical work on the question of confidence in proofs.
Inglis and Alcock [QED[QED]Inglis, Matthew; Alcock, LaraExpert and novice approaches to reading mathematical proofs (2012)Journal for Research in Mathematics Education(link)] performed an empirical study on eye movements in undergrads vs postgrads. A set of undergraduates and post-graduate researchers were presented with a set of natural language proofs and then asked to judge the validity of these proofs. The main outcomes they suggest from their work are that mathematicians can disagree about the validity of even short proofs and that post-graduates read proofs in a different way to undergraduates: moving their focus back and forth more. This suggests that we might expect undergraduates and postgraduates to present different reasons for their confidence in the questions.
2.5.3. Understandability and confidence within automated theorem proving.
The concepts of understandability and confidence have also been studied empirically within the context of proof assistants. This will be picked up in Chapter 6.
Stenning et al.[SCO95[SCO95]Stenning, Keith; Cox, Richard; Oberlander, JonContrasting the cognitive effects of graphical and sentential logic teaching: reasoning, representation and individual differences (1995)Language and Cognitive Processes(link)] used the graphical Hyperproof software (also discussed in Section 5.1) to compare graphical and sentence-based representations in the teaching of logic.
They found that both representations had similar transferabilityThat is, do lessons learnt in one domain transfer to anologous problems in other domains?
The psychological literature identifies this as a difficult problem in teaching. and that the best teaching representation (in terms of test scores) was largely dependent on the individual differences between the students.
This suggests that in looking for what it means for a proof to be understandable, we should not forget that people have different ways of thinking about proofs, and so there is not going to be a one-size-fits-all solution. It also suggests that providing multiple ways of conceptualising problems should help with understandability.
In Grebing's thesis [Gre19[Gre19]Grebing, Sarah CaeciliaUser Interaction in Deductive Interactive Program Verification (2019)PhD thesis (Karlsruhe Institute of Technology)(link)], a set of focus group studies are conducted to ask a set of users with a variety of experience-levels in Isabelle and KeY, to reflect on the user interfaces.
One of her main findings was that due to the extensive levels of automation in the proving process, there can arise a 'gap' between the user's model of the proof state and the proof state created through the automation.
Grebing then provides a bridge for this gap in the form of a proof scripting language and user interface for the KeY prover at a higher level of abstraction than the existing interface.
Grebing also provides a review of other empirical studies conducted on the user interfaces of proof assistants [Gre19 §6.2.0].
2.6. Human-like reasoning
How should a prover work to produce human-like mathematical reasoning?
The easiest answer is: however humans think it should reason!
The very earliest provers such as the Boyer-Moore theorem prover [BM73[BM73]Boyer, Robert S.; Moore, J. StrotherProving Theorems about LISP Functions (1973)IJCAI(link), BM90[BM90]Boyer, Robert S; Moore, J StrotherA theorem prover for a computational logic (1990)International Conference on Automated Deduction(link), BKM95[BKM95]Boyer, Robert S; Kaufmann, Matt; Moore, J StrotherThe Boyer-Moore theorem prover and its interactive enhancement (1995)Computers & Mathematics with Applications] take this approach to some extent; the design is steered through a process of introspection on how the authors would prove theorems.
Nevertheless, with their 'waterfall' architecture, the main purpose is to prove theorems automatically, rather than creating proofs that a human could follow.
Indeed Robinson's machine-like resolution method [BG01[BG01]Bachmair, Leo; Ganzinger, HaraldResolution theorem proving (2001)Handbook of automated reasoning(link)] was such a dominant approach that Bledsoe titled his paper non-resolution theorem proving[Ble81[Ble81]Bledsoe, Woodrow WNon-resolution theorem proving (1981)Readings in Artificial Intelligence(link)].
In this paper, Bledsoe sought to show another side of automated theorem proving through a review of alternative methods to resolution. A quote from this paper stands out for our current study:
It was in trying to prove a rather simple theorem in set theory by paramodulation and resolution, where the program was experiencing a great deal of difficulty, that we became convinced that we were on the wrong track. The addition of a few semantically oriented rewrite rules and subgoaling procedures made the proof of this theorem, as well as similar theorems in elementary set theory, very easy for the computer. Put simply: the computer was not doing what the human would do in proving this theorem. When we instructed it to proceed in a "human-like" way, it easily succeeded. Other researchers were having similar experiences.
This quote captures the concept of 'human-like' that I want to explore. Some piece of automation is 'human-like' when it doesn't get stuck in a way that a human would not.
Another early work on human-oriented reasoning is that of Nevins [Nev74[Nev74]Nevins, Arthur JA human oriented logic for automatic theorem-proving (1974)Journal of the ACM(link)].
Similar to this thesis, Nevins is motivated by the desire to make proofs more understandable to mathematicians.
Some examples of prover automation that are designed to perform steps that a human would take are grind for PVS[SORS01[SORS01]Shankar, Natarajan; Owre, Sam; Rushby, John M; et al.PVS prover guide (2001)Computer Science Laboratory, SRI International, Menlo Park, CA(link)] and the waterfall algorithm in ACL2[KMM13[KMM13]Kaufmann, Matt; Manolios, Panagiotis; Moore, J StrotherComputer-aided reasoning: ACL2 case studies (2013)publisher Springer].
All of the systems mentioned so far came very early in the history of computing, and had a miniscule proportion of the computing power available to us today.
Today, the concern that a piece of automation may not find a solution in a human-like way or finds a circumlocuitous route to a proof is less of a concern because computers are much more powerful.
However I think that the resource constraints that these early pioneers faced provides some clarity on why building human-like reasoning systems matters.
The designers of these early systems were forced to introspect carefully on how they themselves were able to prove certain theorems without needing to perform a large amount of compute, and then incorporated these human-inspired insights in to their designs.
My own journey into this field started with reading the work of Gowers and Ganesalingam (G&G) in their Robot prover [GG17[GG17]Ganesalingam, Mohan; Gowers, W. T.A fully automatic theorem prover with human-style output (2017)Journal of Automated Reasoning(link)]A working fork of this can be found at https://github.com/edayers/robotone..
G&G's motivation was to find a formal system that better represented the way that a human mathematician would solve a mathematics problem, demonstrating this through the ability to generate realistic natural-language write-ups of these proofs.
The system made use of a natural-deduction style hierarchical proof-state with structural sharing.
The inference rules (which they refer to as 'moves') on these states and the order in which they were invoked were carefully chosen through an introspective process.
The advantage of this approach is that the resulting proofs could be used to produce convincing natural language write-ups of the proofs. However, the system was not formalised and was limited to the domains hard-coded in to the system. The work in this thesis is a reimagining of this system within a formalised ITP system.
A different approach to exploring human-like reasoning is by modelling the process of mathematical discourse.
Pease, Cornelli, Martin, et al[CMM+17[CMM+17]Corneli, Joseph; Martin, Ursula; Murray-Rust, Dave; et al.Modelling the way mathematics is actually done (2017)Proceedings of the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Design(link), PLB+17[PLB+17]Pease, Alison; Lawrence, John; Budzynska, Katarzyna; et al.Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation (2017)Artificial Intelligence(link)] have investigated the use of graphical discourse models of mathematical reasoning.
In this thesis, however I have restricted the scope to human-like methods for solving simple lemmas that can produce machine-checkable proofs.
Another key way in which humans reason is through the use of diagrams [Jam01[Jam01]Jamnik, MatejaMathematical Reasoning with Diagrams: From Intuition to Automation (2001)publisher CSLI Press(link)] and alternative representations of mathematical proofs. A prima facie unintuitive result such as 1+2+3+⋯+n=21n(n+1) snaps together when presented with the appropriate representation in Figure 2.40.
Jamnik's previous work explores how one can perform automated reasoning like this in the domain of diagrams
Some recent work investigating and automating this process is the rep2rep project [RSS+20].
This is an important feature of general human-like reasoning, however in the name of scope management I will not explore representations further in this thesis.
2.6.1. Levels of abstraction
There have been many previous works which add higher-level abstraction layers atop an existing prover with the aim of making a prover that is more human-like.
Archer et al. developed the TAME system for the PVS prover [AH97[AH97]Archer, Myla; Heitmeyer, ConstanceHuman-style theorem proving using PVS (1997)International Conference on Theorem Proving in Higher Order Logics(link)].
Although they were focussed on proving facts about software rather than mathematics, the goals are similar: they wish to create software that produces proofs which are natural to humans.
TAME makes use of a higher abstraction level.
However, it is only applied to reasoning about timed automata and doesn't include a user study.
As part of the auto2 prover tactic for Isabelle, Zhan [Zha16[Zha16]Zhan, BohuaAUTO2, a saturation-based heuristic prover for higher-order logic (2016)International Conference on Interactive Theorem Proving(link)] developed a high-level proof script syntax to guide the automation of auto2.
A script takes the form of asserting several intermediate facts for the prover to prove before proving the main goal.
This script is used to steer the auto2 prover towards proving the result. This contrasts with tactic-based proof and structural scripts (e.g. Isar [Wen99]) which are instead instructions for chaining together tactics.
With the auto2 style script, it is possible to omit a lot of the detail that would be required by tactic-based scripts, since steps and intermediate goals that are easy for the automation to solve can be omitted entirely.
A positive of this approach is that by being implemented within the Isabelle theorem prover, the results of auto2 are checked by a kernel. However it is not a design goal of auto2 to produce proofs that a human can read.
2.6.2. Proof planning
Proof planning originated with Bundy [Bun88[Bun88]Bundy, AlanThe use of explicit plans to guide inductive proofs (1988)International conference on automated deduction(link), Bun98[Bun98]Bundy, AlanProof Planning (1998)publisher University of Edinburgh, Department of Artificial Intelligence(link)] and is the application of performing a proof with respect to a high-level plan (e.g., I am going to perform induction then simplify terms) that is generated before low-level operations commence (performing induction, running simplification algorithms). The approach follows the general field of AI planning.
AI planning in its most general conception [KKY95[KKY95]Kambhampati, Subbarao; Knoblock, Craig A; Yang, QiangPlanning as refinement search: A unified framework for evaluating design tradeoffs in partial-order planning (1995)Artificial Intelligence(link)] is the process of searching a graph G using plan-space rather than by searching it directly.
In a typical planning system, each point in plan-space is a DAGDirected Acyclic Graph of objects called ground operators or methods, each of which has a mapping to paths in G.
Each ground operator is equipped with predicates on the vertices of G called pre/post-conditions.
Various AI planning methods such as GRAPHPLAN [BF97] can be employed to discover a partial ordering of these methods, which can then be used to construct a path in G.
This procedure applied to the problem of finding proofs is proof planning.
The main issue with proof planning [Bun02] is that it is difficult to identify sets of conditions and methods that do not cause the plan space to be too large or disconnected. However, in this thesis we are not trying to construct plans for entire proofs, but just to model the thought processes of humans when solving simple equalities.
A comparison of the various proof planners is provided by Dennis, Jamnik and Pollet [DJP06].
Proof planning in the domain of finding equalities frequently involves a technique called rippling[BSV+93[BSV+93]Bundy, Alan; Stevens, Andrew; Van Harmelen, Frank; et al.Rippling: A heuristic for guiding inductive proofs (1993)Artificial Intelligence(link), BBHI05[BBHI05]Bundy, Alan; Basin, David; Hutter, Dieter; et al.Rippling: meta-level guidance for mathematical reasoning (2005)publisher Cambridge University Press(link)], in which an expression is annotated with additional structure determined by the differences between the two sides of the equation that directs the rewriting process.
The rippling algorithm captures some human intuitions about which parts of a rewriting expression are salient.
In the system for equational rewriting I introduce in Chapter 4, I avoid using rippling because the techniques are tied to peforming induction.
Another technique associated with proof planning is the concept of proof critics[Ire92[Ire92]Ireland, AndrewThe use of planning critics in mechanizing inductive proofs (1992)International Conference on Logic for Programming Artificial Intelligence and Reasoning(link)].
Proof critics are programs which take advantage of the information from a failed proof plan to construct a new, amended proof plan.
An interactive version of proof critics has also been developed [IJR99].
In the work in Chapter 3, this concept of revising a proof based on a failure is used.
Another general AI system that will be relevant to this thesis is hierarchical task networks[MS99[MS99]Melis, Erica; Siekmann, JörgKnowledge-based proof planning (1999)Artificial Intelligence(link), Tat77[Tat77]Tate, AustinGenerating project networks (1977)Proceedings of the 5th International Joint Conference on Artificial Intelligence.(link)] which are used to drive the behaviour of artificial agents such as the ICARUS architecture [LCT08].
In a hierarchical task network, tasks are recursively refined into subtasks, which are then used to find fine-grained methods for achieving the original tasks, eventually bottoming out in atomic actions such as actuating a motor.
HTNs naturally lend themselves to human-like reasoning, and I will make use of these in designing a hierarchical algorithm for performing equational reasoning.
2.7. Natural language for formal mathematics
In this section I will survey the background and related work on using natural language to generate proofs.
The material in this chapter will be used in Section 3.6 and Chapter 6.
2.7.1. Natural language generation in a wider context
Data-to-text natural language generation (NLG) is a subfield of natural language processing (NLP) that focusses on the problem of computing intelligible natural language discourses and text from some non-textual object (without a human in the loop!). An example is producing an English description of the local weather forecast from meteorological data.
NLG techniques can range from simple 'canned text' and 'mail-merge' applications right up to systems with aspirations of generality such as modern voice recognition in smartphones.
There are a wide variety of architectures available for modern NLG [GK18[GK18]Gatt, Albert; Krahmer, EmielSurvey of the state of the art in natural language generation: Core tasks, applications and evaluation (2018)Journal of Artificial Intelligence Research(link)], however they usually carry a modular structure, with a backbone [RD00] being split in to three pipeline stages as shown in Figure 2.41.
[RD00]Reiter, Ehud; Dale, RobertBuilding natural language generation systems (2000)publisher Cambridge University Press(link)
Macro-planner or discourse planner: dictates how to structure the general flow of the text, that is, serialising the input data.
These often take the form of 'expert systems' with a large amount of domain specific knowledge encoded.
Micro-planner: determines how the stream of information from the macro-planner should be converted into individual sentences, how sentences should be structured and determining how the argument should 'flow'.
Realiser: produces the final text from the abstracted output of the micro-planner, for example, applying punctuation rules and choosing the correct conjugations.
These choices of stages are mainly motivated through a desire to reuse code and to separate concerns (a realiser does not need to know the subject of the text it is correcting the punctuation from). I make use of this architecture in Section 3.6.
An alternative approach to the one outlined above is to use statistical methods for natural language generation.
The advent of scalable machine learning (ML) and neural networks (NNs) of the 2010s has gained dominance in many NLG tasks such as translation and scene description.
The system developed for this work in Section 3.6 is purely classical, with no machine learning component.
In the context of producing simple write-ups of proofs, there will likely be some gains from including ML, but it is not clear that a statistical approach to NLG is going to assist in building understandable descriptions of proofs, because it is difficult to formally confirm that the resulting text generated by a black-box NLG component is going to accurately reflect the input.
2.7.2. Natural language generation for mathematics
The first modern study of the linguistics of natural language mathematics is the work of Ranta [Ran94[Ran94]Ranta, AarneSyntactic categories in the language of mathematics (1994)International Workshop on Types for Proofs and Programs(link), Ran95[Ran95]Ranta, AarneContext-relative syntactic categories and the formalization of mathematical text (1995)International Workshop on Types for Proofs and Programs(link)] concerning the translation between dependent type theory and natural language and I will use some of his insights in Section 3.6. Ganesalingam's thesis [Gan10[Gan10]Ganesalingam, MohanThe language of mathematics (2010)PhD thesis (University of Cambridge)(link)] is an excellent reference for understanding the linguistics of mathematics in general, however it is more concerned with natural language input.
There have been numerous previous attempts at creating natural language output from a theorem prover:
Felty-Miller [FM87[FM87]Felty, Amy; Miller, DaleProof explanation and revision (1987)Technical Report(link)], Holland-Minkley et al within the NuPrl prover[HBC99[HBC99]Holland-Minkley, Amanda M; Barzilay, Regina; Constable, Robert LVerbalization of High-Level Formal Proofs. (1999)AAAI/IAAI(link)], and also in Theorema [BCJ+06[BCJ+06]Buchberger, Bruno; Crǎciun, Adrian; Jebelean, Tudor; et al.Theorema: Towards computer-aided mathematical theory exploration (2006)Journal of Applied Logic(link)].
A particularly advanced NLG for provers was Proverb [HF97[HF97]Huang, Xiaorong; Fiedler, ArminProof Verbalization as an Application of NLG (1997)International Joint Conference on Artificial Intelligence(link)] for the Ωmega theorem prover [BCF+97[BCF+97]Benzmüller, Christoph; Cheikhrouhou, Lassaad; Fehrer, Detlef; et al.Ωmega: Towards a mathematical assistant (1997)Automated Deduction - CADE-14(link)], this system's architecture uses the pipeline in Figure 2.41 and takes as input a proof term generated by the Ωmega toolchain and outputs a natural language sentence.
An issue with these generation tools is that their text will often produce text that does not appear natural at the macro-level. That is, the general structure of the argument will be different to what would be found in a mathematical textbook. G&G illustrate some examples of this in their paper [GG17 §2].
The process of synthesising natural language is difficult in the general case.
But as G&G [GG17] note, the language found in mathematical proofs is much more restricted than a general English text.
At its most basic, a natural language proof is little more than a string of facts from the assumptions to the conclusion.
There is no need for time-sensitive tenses or other complexities that arise in general text.
Proofs are written this way because mathematical proofs are written to be checked by a human and so a uniformity of prose is used that minimises the chance of 'bugs' creeping in.
This, combined with a development calculus designed to encourage human-like proof steps, makes the problem of creating mathematical natural language write-ups much more tenable.
I will refer to these non-machine-learning approaches as 'classical' NLG.
A related problem worth mentioning here is the reverse process of NLG: parsing formal proofs and theorem statements from a natural language text.
The two problems are interlinked in that they are both operating on the same grammar and semantics, but parsing raises a distinct set of problems to NLG, particularly around ambiguity [Gan10 ch. 2].
Within mathematical parsing there are two approaches. The first approach is controlled natural language[Kuh14[Kuh14]Kuhn, TobiasA survey and classification of controlled natural languages (2014)Computational linguistics(link)] as practiced by ForTheL [Pas07[Pas07]Paskevich, AndreiThe syntax and semantics of the ForTheL language (2007)PhD thesis (Université Paris XII)(link)] and Naproche/SAD [CFK+09[CFK+09]Cramer, Marcos; Fisseni, Bernhard; Koepke, Peter; et al.The Naproche Project: Controlled Natural Language Proof Checking of Mathematical Texts (2009)Controlled Natural Language, Workshop on Controlled Natural Language(link)].
Here, a grammar is specified to parse text that is designed to look as close to a natural langauge version of the text as possible.
The other approach (which I will not make use of in this thesis) is in using machine learning techniques, for example the work on parsing natural mathematical texts is in the work of Stathopoulos et al[ST16[ST16]Stathopoulos, Yiannos A; Teufel, SimoneMathematical information retrieval based on type embeddings and query expansion (2016)COLING 2016(link), SBRT18[SBRT18]Stathopoulos, Yiannos; Baker, Simon; Rei, Marek; et al.Variable Typing: Assigning Meaning to Variables in Mathematical Text (2018)NAACL-HLT 2018(link)].
In Section 3.6 I will make use of some ideas from natural language parsing, particularly the concept called notion by ForTheL and non-extensional type by Ganesalingam. A non-extensional type is a noun-phrase such as "element of a topological space" or "number" which is assigned to expressions, these types are not used by the underlying logical foundation but are used to parse mathematical text. To see why this is needed consider the syntax xy. This is parsed to an expression differently depending on the types of x and y (e.g., if x is a function vs. an element of a group). Non-extensional types allow this parse to be disambiguated even if the underlying foundational language does not have a concept of a type.
2.8. Chapter summary
In this chapter I have provided the necessary background information and prior work needed to frame the rest of the thesis.
I have explained the general design of proof assistants (Section 2.1).
I have described a meta-level pseudolanguage for constructing algorithms (Section 2.2) and provided some gadgets for working with inductive types within it (Section 2.3).
I have also presented the philosophy and social aspects of understandability in mathematics (Section 2.5); human-like automated reasoning (Section 2.6); and natural language generation of mathematical text (Section 2.7).
Chapter 3
A development calculus
Now that we have reviewed the requisite background material, I can define the moving parts of a human-like theorem prover.
The driving principle is to find ways of representing proofs at the same level of detail that a human mathematician would use to communicate to colleagues.
The contributions of this chapter are:
The Box datastructure, a development calculus (Section 3.3) designed to better capture how humans reason about proofs while also being formally sound.
A set of inference rules on Box which preserve this soundness (Section 3.5).
A natural language write-up component converting proof objects created with this layer to an interactive piece of text (Section 3.6).
In the supplementary Appendix A, an 'escape hatch' from the Box datastructure to a metavariable-oriented goal state system as used by Lean (Section 3.4.4, Appendix A). This enables compatibility between Box-style proofs and existing automation and verification within Lean.
HumanProof integrates with an existing proof assistant (in this case Lean).
By plugging in to an existing prover, it is possible to gain leverage by utilising the already developed infrastructure for that prover such as parsers, tactics and automation.
Using an existing prover also means that the verification of proofs can be outsourced to the prover's kernel.
The first research question of Section 1.2 was to investigate what it means for a proof to be human-like.
I provided a review to answer this question in Section 2.6.
Humans think differently to each other, and I do not wish to state that there is a 'right' way to perform mathematics.
However, I argue that there are certain ways in which the current methods for performing ITP should be closer to the general cluster of ways in which humans talk about and solve problems.
In this chapter I investigate some ways in which the inference rules that provers use could be made more human-like, and then introduce a new proving abstraction layer, HumanProof, written in the Lean 3 theorem prover, implementing these ideas.
Later, in Chapter 6, I gather thoughts and ratings from real mathematicians about the extent to which the developed system achieves these goals.
In Section 3.1, I first present an example proof produced by a human to highlight the key features of 'human-like' reasoning that I wish to emulate.
Then in Section 3.2 I give an overview of the resulting designs and underline the primary design decisions and the evidence that drives them.
In Section 3.3 I provide the details and theory of how the system works through defining the key Box structure and tactics on Boxes.
The theory behind creating valid proof terms from Boxes is presented in Section 3.4 as well as how to run standard tactics within Boxes (Section 3.4.4).
This theoretical basis will then be used to define the human-like tactics in Section 3.5.
Then, I will detail the natural language generation pipeline for HumanProof in Section 3.6.
3.1. Motivation
Building on the background where I explored the literature on the definition of 'human-like' (Section 2.6) and 'understandable' (Section 2.5.1) proofs, my goal in this section is find some specific improvements to the way in which computer aided mathematics is done. I use these improvements to motivate the design choices of the HumanProof system.
3.1.1. The need for human-like systems
In Section 1.1, I noted that non-specialist mathematicians have yet to widely accept proof assistants despite the adoption of other tools such as computer algebra systems.
Section 1.1 presented three problems that mathematicians have with theorem provers: differing attitudes on correctness, a high learning cost to learning to use ITP and a low resulting reward -- learning the truth of something that they 'knew' was true anyway.
One way in which to improve this situation is to reduce the cost of learning to use proof assistants through making the way in which they process proofs more similar to how a human would process proofs, making the proofs more closely match what the mathematician already knows.
Making a prover which mimics a human's thought process also helps overcome the problem of differing attitudes of correctness.
Requiring a human-like approach to reasoning means that many automated reasoning methods such as SMT-solvers and resolution (see Section 2.6) must be ruled out.
In these machine-oriented methods, the original statement of the proposition to be proved is first reduced to a normal form and mechanically manipulated with a small set of inference rules.
The resulting proof is scarcely recognisable to a mathematician as a proof of the proposition, even if it is accepted by the kernel of a proof assistant.
As discussed in Section 1.1, Section 2.5 and as will be confirmed in Chapter 6, mathematicians do not care just about a certificate that a statement is correct but also about the way in which the statement is correct.
Given some new way of creating proofs; how can we determine whether these created proofs are more 'human-like' than some other system?
The way I propose here is to require that the program be able to imitate the reasoning of humans at least well enough to produce convincing natural language write-ups of the proofs that it generates, and then to test how convincing these write-ups are through asking mathematicians.
This approach is shared by the previous work of Gowers and Ganesalingam [GG17[GG17]Ganesalingam, Mohan; Gowers, W. T.A fully automatic theorem prover with human-style output (2017)Journal of Automated Reasoning(link)]Gowers and Ganesalingam is abbreviated G&G., where they use a similar framework to the HumanProof system presented in this thesis to produce natural language write-ups of proofs for some lemmas in the domain of metric space topology.
The work presented in this thesis builds significantly on the work of G&G.
3.1.2. Modelling human-like reasoning
One of the key insights of Gowers and Ganesalingam is that humans reason with a different 'basis' of methods than the logical operations and tactics that are provided to the user of an ITP.
For example, a hypothesis such as a function f:X→Y being continuous expands to a formula (3.1) with interlaced quantifiers.
However in a mathematical text, if one needs to prove d(f(x),f(y))<ε, the hypothesis that f is continuous will be applied in one go. That is, a step involving (3.1) would be written as "Since f is continuous, there exists a δ>0 such that d(f(x),f(y))<ε whenever d(x,y)<δ". Whereas in an ITP this process will need to be separated in to several steps: first show x∈X, then obtain δ, then show d(x,y)<δ.
Another example with the opposite problem is the automated tactics such as the tableaux prover blast[Pau99[Pau99]Paulson, Lawrence CA generic tableau prover and its integration with Isabelle (1999)Journal of Universal Computer Science(link)].
The issue with tactics is that their process is opaque and leaves little explanation for why they succeed or fail.
They may also step over multiple stages that a human would rather see spelled out in full.
The most common occurrence of this is in definition expansion; two terms may be identical modulo definition expansion but a proof found in a textbook will often take the time to point out when such an expansion takes place.
This points towards creating a new set of inference rules for constructing proofs that are better suited for creating proofs by corresponding better to a particular reasoning step as might be used by a human mathematician.
3.1.3. Structural sharing
Structural sharing is defined as making use of the same substructure multiple times in a larger structure.
For example, a tree with two branches being the same would be using structural sharing if the sub-branches used the same object in memory.
Structural sharing of this form is used frequently in immutable datastructures for efficiency.
However here I am interested in whether structural sharing has any applications in human-like reasoning.
When humans reason about mathematical proofs, they often flip between forwards reasoning and backwards reasoningBroadly speaking, forwards reasoning is any mode of modifying the goal state that acts only on the hypotheses of the proof state. Whereas backwards reasoning modifies the goals..
The goal-centric proof state used by ITPs can make this kind of reasoning difficult.
In the most simple example, suppose that the goal is P ∧ Q ⊢ Q ∧ PThat is, given the hypothesis P ∧ Q, prove Q ∧ P where P and Q are propositions and ∧ is the logical-and operation..
One solution is to perform a split on the goal to produce P ∧ Q ⊢ Q and P ∧ Q ⊢ P.
However, performing a conjunction elimination on the P ∧ Q hypothesis will then need to be performed on both of the new goals.
This is avoided if the elimination is performed before splitting P ∧ Q.
In this simplified example it is clear which order the forwards and backwards reasoning should be performed.
But in more complex proofs, it may be difficult to see ahead how to proceed.
A series of backwards reasoning steps may provide a clue as to how forwards reasoning should be applied.
The usual way that this problem is solved is for the human to edit an earlier part of the proof script with the forwards reasoning step on discovering this.
I reject this solution because it means that the resulting proof script no longer represents the reasoning process of the creator.
The fact that the forwards reasoning step was motivated by the goal state at a later point is lost.
The need to share structure among objects in the name of efficiency has been studied at least as far back as Boyer and Moore [BM72[BM72]Boyer, R. S.; Moore, J. S.The sharing structure in theorem-proving programs (1972)Machine intelligence(link)]. However, the motivation behind introducing it here is purely for the purpose of creating human-like proofs.
The solution that I propose here is to use a different representation of the goal state that allows for structural sharing.
This alteration puts the proof state calculus more in the camp of OLEG [McB00[McB00]McBride, ConorDependently typed functional programs and their proofs (2000)PhD thesis (University of Edinburgh)(link)], and the G&G prover.
The details of the implementation of structural sharing are presented later in Section 3.5.4.
Structural sharing can also be used to implement backtracking and counterfactuals.
For example, suppose that we need to prove A ⊢ P ∨ Q, one could apply the ∨-left-introduction rule P ⇒ P ∨ Q, but then one might need to backtrack later in the event that really the right-introduction rule Q ⇒ P ∨ Q should be used instead.
Structural sharing lets us split a goal into two counterfactuals.
3.1.4. Verification
One of the key benefits of proof assistants is that they can rigorously check whether a proof is correct.
This distinguishes the HumanProof project from the prior work of G&G, where no formal proof checking was present.
While I have argued in Section 2.5 (and will later be suggested from the results of my user study in Section 6.6) that this guarantee of correctness is less important for attracting working mathematicians, there need not be a conflict between having a prover which is easy for non-specialists to understand and which is formally verified.
3.1.5. What about proof planning?
Proof planning is the process of creating proofs using abstract proof methods that are assembled with the use of classical AI planning algorithms[RN10]Russell, Stuart J.; Norvig, PeterArtificial Intelligence - A Modern Approach (2010)publisher Pearson Education(link)An introduction to classical AI planning can be found in Russel and Norvig [RN10 Pt.III]..
The concept of proof planning was first introduced by Bundy [Bun88[Bun88]Bundy, AlanThe use of explicit plans to guide inductive proofs (1988)International conference on automated deduction(link)].
A review of proof planning is given in Section 2.6.2.
The advantage of proof planning is that it represents the way in which a problem will be solved at a much more abstract level, more like human mathematicians.
The primary issue with proof planning is that there is a sharp learning curve.
In order to get started with proof plans, one must learn a great deal of terminology and a new way of thinking about formalised mathematics.
The user has to familiarise themselves with the way in which proof methods are used to construct proof plans and how to diagnose malformed plans for their particular problems.
Bundy presents his own critique of proof planning [Bun02[Bun02]Bundy, AlanA critique of proof planning (2002)Computational Logic: Logic Programming and Beyond(link)] which goes in to more detail on this point.
The study of proof planning has fallen out of favour for the 21st century so far, possibly in relation to the rise of practical SMT solvers such as E prover[SCV19[SCV19]Schulz, Stephan; Cruanes, Simon; Vukmirović, PetarFaster, Higher, Stronger: E 2.3 (2019)Proc. of the 27th CADE, Natal, Brasil(link)] and Z3 prover[MB08[MB08]de Moura, Leonardo; Bjørner, NikolajZ3: An efficient SMT solver (2008)International conference on Tools and Algorithms for the Construction and Analysis of Systems(link)] and their incorporation in to ITP through the use of 'hammer' software like Isabelle's Sledgehammer [BN10[BN10]Böhme, Sascha; Nipkow, TobiasSledgehammer: judgement day (2010)International Joint Conference on Automated Reasoning(link)].
I share a great deal of the ideals that directed proof planning and the equational reasoning system presented in Chapter 4 is inspired by it.
I take a more practical stance; the additional abstractions that are placed atop the underlying tactic system should be transparent, in that they are understandable without needing to be familiar with proof planning and with easy 'escape hatches' back to the tactic world if needed.
This design goal is similar to that of the X-Barnacle prover interface [LD97[LD97]Lowe, Helen; Duncan, DavidXBarnacle: Making Theorem Provers More Accessible (1997)14th International Conference on Automated Deduction(link)] (discussed later in Section 5.1), where a GUI is used to present an explorable representation of a proof plan.
3.2. Overview of the software
The software implementation of the work presented in this thesis is called 'HumanProof' and is implemented using the Lean 3 prover.
The source code can be found at https://github.com/edayers/lean-humanproof-thesis.
In this section I give a high-level overview of the system and some example screenshots.
A general overview of the system and how it relates to the underlying Lean theorem prover is shown in Figure 3.2.
Given a theorem to prove, HumanProof is invoked by indicating a special begin[hp] script block in the proof document (see Figure 3.3).
This initialises HumanProof's Box datastructure with the assumptions and goal proposition of the proof.
The initial state of the prover is shown in the goal view of the development environment, called the Info View (the right panel of Figure 3.3).
Using the ProofWidgets framework (developed in Chapter 5), this display of the state is interactive: the user can click at various points in the document to determine their next steps.
Users can then manipulate this datastructure either through the use of interactive buttons or by typing commands in to the proof script in the editor.
In the event of clicking the buttons, the commands are immediately added to the proof script sourcefile as if the user had typed it themselves (the left panel of Figure 3.3).
In this way, the user can create proofs interactively whilst still preserving the plaintext proof document as the single-source-of-truth; this ensures that there is no hidden state in the interactive view that is needed for the Lean to reconstruct a proof of the statement.
While the proof is being created, the system also produces a natural language write-up (labelled 'natural language writeup' in Figure 3.2) of the proof (Section 3.6) that is displayed alongside the proof state. As the proof progresses, users can see the incomplete natural language proof get longer too.
The system also comes equipped with a module for solving equalities using the 'subtasks algorithm' (Chapter 4); labelled 'subtasks' on Figure 3.2.
The subtasks algorithm uses a hierarchical planning (see Section 2.6.2) system to produce an equality proof that is intended to match the way that a human would create the proof, as opposed to a more machine like approach such as E-matching [BN98[BN98]Baader, Franz; Nipkow, TobiasTerm rewriting and all that (1998)publisher Cambridge University Press(link) Ch. 10].
The output of this subsystem is a chain of equations that is inserted into the natural language writeup.
3.3. The Box datastructure
At the heart of HumanProof is a development calculus using a datastructure called Box.
The considerations from Section 3.1.3 led to the development of an 'on-tree' development calculus.
Rather than storing a flat list of goals and a metavariable context alongside the result, the entire development state is stored in a recursive tree structure which I call a Box.
The box tree, to be defined in Section 3.3.2, stores the proof state as an incomplete proof tree with on-tree metavariable declarations which is then presented to the user as a nested set of boxes.
3.3.1. An example of Box in action.
Before defining boxes in Section 3.3.2, let's look at a simple example.
Boxes are visualised as a tree of natural-deduction-style goal states.
Let's start with a minimal example to get a feel for the general progression of a proof with the Box architecture.
Let's prove P ∨ Q → Q ∨ P using Boxes.
The initial box takes the form (3.4).
And we can read (3.4) as saying "we need to show P ∨ Q → Q ∨ P".
The ?𝑡 is the name of the metavariable that the proof of this will be assigned to.
The first action is to perform an intro step to get (3.5).
To be read as "Given P ∧ Q, we need to show Q ∨ P".
So far the structure is the same as would be observed on a flat goal list structure.
The idea is that everything above a horizontal line is a hypothesis (something that we have) and everything below is a goal (something we want).
When all of the goals are solved, we should have a valid proof of the original goal.
At this point, we would typically perform an elimination step on ℎ (e.g., casesℎ in Lean) (3.6).
Here in (3.6) we can see nested boxes, each nested box below the horizontal line must be solved to solve the parent box.
However, in the box architecture there is an additional step available; a branching on the goal (3.7).
If a pair of boxes appear with a ⋁ between them, then either of the boxes can be solved to solve the parent box.
And then we can eliminate h on the branched box:
Now at this point, we can directly match ₁ with ?𝑡₁₂ and ₂ with ?𝑡₂₁ to solve the box.
Behind the scenes, the box is also producing a result proof term that can be checked by the proof assistant's kernel.
3.3.2. Definition of Box
The above formulation is intended to match with the architecture designed in G&G, so that all of the same proof-steps developed in G&G are available.
Unlike G&G, the system also interfaces with a flat goal-based development calculus, and so it is possible to use both G&G proof-steps and Lean tactics within the same development calculus.
To do this, let's formalise the system presented above in Section 3.3.1 with the following Box datatype (3.9).
Define a Binder:=(name:Name) × (type:Expr) to be a name identifier and a type with notation (name∶type), using a smaller colon to keep the distinction from a meta-level type annotation.
I will represent instances of the Box type with a 2D box notation defined in (3.10) to make the connotations of the datastructure more apparent.
These visualisations are also presented directly to the user through the use of the widgets UI framework presented in Chapter 5.
The details of this visualisation are given in Section 5.8.
To summarise the roles for each constructor:
ℐ 𝑥𝑏 is a variable introduction binder, that is, it does the same job as a lambda binder for expressions and is used to introduce new hypotheses and variables.
𝒢 𝑚𝑏 is a goal binder, it introduces a new metavariable ?𝑚 that the child box depends on.
𝑟 is the result box, it depends on all of the variables and goals that are declared above it. It represents the proof term that is returned once all of the goal metavariables are solved. Extracting a proof term from a well-formed box will be discussed in Section 3.4.
𝒜 𝑏₁(𝑥 ∶ α)𝑏₂ is a conjunctive pair of boxes. Both boxes have to be solved to complete the proof. Boxb₂ depends on variable 𝑥. When 𝑏₁ is solved, the 𝑥 value will be replaced with the resulting proof term of 𝑏₁.
𝒪 𝑏₁𝑏₂ is a disjunctive pair, if either of the child boxes are solved, then so is the total box. This is used to implement branching and backtracking.
𝒱 𝑥𝑏 is a value binder. It introduces a new assigned variable.
Boxes also have a set of well-formed conditions designed to follow the typing judgements of the underlying proof-assistant development calculus.
This will be developed in Section 3.4.
3.3.3. Initialising and terminating a Box
Given an expression representing a theorem statement P:Expr, ∅ ⊢ P ∶ Prop, we can initialise a box to solve P as 𝑏₀:= 𝒢 (𝑡 ∶ P)( 𝑡)(3.11).
In the case that P also depends on a context of hypotheses Γ ⊢ P ∶ Prop, these can be incorporated by prepending to the initial 𝑏₀ in (3.11) with an ℐ box for each ∈ Γ.
For example, if Γ=[(𝑥∶α),(𝑦∶β)] then send 𝑏₀ to ℐ (𝑥∶α), ℐ (𝑦∶β),𝑏₀.
Say that a Box is solved when there are no 𝒢-binders remaining in the Box. At this point, the proving process ceases and a proof term and natural language proof may be generated.
3.3.4. Transforming a Box
The aim is to solve a box through the use of a sequence of sound transformations on it.
Define a box-tactic is a partial function on boxes BoxTactic:=Box → OptionBox.
Box-tactics act on Boxes in the same way that tactics act on proof states.
That is, they are functions which act on a proof-state (i.e., a representation of an incomplete proof) in order to prove a theorem.
This is to make it easier to describe how box-tactics interface with tactics in Section 3.4 and Appendix A.
In Section 3.3.1 we saw some examples of box-tactics to advance the box state and eventually complete it.
A complete set of box-tactics that are implemented in the system will be given in Section 3.5.
As with tacticsAt least, tactics in a 'checker' style proof assistant such as Lean. See Section 2.1 for more information., there is no guarantee that a particular box-tactic will produce a sound reasoning step; some box-tactics will be nonsense (for example, a box-tactic that simply deletes a goal) and not produce sound proofs.
In Section 3.4 I will define what it means for a box-tactic to be sound and produce a correct proof that can be checked by the ITP's kernel.
3.3.5. Relation to other development calculi
Thee Box calculus's design is most similar to McBride's OLEG [McB00[McB00]McBride, ConorDependently typed functional programs and their proofs (2000)PhD thesis (University of Edinburgh)(link)] and G&G's prover [GG17[GG17]Ganesalingam, Mohan; Gowers, W. T.A fully automatic theorem prover with human-style output (2017)Journal of Automated Reasoning(link)].
A more abstract treatment can be found in the work of Sterling and Harper [SH17[SH17]Sterling, Jonathan; Harper, RobertAlgebraic Foundations of Proof Refinement (2017)CoRR(link)], implemented within the RedPRL theorem prover.
The novel contribution of the Box calculus developed here is that it works within a Spiwack-style [Spi11[Spi11]Spiwack, ArnaudVerified computing in homological algebra, a journey exploring the power and limits of dependent type theory (2011)PhD thesis (INRIA)(link)]See Section 2.4 for more background information. flat metavariable context model as is used in Lean.
That is, it is a layer atop the existing metavariable context system detailed in Section 2.4.3.
This means that it is possible for the new calculus to work alongside an existing prover, rather than having to develop an entirely new one as was required for OLEG and the G&G prover.
This choice opens many possibilities: now one can leverage many of the advanced features that Lean offers such as a full-fledged modern editor and metaprogramming toolchain [EUR+17[EUR+17]Ebner, Gabriel; Ullrich, Sebastian; Roesch, Jared; et al.A metaprogramming framework for formal verification (2017)Proceedings of the ACM on Programming Languages(link)].
This approach also reduces some of the burden of correctness pressed upon alternative theorem provers, because we can outsource correctness checking to the Lean kernel.
Even with this protection, it is still frustrating when a development calculus produces an incorrect proof and so I will also provide some theoretical results in Section 3.4 and Appendix A on conditions that must be met for a proof step to be sound.
The design of the Box calculus is independent of any particular features of Lean, and so a variant of it may be implemented in other systems.
The central datatype is the Box. This performs the role of holding a partially constructed proof object and a representation of the goals that remain to be solved.
As discussed in Section 3.1.3, the purpose is to have a structurally shared tree of goals and assumptions that is also compatible with Lean tactics.
McBride's OLEG [McB00[McB00]McBride, ConorDependently typed functional programs and their proofs (2000)PhD thesis (University of Edinburgh)(link)] is the most similar to the design presented here.
OLEG 'holes' are functionally the same as metavariables.
That is, they are specially tagged variables that will eventually be assigned with expressions.
OLEG provides an additional constructor for expressions called 'hole-bindings' or '?-bindings'.
Because OLEG is a ground-up implementation of a new theorem prover, hole-bindings can be added directly as constructors for expressions. This is not available in Lean (without reimplementing Lean expressions and all of the algorithms)It might be possible to use Lean's expression macro system to implement hole-bindings, but doing so would still require reimplementing a large number of type-context-centric algorithms such as unification [SB01].[SB01]Snyder, Wayne; Baader, FranzUnification theory (2001)Handbook of automated reasoning(link).
These hole-bindings perform the same role as the 𝒢 constructor in that they provide the context of variables that the hole/metavariable is allowed to depend on.
But if the only purpose of a hole-binding is to give a context, then why not just explicitly name that context as is done in other theorem provers?
The Box architecture given above is intended to give the best of both worlds, in that you still get a shared goal-tree structure without needing to explicitly bind metavariables within the expression tree.
Instead they are bound in a structure on top of it.
Lean and Coq's proof construction systems make use of the metavariable context approach outlined in Section 2.4.
The metavariable context here performs the same role as the 𝒢 goal boxes, however this set of goals is flattened in to a list structure rather than stored in a tree as in Box.
This makes many aspects such as unification easier but means that structural sharing (Section 3.1.3) is lost.
In Section 3.4.4 I show that we do not have to forgo use of the algorithms implemented for a flat metavariable structure to use Boxes.
In Isabelle, proofs are constructed through manipulating the proof state directly through an LCF-style [Mil72[Mil72]Milner, RobinLogic for computable functions description of a machine implementation (1972)Technical Report(link)] kernel of available functionsAs can be seen in the source https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Pure/thm.ML.. Schematic variables are used to create partially constructed terms.
Sterling and Harper [SH17[SH17]Sterling, Jonathan; Harper, RobertAlgebraic Foundations of Proof Refinement (2017)CoRR(link)] provide a category-theoretical theory of partially constructed proofs and use these principles in the implementation of RedPRL.
They are motivated by the need to create a principled way performing refinement of proofs in a dependently-typed foundation.
They develop a judgement-independent framework for describing development calculi within a category-theoretical setting.
Another hierarchical proof system is HiProof [ADL10[ADL10]Aspinall, David; Denney, Ewen; Lüth, ChristophTactics for hierarchical proof (2010)Mathematics in Computer Science(link)]. HiProof makes use of a tree to write proofs. The nodes of a tree are invocations of inference rules and axioms and an edge denotes the flow of evidence in the proof. These nodes may be grouped to provide varying levels of detail. These hierarchies are used to describe a proof, whereas a Box here describes a partially completed proof and a specification of hypotheses and goals that must be set to construct the proof.
3.4. Creating valid proof terms from a Box
Note that because we are using a trusted kernel, the result of producing an invalid proof with Box is a mere inconvenience because the kernel will simply reject it.
However, in order for the Box structure defined in Section 3.3.2 to be useful within a proof assistant such as Lean as motivated by Section 3.1.4, it is important to make sure that a solved Box produces a valid proof for the underlying trusted kernel.
To do this, I will define a typing judgement 𝑀;Γ ⊢ 𝑏 ∶ α and then present a method for extracting a proof term 𝑀;Γ ⊢ 𝑟 ∶ α from 𝑏 with the same type provided 𝑏 is solved.
3.4.1. Assignability for Box
In Section 2.4.2, I introduced the concept of an assignable datastructure for generalising variable-manipulation operations to datatypes other than expressions.
We can equip a datatype containing expressions with an assignability structure assign(3.12).
This is a variable-context-aware traversal over the expressions present for the datatype.
For Box, this traversal amounts to traversing the expressions in each box, while adding to the local context if the subtree is below a binder.
The definition of assign induces a definition of variable substitution and abstraction over Boxes.
3.4.2. Typing judgements for Box
In Section 2.4, I defined contexts Γ, metavariable contexts 𝑀.
As covered in Carneiro's thesis [Car19[Car19]Carneiro, MarioLean's Type Theory (2019)Masters' thesis (Carnegie Mellon University)(link)], Lean's type theory affords a set of inference rules on typing judgements Γ ⊢ 𝑡 ∶ α, stating that the expression 𝑡 has the type α in the context Γ.
However, these inference rules are only defined for expressions 𝑡:Expr that do not contain metavariables.
In Appendix A.1, I extend these judgements (A.10), (A.11) to also include expressions containing metavariable contexts 𝑀;Γ ⊢ 𝑡 ∶ α.
In a similar way, we can repeat this for Box: given contexts 𝑀 and Γ we can define a typing judgement 𝑀;Γ ⊢ 𝑏 ∶ β where 𝑏:Box and β is a type.
The inference rules for this are given in (3.13).
These have been chosen to mirror the typings given in Section 2.4.3.
These typing rules have been designed to match the typing rules (A.10) of the underlying proof terms that a Box produces when solved, as I will show next.
3.4.3. Results of a Box
The structure of Box is designed to represent a partially complete expression without the use of unbound metavariables.
Boxes can be converted to expressions containing unbound metavariables using results:Box → SetExpr as defined in (3.14).
A 𝑏:Box is solved when there are no remaining 𝒢 entries in it.
When 𝑏 is solved, the set of results for 𝑏 does not contain any metavariables and hence can be checked by the kernel.
In the case that 𝑏 is unsolved, the results of 𝑏 contain unbound metavariables. Each of these metavariables corresponds to a 𝒢-binder that needs to be assigned.
Lemma 3.15 (compatibility): Suppose that 𝑀;Γ ⊢ 𝑏:α for 𝑏:Box as defined in (3.13).
Then [..𝑀,..goals𝑏];Γ ⊢ 𝑟 ∶ α.
(Say that 𝑏 is compatible with 𝑟 ∈ results𝑏.)
Here, goals𝑏 is the set of metavariable declarations formed by accumulating all of the 𝒢-binders in 𝑏.
(3.16) shows a formal statement of Lemma 3.15.
Lemma 3.15 states that given a box 𝑏 and an expression 𝑟 that is a result of 𝑏,
then if 𝑏 is a valid box with type α then 𝑟 will type to α too in the metavariable context including all of the goals in 𝑏.
Lemma 3.15 is needed because it ensures that our Box will produce well-typed expressions when solved.
Using Lemma 3.15, we can find box-tacticsm:Box → OptionBox - partial functions from Box to Box - such that 𝑀;Γ ⊢ 𝑏 ∶ α ⇒ 𝑀;Γ ⊢ m𝑏 ∶ α whenever 𝑏 ∈ domm.
Hence a chain of such box-tactic applications will produce a result that satisfies the initial goal.
Proof: Without loss of generality, we only need to prove Lemma 3.15 for a 𝑏:Box with no 𝒪 boxes and a single result [𝑟]=results𝑏.
To see why, note that any box containing an 𝒪 can be split as in (3.17) until each Box has one result.
Then we may prove Lemma 3.15 for each of these in turn.
Write result𝑏 to mean this single result 𝑟.
Performing induction on the typing judgements for boxes, the most difficult is 𝒜-typing, where we have to show (3.18).
where 𝑀' :=[..𝑀,..goals(𝒜 𝑏₁(𝑥∶α)𝑏₂)].
To derive this it suffices to show that result is a 'substitution homomorphism':
where σ is a substitutionSee Section 2.4.1.
A substitution is a partial map from variables to expressions. in context Γ and
≡ is the definitional equality judgement under Γ.
Then we have
We can see the substitution homomorphism property of result holds by inspection on the equations of result, observing that each LHS expression behaves correctly.
Here is the case for ℐ:
This completes the proof of Lemma 3.15. By using compatibility, we can determine whether a given box-tactic m:Box → OptionBox is sound.
Define a box-tactic m to be sound when for all 𝑏 ∈ domm we have some α such that 𝑀;Γ ⊢ (m𝑏) ∶ α whenever 𝑀;Γ ⊢ 𝑏 ∶ α.
Hence, to prove a starting propositionOr, in general, a type α.P, start with an initial box 𝑏₀:= 𝒢 (?t₀∶P)( ?t₀).
Then if we only map 𝑏₀ with sound box-tactics to produce a solved box 𝑏ₙ, then each of results𝑏ₙ always has type α and hence is accepted by Lean's kernel.
Given a box-tactic m that is sound on 𝑏, then we can construct a sound box-tactic on ℐ (𝑥∶α)𝑏 too that acts on the nested box 𝑏.
3.4.4. Escape-hatch to tactics
As discussed in Section 2.4.4, many provers, including Lean 3, come with a tactic combinator language to construct proofs through mutating an object called the TacticState comprising a metavariable context and a list of metavariables called the goals.
In Section 3.1 I highlighted some of the issues of this approach, but there are many built-in and community-made tactics which can still find use within a HumanProof proof.
For this reason, it is important for HumanProof to provide an 'escape hatch' allowing these tactics to be used within the context of a HumanProof proof seamlessly.
I achieve this compatibility system between Boxes and tactics through defining a zipper [Hue97[Hue97]Huet, GérardFunctional Pearl: The Zipper (1997)Journal of functional programming(link)] structure on Boxes (Appendix A.2) and then a set of operations for soundly converting an underlying TacticState to and from a Box object.
The details of this mechanism can be found in Appendix A.2.
It is used to implement some of the box-tactics presented next in Section 3.5, since in some cases the box-tactic is the same as its tactic-based equivalent.
3.4.5. Summary
In this section, I defined assignability on Boxes and the valid typing judgement inference rules on Box. I used these to define the soundness of a box-tactic and showed that for a box-tactic to be sound, it suffices to show that its typing judgement is preserved through the use of Lemma 3.15.
I also briefly review Appendix A, which presents a mechanism for converting a tactic-style proof to a box-tactic.
3.5. Human-like-tactics for Box.
Using the framework presented above we can start defining sound tactics on Boxes and use Box to actualise the kinds of reasoning discussed in Section 3.1.
Many of the box-tactics here are similar to inference rules that one would find in a usual system, and so I do not cover these ones in great detail.
I also skip many of the soundness proofs, because in Appendix A I instead provide an 'escape hatch' for creating sound box-tactics from tactics in the underlying metavariable-oriented development calculus.
3.5.1. Simplifying box-tactics
We have the following box-tactics for reducing Boxes, these should be considered as tidying box-tactics.
3.5.2. Deleting tactics
These are box-tactics that cause a Box to become simpler, but which are not always 'safe' to do, in the sense that they may lead to a Box which is impossible to solve. That is, the Box may still have a true conclusion but it is not possible to derive this from the information given on the box. For example, deleting a hypothesis 𝑝 ∶ P, may prevent the goal ?𝑡 ∶ P from being solved. The rules for deletion are presented in (3.23).
To motivate 𝒪-revert tactics, recall that an 𝒪-box 𝑏₁ ⋁ 𝑏₂ represents the state that either𝑏₁ or 𝑏₂ needs to be solved, so 𝒪-reversion amounts to throwing away one of the boxes.
This is similar to 𝒪-reduce in (3.22) with the difference being that we do not need one of the boxes to be solved before applying.
These are useful when it becomes clear that a particular 𝒪-branch is not solvable and can be deleted.
3.5.3. Lambda introduction
In tactics, an intro tactic is used to introduce Π-bindersΠ-binders Π (𝑥:α),β are the dependent generalisation of the function type α → β where the return type β may depend on the input value α..
That is, if the goal state is ⊢ Π (𝑥:α),β[𝑥] the intro tactic produces a new state (𝑥:α) ⊢ β[𝑥].
To perform this, it assigns the goal metavariable ?t₁ : Π (𝑥:α),β[𝑥] with the expression λ (𝑥:α),?t₂ where ?t₂ :β[𝑥] is the new goal metavariable with context including the additional local variable 𝑥:α.
The intro tactic on Box is analogous, although there are some additional steps required to ensure that contexts are preserved correctly.
The simplified case simple_intro(3.24), performs the same steps as the tactic version of intro.
The full version (3.25) is used in the case that the ℐ-box is not immediately followed by an -box.
In this case, a conjunctive 𝒜-box must be created in order to have a separate context for the new (𝑥:α) variable.
The fact that intro is sound follows mainly from the design of the definitions of ℐ:
Structural sharing is defined as making use of the same substructure multiple times in a larger structure.
For example, a tree with two branches being the same would be using structural sharing if the sub-branches used the same object in memory.
Define 𝑏' to be ℐ (𝑥:α), 𝒢 (?t₁ :β), ?t₁, represented graphically in (3.26). The typing judgement (3.26) follows from the typing rules (3.13).
By the definition of a sound box-tactic we may assume ⊢ (𝒢 ?t₀,𝑏):γ for some type γ. From the 𝒢 typing rule (3.13) we then have [?t₀];∅ ⊢ 𝑏:γ.
Then it follows from 𝒜 typing (3.13) that ⊢ 𝒜 𝑏' (t₀ : Π (𝑥:α),β)𝑏:γ where 𝑏' := ℐ (𝑥:α), 𝒢 (?t₁ :β), ?t₁.
3.5.4. Split and cases tactics
Here I present some box-tactics for performing introduction and elimination of the ∧ type.
The Box version of split performs the same operation as split in Lean: introducing a conjunction.
A goal ?t₀ :P ∧ Q is replaced with a pair of new goals (?t₁,?t₂).
These can be readily generalised to other inductive datatypes with one constructorOne caveat is that the use of ∃ requires the use of a non-constructive axiom of choice with this method. This is addressed in Section 3.5.8.
In the implementation, these are implemented using the tactic escape-hatch described in Appendix A.
Similarly we can eliminate a conjunction with cases.
3.5.5. Induction box-tactics
∧-elimination (3.28) from the previous section can be seen as a special case of induction on datatypes.
Most forms of dependent type theory use inductive datatypes (see Section 2.2.3) to represent data and propositions, and use induction to eliminate them.
To implement induction in CICCalculus of Inductive Constructions. The foundation used by Lean 3 and Coq (Section 2.1.3). See [Car19 §2.6] for the axiomatisation of inductive types within Lean 3's type system., each inductive datatype comes equipped with a special constant called the recursor.
This paradigm broadens the use of the words 'recursion' and 'induction' to include datastructures that are not recursive.
For example, we can view conjunction A ∧ B:Prop as an inductive datatype with one constructor mk:A → B → A ∧ B.
Similarly, a disjunctive A ∨ B has two constructors inl:A → A ∨ B and inr:B → A ∨ B. Interpreting → as implication, we recover the basic introduction axioms for conjunction and disjunction. The eliminators for ∧ and ∨ are implemented using recursors given in (3.29).
Performing an induction step in a CIC theorem prover such as Lean amounts to the application of the relevant recursor.
Case analysis on a disjunctive hypothesis makes for a good example of recursion, the recursor ∨-rec:(P → C) → (Q → C) → (P ∨ Q) → C is used.
Given a box ℐ (h₀:P ∨ Q),𝑏 where h₀ ⊢ 𝑏 ∶ α, the ∨-cases box-tactic sends this to the box defined in (3.30).
This is visualised in (3.31).
Note that the 𝑏:Box in (3.31) may contain multiple goals. When the cases box-tactic is applied to ℐ (h₀∶P ∨ Q),𝑏, the resulting Box on the rhs of (3.31) results in two copies of these goals. This implements structural sharing of goals as motivated in Section 3.1.3. Structural sharing has a significant advantage over the goal-state style approach to tactics, where the equivalent cases tactic would have to be applied separately to each goal if there were multiple goals.
This structurally-shared induction step also works on recursive datastructures such as lists and natural numbers. These datatypes' recursors are more complicated than non-recursive datastructures such as those in (3.29) in order to include induction hypotheses. The recursor for natural numbers is shown in (3.32). (3.33) is the corresponding box-tactic that makes use of (3.32). (3.34) is the detailed Box structure for the right-hand side of (3.33).
In general, finding the appropriate motive 𝒞 for an induction step amounts to a higher order unification problem which was shown to be undecidable [Dow01[Dow01]Dowek, GilesHigher-order unification and matching (2001)Handbook of automated reasoning(link) §3].
However, in many practical cases 𝒞 can be found and higher-order provers come equipped with heuristics for these cases, an early example being Huet's semidecidable algorithm.
Rather than reimplementing these heuristics, I implement induction box-tactics on Box by using the 'escape hatch' feature (Section 3.4.4).
3.5.6. Introducing 𝒪 boxes
The purpose of 𝒪 boxes is to enable backtracking and branches on Boxes that enables structural sharing.
The G&G prover [GG17[GG17]Ganesalingam, Mohan; Gowers, W. T.A fully automatic theorem prover with human-style output (2017)Journal of Automated Reasoning(link)] takes a similar approach.
For example, suppose that we had a goal x ∈ A ∪ B for some sets A, B. We might have some lemmas of the form h₁:P → x ∈ A and h₂:Q → x ∈ B but we are not yet sure which one to use.
In a goal-based system, if you don't yet know which injection to use, you have to guess and manually backtrack.
However, there may be some clues about which lemma is correct that only become apparent after applying an injection.
In the above example, if only h₃:P is present as a hypothesis, it requires first performing injection before noticing that h₁ is the correct lemma to apply.
In Section 3.7.1 I discuss more advanced, critic-like workflows that 𝒪-boxes also enable.
The 𝒪 box allows us to explore various counterfactuals without having to perform any user-level backtracking (that is, having to rewrite proofs).
The primitive box-tactic that creates new 𝒪-boxes is shown in (3.35).
This is used to make more 'human-like' box-tactics such as ∨-split(3.36).
3.5.7. Unification under a Box
Unification is the process of taking a pair of expressions 𝑙𝑟:Expr within a joint context 𝑀;Γ and finding a valid set of assignments of metavariables σ in 𝑀 such that (𝑀+σ);Γ ⊢ 𝑙 ≡ 𝑟.
Rather than develop a whole calculus of sound unification for the Box system, I can use the 'escape hatch' tactic compatibility layer developed in Appendix A to transform a sub-Box to a metavariable context and then use the underlying theory of unification used for the underlying development calculus of the theorem prover (in this case Lean).
This is a reasonable approach because unifiers and matchers for theorem provers are usually very well developed in terms of both features and optimisation, so I capitalise on a unifier already present in the host proof assistant has a perfectly good one already.
3.5.8. Apply
In textbook proofs of mathematics, often an application of a lemma acts under ∃ binders.
For example, let's look at the application of fs𝑛 being continuous from earlier.
In the example the application of h₁ with 𝑁,ε,h₃, and then eliminating an existential quantifier δ and then applying more arguments y, all happen in one step and without much exposition in terms of what δ depends on. A similar phenomenon occurs in backwards reasoning. If the goal is dist(f𝑥)(f𝑦)<ε, in proof texts the continuity of f is applied in one step to replace this goal with distxy<δ, where δ is understood to be an 'output' of applying the continuity of f.
Contrast this with the logically equivalent Lean tactic script fragment (3.38):
In order to reproduce this human-like proof step, we need to develop a theory for considering 'complex applications'.
A further property we desire is that results of the complex application must be stored such that we can recover a natural language write-up to explain it later (e.g., creating "Since f is continuous at x, there is some δ...").
The apply subsystem works by performing a recursive descent on the type of the assumption being applied.
For example, applying the lemma given in (3.37) to a goal 𝑡:P attempts to unify P with dist(f?𝑥)(f?𝑦)<?ε with new metavariables ?𝑥?𝑦:X, ε:ℝ.
If the match is successful, it will create a new goal for each variable in a Π-binderNote that ∀ is sugar for Π. above the matching expression and a new 𝒱-binder for each introduced ∃-variable and each conjunct.
These newly introduce nested boxes appear in the same order as they appear in the applied lemma.
This apply system can be used for both forwards and backwards reasoning box-tactics. Above deals with the backwards case, in the forwards case, the task is reversed, with now a variable bound by a Π-binder being the subject to match against the forwards-applied hypothesis.
An example of applying (3.37) to the goal dist(fx)(fy)<ε can be seen in (3.1).
3.5.8.1. A note on using apply with existential statements
One complication with this approach to apply is performing many logical inference steps when applying a lemma in one go.
There is a technical caveat with applications of existential statements such as ∃ (δ:ℝ),d(𝑥,𝑦)<δ:
by default, Lean is a non-classical theorem prover, which here amounts to saying that the axiom of choice is not assumed automatically.
Without the axiom of choice, it is not generally possible to construct a projection function ε: ∃ (𝑥:α),P[𝑥] → α such that P[εℎ] is true for all ℎ: ∃ (𝑥:α),P. There are two ways to overcome this limitation:
Assume the axiom of choice and make use of the nonconstructive projector ε.
When an apply step encounters an existential quantifier, wrap the entire proof in an existential quantifier recursorRecursors are discussed in Section 3.5.5.∃-rec(C:Prop):(∀ (𝑥:α),P𝑥 → C) → (∃ (𝑥:α),P𝑥) → C using 𝒜-boxes. This is performed in exactly the same manner that induction box-tactics are applied in Section 3.5.5.
HumanProof, as it is currently implemented, uses strategy 1.
This prevents proofs from being constructive, but is otherwise not so great a concession, since mathematicians regularly make use of this in fields outside logic.
There was some effort to also implement strategy 2, but I dropped it.
3.5.9. Summary
This section introduced a set of sound box-tactics that are implemented for the HumanProof system. In the next section we will see how these box-tactics can be used to create natural language write-ups of proofs.
3.6. Natural language generation of proofs
In this section I detail how the above box architecture is used to produce natural language writeups as the proof progresses.
The general field is known as Natural Language Generation (NLG).
You can find a background survey of NLG both broadly and within the context of generating proofs in Section 2.7.
Here I lean on the work of Ganesalingam, who in his thesis [Gan10[Gan10]Ganesalingam, MohanThe language of mathematics (2010)PhD thesis (University of Cambridge)(link)] has specified a working theory of the linguistics of natural language mathematics.
As well as generating a formally verifiable result of a proof, I also extend on G&G by providing some new mechanisms for converting Lean predicates and typeclasses in to English language sentences.
That is, in the implementation of the G&G theorem prover, many natural language constructs such as "X is a metric space" were hard-coded in to the system.
In this work I provide a general framework for attaching verbalisations of these kinds of statements to typeclasses and predicates within Lean.
I also make the resulting write-up interactive; emitting a partial proof write-up if the proof-state is not yet solved and also inspecting the natural language write-up through the widgets system are possible.
In contrast G&G's output was a static LATEX file.
The goal of this section is to demonstrate that the Box architecture above is representative of human-like reasoning by constructing natural language writeups of the proofs created using Boxes. As such the NLG used here is very simple compared to the state of the art and doesn't make use of any modern techniques such as deep learning. The output of this system is evaluated by real, human mathematicians in Chapter 6.
An example of a proof generated by the system is shown below in Output 3.40.
There are some challenges in converting a Box proof to something that reads like a mathematical proof that I will detail here.
3.6.1. Overview
The architecture of the NLG component is given in Figure 3.41.
The design is similar to the standard architecture discussed in Section 2.7.1.
In Section 3.1.2 I explained the decision to design the system to permit only a restricted set of box-tactics on a Box representing the goal state of the prover.
To create the natural language write-up from these box-tactics, each box-tactic also emits an Act object.
This is an inductive datatype representing the kind of box-tactic that occurred.
So for example, there is an Intro:ListBinder → Act that is emitted whenever the intro box-tactic is performed, storing the list of binders that were introduced.
A list of Acts is held in the state monad for the interactive proof session.
This list of acts is then fed to a micro-planner, which converts the list of acts to an abstract representation of sentencesSometimes referred to as a phrase specification.
These sentences are converted to a realised sentence with the help of Run which is a form of S-expression [McC60[McC60]McCarthy, JohnRecursive functions of symbolic expressions and their computation by machine, Part I (1960)Communications of the ACM(link)] containing text and expressions for interactive formatting.
This natural language proof is then rendered in the output window using the widgets system (Chapter 5).
3.6.2. Grice's laws of implicature
One resource that has proven useful in creating human-like proofs is the work of the Grice on implicature in linguistics [Gri75[Gri75]Grice, Herbert PLogic and conversation (1975)Speech acts(link)].
To review, Grice states that there is an unwritten rule in natural languages that one should only provide as much detail as is needed to convey the desired message. For example, the statement "I can't find my keys" has the implicature "Do you know where my keys are?", it implies that the keys may have been lost at the current location and not in a different part of town and so on.
If superfluous detail is included, the reader will pick this up and try to use it to infer additional information. Saying "I can't find my keys at the moment" interpreted literally has the same meaning as "I can't find my keys", but implicitly means that I have only just realised the key loss or that I will be able to find them soon. Grice posits four maxims that should be maintained in order for a sentence or phrase to be useful:
Quantity The contribution should contain no more or less than what is required. Examples: "Since x>5 and x is prime, x>6". "Let x be a positive real such that x>0."
Quality Do not say things for which you don't have enough evidence or things that are not true. An example here would be a false proof.
Relation The contributed sentence should be related to the task at hand. Example; putting a true but irrelevant statement in the middle of the proof is bad.
Manner The message should avoid being obscure, ambiguous and long-winded.
Mathematical texts are shielded from the more oblique forms of implicature that may be found in general texts, but Grice's maxims are still important to consider in the construction of human-readable proofs and serve as a useful rule-of-thumb in determining when a generated sentence will be jarring to read.
With respect to the quantity maxim, it is important to remember also that what counts as superfluous detail can depend on the context of the problem and the skill-level of the reader. For example, one may write:
Suppose A and B are open subsets of X. Since f is continuous, f−1[A∪B] is open.
A more introductory text will need to also mention that X is a topological space and so A∪B is open. Generally these kinds of implicit lemma-chaining can become arbitrarily complex, but it is typically assumed that these implicit applications are entirely familiar to the reader.
Mapping ability level to detail is not a model that I will attempt to write explicitly here. One simple way around this is to allow the proof creator to explicitly tag steps in the proof as 'trivial' so that their application is suppressed in the natural language write-up.
Determining this correct level of detail may be a problem in which ML models may have a role to play.
3.6.3. Microplanning symbolic mathematics
From a linguistic perspective, a remarkable property of mathematical texts is the interlacing of mathematical symbols and natural language.
In the vast majority of cases, each symbolic construct has a natural language equivalent (else verbalising that symbol in conversation would be difficult).
For example: "x+y" versus "x plus y".
Sometimes multiple verbalisations are possible: P⇒Q can be "P implies Q" or "Q whenever P".
Sometimes the the symbolic form of a statement is not used as frequently: "p is prime" versus p∈P.
In making text flow well, the decision of when to move between symbolic and textual renderings of a mathematical proof is important.
The rule-of-thumb that I have arrived at is to render the general flow of the proof's reasoning using text and to render the objects that are being reasoned about using symbols.
The idea here is that one should be able to follow the rough course of argument whilst only skimming the symbolic parts of the proof.
3.6.4. Microplanning binders with class predicate collections
In mathematics, it is common that a variable will be introduced in a sentence and then referenced in later sentences.
For example, one will often read sentences such as "Let X be a metric space and let x and y be points in X".
This corresponds to the following telescopeA telescope is a list of binders where the type of a binder may depend on variables declared ealier in the list. Telescopes are equivalent to a well-formed context (see Section 2.1.3) but the term telescope is also used to discuss lists of binders that appear in expressions such as lambda and forall bindings. of binders: (X:Type)(_:metric_spaceX)(xy:X).
These effectively act as 'linguistic variable binders'.
In this subsection I will highlight how to convert lists of binders to natural language phrases of this form.
To the best of my knowledge this is an original contribution so I will explain this mechanism in more detail.
This approach is inspired by the idea of 'notions' as first used in the ForTheL controlled natural language parser for the SAD project [VLP07[VLP07]Verchinine, Konstantin; Lyaletski, Alexander; Paskevich, AndreiSystem for Automated Deduction (SAD): a tool for proof verification (2007)International Conference on Automated Deduction(link), Pas07[Pas07]Paskevich, AndreiThe syntax and semantics of the ForTheL language (2007)PhD thesis (Université Paris XII)(link), VLPA08[VLPA08]Verchinine, Konstantin; Lyaletski, Alexander; Paskevich, Andrei; et al.On correctness of mathematical texts from a logical and practical point of view (2008)International Conference on Intelligent Computer Mathematics(link)] also used by Naproche/SAD [DKL20[DKL20]De Lon, Adrian; Koepke, Peter; Lorenzen, AntonInterpreting Mathematical Texts in Naproche-SAD (2020)Intelligent Computer Mathematics(link)].
Ganesalingam [Gan10[Gan10]Ganesalingam, MohanThe language of mathematics (2010)PhD thesis (University of Cambridge)(link)] refers to these as non-extensional types and Ranta [Ran94[Ran94]Ranta, AarneSyntactic categories in the language of mathematics (1994)International Workshop on Types for Proofs and Programs(link)] as syntactic categories.
The act of
The PROVERB system [HF97[HF97]Huang, Xiaorong; Fiedler, ArminProof Verbalization as an Application of NLG (1997)International Joint Conference on Artificial Intelligence(link)] and the G&G system [GG17[GG17]Ganesalingam, Mohan; Gowers, W. T.A fully automatic theorem prover with human-style output (2017)Journal of Automated Reasoning(link)] provide a mechanism for generating natural language texts using a similar technique for aggregating assumptions, however these approaches do not allow for the handling of more complex telescopes found in dependent type theory.
Table 3.42 presents some examples of the kinds of translations in question.
Table 3.42
Examples of generating natural language renderings of variable introductions from type-theory telescopes.
Square brackets on a binder such as [groupG] denote a typeclass binder.
This typeclass binder is equivalent to the binder (𝔤 :groupG) where the binder name 𝔤 is omitted.
Typeclasses were first introduced by Hall et al for use with the Haskell programming language [HHPW96].
Typeclasses are used extensively in the Lean 3 theorem prover. A description of their implementation can be found in [MAKR15 §2.4].
Telescope
Generated text
(X:Type)[metric_spaceX](𝑥𝑦:X)
LetX be a metric space and let 𝑥 and 𝑦 be points in X.
(G:Type)[groupG](𝑥𝑦:G)
LetG be a group and let 𝑥 and 𝑦 be elements of G.
(G:Type)[groupG](H:setG)(h₁:subgroup.normalGH)
LetG be a group and H be a normal subgroup of G.
(𝑎𝑏:ℤ)(h₁:coprime𝑎𝑏)
Let𝑎 and 𝑏 be coprime integers.
(𝑓:X → Y)(h₁:continuous𝑓)
Let𝑓:X → Y be a continuous function.
(T:Type)[topological_spaceT](U:setT)(h₁:openU)
LetT be a topological space and let U be an open set in T.
(ε:ℝ)(h₁:ε>0)
Letε>0.
[HHPW96]Hall, Cordelia V; Hammond, Kevin; Peyton Jones, Simon L; et al.Type classes in Haskell (1996)ACM Transactions on Programming Languages and Systems (TOPLAS)(link)[MAKR15]de Moura, Leonardo; Avigad, Jeremy; Kong, Soonho; et al.Elaboration in Dependent Type Theory (2015)CoRR(link)The variable introduction sentences in Table 3.42 take the role of a variable binder for mathematical discourse.
This variable is then implicitly 'in scope' until its last mention in the text. Some variables introduced in this way can remain in scope for an entire book.
For example, the choice of underlying field k in a book on linear algebra.
As Ganesalingam notes [Gan10[Gan10]Ganesalingam, MohanThe language of mathematics (2010)PhD thesis (University of Cambridge)(link) §2.5.2], "If mathematicians were not able to use variables in this way, they would need to write extremely long sentences!"
Let's frame the problem as follows: take as input a telescope of binders (e.g, [(𝑎:ℤ),(𝑏:ℤ),(h₁:coprime𝑎𝑏)]) and produce a 'variable introduction text' string as shown in the above table.
The problem involves a number of challenges:
There is not a 1-1 map between binders and pieces of text: in "Let 𝑎, 𝑏 be coprime", the binder h₁:coprime𝑎𝑏 is not named but instead treated as a property of 𝑎 and 𝑏.
The words that are used to describe a variable can depend on which typeclass [HHPW96]See the caption of Table 3.42 for more information on typeclasses. their type belongs to. For instance, we write "let 𝑥 and 𝑦 be points" or "let 𝑥 and 𝑦 be elements of G" depending on whether the type of 𝑥 and 𝑦 is an instance of group or metric_space.
Compare "𝑥 and 𝑦 are prime" versus "𝑥 and 𝑦 are coprime". The first arises from (𝑥𝑦:ℕ)(h₁:prime𝑥)(h₂:prime𝑦) whereas the second from (𝑥𝑦:ℕ)(h₁:coprime𝑥𝑦). Hence we need to model the adjectives "prime" and "coprime" as belonging to distinct categories.
To solve this I introduce a schema of class predicate collections. Each binder in the input telescope is converted to two pieces of data; the subject expression𝑥 and the class predicate𝑐𝑝; which is made from one of the following constructors.
adjective: "continuous", "prime", "positive"
fold_adjective: "coprime", "parallel"
symbolic_postfix: "∈ A", ">0", ":X → Y"
class_noun: "number", "group", "points in X", "elements of G", "function", "open set in T"
none: a failure case. For example, if the binder is just for a proposition that should be realised as an assumption instead of a predicate about the binder.
The subject expression and the class predicate for a given binder in the input telescope are assigned by consulting a lookup table which pattern-matches the binder type expressions to determine the subject expression and any additional parameters (for example T in "open set in T"). Each pair ⟨𝑥,𝑐𝑝⟩ is mapped to ⟨[𝑥],[𝑐𝑝]⟩ :ListExpr × ListClassPredicate. I call this a class predicate collection (CPC). The resulting list of CPCs is then reduced by aggregating [DH93[DH93]Dalianis, Hercules; Hovy, EduardAggregation in natural language generation (1993)European Workshop on Trends in Natural Language Generation(link)] adjacent pairs of CPCs according to (3.43).
In certain cases, the merging operation can also delete class predicates that are superseded by later ones.
An example is that if we have (𝑥:X)(h₁:𝑥 ∈ A), this can be condensed directly to ⟨[𝑥],[symbolic_postfix"∈ A"]⟩ which realises to "Let 𝑥 ∈ A" instead of the redundant "Let 𝑥 ∈ A be an element of X" which violates Grice's maxim of quantity (Section 3.6.2).
Additionally, the resulting class predicate collection list is partitioned into two lists so that only the first mention of each subject appears in the first list.
For example; 𝑥:X and h:𝑥 ∈ A both have the subject 𝑥, but "Let 𝑥 be a point and let 𝑥 ∈ A"
These class predicate collections can then be realised for a number of binder cases:
Let: "Let U be open in X"
Forall: "For all U open in X"
Exists: "For some U open in X"
class_noun can be compared to the concept of a 'notion' in ForTheL and Naproche/SAD and a 'non-extensional type' in Ganesalingam [Gan10[Gan10]Ganesalingam, MohanThe language of mathematics (2010)PhD thesis (University of Cambridge)(link)].
It takes the role of a noun that the introduced variable belongs to, and is usually preceded with an indefinite article: "let 𝑥 be an element of G".
Will some mechanism like CPCs be necessary in the future, or are they a cultural artefact of the way that mathematics has been done in the past? When designing mathematical definitions in formalised mathematics, one must often make a choice in how new datatypes are defined: should there be a new type 'positive real number' or just use the real numbers ℝ and add a hypothesis ε>0? In natural language mathematics, one is free to move between these bundled and unbundled representations without concern. The CPC structure reflects this; "ε is a positive real" can be interpreted as either a "real that is positive" or as a single semantic type "positive real". Natural mathematics does not disambiguate between these two because they are both equivalent within its informal rules, similar to how the representation of 𝑎+𝑏+𝑐 does not need to disambiguate between (𝑎+𝑏)+𝑐 and 𝑎+(𝑏+𝑐) since they are equal.
3.6.5. Handling 'multi-apply' steps
The specialised apply box-tactic discussed in Section 3.5.8 requires some additional processing.
The apply box-tactic returns a datatype called ApplyTree that indicates how a given lemma was applied, resulting in parameters, goals and values obtained through eliminating an existential statement.
These are converted in to "since" sentences:
"Since f is continuous, there exists some δ>0 such that d(f𝑥)(f𝑦)<0 whenever d𝑥𝑦<δ"
The code that produces this style of reasoning breaks down in to a Reason component indicating where the fact came from and a restatement of the fact with the parameters set to be relevant to the goal.
In most cases, the Reason can simply be a restatement of the fact being used.
However, it is also possible to produce more elaborate reasons.
For example, applyℎ for some hypothesis ℎ will also match preconditions on ℎ if they appear in context.
That is, if h₀ ∶ P → Q, then applyh₀ in the box in (3.44) will automatically include the propositional assumption h₁:P to solve the Box, instead of resulting in a new goal ?t₂ :P.
This will produce the reason "Since P → Q and P, we have Q".
3.6.6. Multiple cases
Some problems branch into multiple cases. For example, the A ∪ B problem.
Here, some additional macroplanning needs to occur, since it usually makes sense to place each of the cases in their own paragraph.
When cases is performed, the resulting 𝒜-box contains two separate branches for each case as discussed in (3.28).
When a new box-tactic is performed to create an Act, box-tactics that are performed within one of these case blocks causes the Act to be tagged with the case.
This is then used to partition the resulting rendered string into multiple paragraphs.
3.6.7. Realisation
As shown in Figure 3.41, the set of Acts is compiled to a sequence of Sentence objects and these are converted to a run of text. As detailed in Section 2.7 this last step is called realisation.
In the realisation phase, each sentence is converted to a piece of text containing embedded mathematics.
Each statement is constructed through recursively assembling canned phrases representing each sentence.
This means that longer proofs can become monotonous but the application of synonymous phrases could be used to add variation.
However, the purpose of this NLG system is to produce 'human-like' reasoning and so if the proofs read as too monotonous, it suggests that less detail should have been included in the Act list structure.
When realising logical statements, the prose would become unnatural or ambiguous after a certain depth.
After a depth of two these statements switch to being entirely symbolic.
For example: (P → Q) → X → Y would recursively render in natural language naïvely as "Y whenever X and Q whenever P", even with some more sophisticated algorithm to remove the clunkiness, writing "Y whenever X and P → Q is just much clearer.
Mathematical expressions were pretty printed using Lean's pretty printing engine.
However, the Lean 3 pretty printer needs a metavariable context in order to render, so it was necessary to add a tactic state object alongside the Act objects.
It was necessary to store this context separately for each act because some metavariables would become solved through the course of the proof and cause confusing statements such as "by setting ε to be ε", where it should read "by setting η to be ε".
Another printing issue was in the printing of values created through destructuring existential variables, which would be rendered as classical.some.
3.6.8. Summary
In this section, I detailed the workings of the natural language write-up component of the HumanProof system.
I gave an overview of the standard architecture pipeline and then discussed the areas of novelty, namely the approach to producing suitable noun-phrase string from type-theoretical telescopes and on the verbalisations multi-apply steps.
3.7. Conclusion
In this chapter, I have introduced a new Box development calculus for human-like reasoning and demonstrated its compatibility (Section 3.4, Appendix A) with the development calculus of the Lean theorem prover.
I have outlined the structure of a set of box-tactics within this calculus that allow for the creation of both formal and natural-language proofs of this output.
I then detailed the natural language generation component of HumanProof.
The component can produce readable proofs of simple lemmas. Supporting larger projects is left for future work.
In the next chapter, we will discuss a new component to enhance the Box system for use with equational reasoning.
I will make use of the work presented in this chapter in the evaluation (Chapter 6).
I will finish this chapter with some thoughts on future directions for the Box datastructure.
A more general outlook on future work can be found in Section 7.2, where I also discuss potential future directions in applying deep learning to natural language generation.
3.7.1. Future work: 𝒪-critics
An avenue for future research is the definition of some additional box-tactics for the Box datastructure that allow it to work in a similar fashion to Ireland's proof critics[Ire92[Ire92]Ireland, AndrewThe use of planning critics in mechanizing inductive proofs (1992)International Conference on Logic for Programming Artificial Intelligence and Reasoning(link)]. Recall from Section 2.6.2 that proof critics (broadly speaking) are a proof planning technique that can revise a proof plan in light of information gained from executing a failed plan. 𝒪-boxes can support a similar idea as I will now exemplify in (3.45), where the statement to prove is ∀ 𝑎𝑏:ℝ, ∃ 𝑥:ℝ,(𝑎 ≤ 𝑥) ∧ (𝑏 ≤ 𝑥). The proof requires spotting the trichotomy property of real numbers: ∀ 𝑥𝑦:ℝ,𝑥 ≤ 𝑦 ∨ 𝑦<𝑥, however it is difficult to see whether this will apply from the goal state.
At this point, one can spot that the lefthand Box is no longer possible to solve unless one assumes 𝑏 ≤ 𝑎. However, rather than deleting the left-hand box, we can instead use this information as in (3.46).
The remaining research question for putting (3.45) and (3.46) into practice is to determine some heuristics when it is appropriate to perform 𝒪-intro (step ②) and step ④, where an instance ℎ:𝑏 ≤ 𝑎 ∨ ¬ 𝑏 ≤ 𝑎 is introduced. What is an appropriate trigger for suggesting the manoeuvre in ④,⑤,⑥ to the user?
Chapter 4
Subtasks
4.1. Equational reasoning
Equality chains are ubiquitous in mathematics.
Here, by equality chain, I mean parts of proofs found in mathematical literature that consist of a list of expressions separated by = or some other transitive relation symbol.
The chains are chosen such that each pair of adjacent expressions are clearly equal to the reader, in the sense that the equality does not need to be explicitly justified. And hence, by transitivity, the chain shows that the first expression is equal to the last one.
For example, take some vector space V. Suppose that one wishes to prove that given a linear map 𝐴:V ⟶ V, its adjoint 𝐴† :V → V is linearIn general, the adjoint should act on the dual space𝐴† :V* → V*..
To do so one typically provides the equality chain (4.1) for all vectors 𝑥𝑢𝑣:V.
The equations that one can compose the reasoning chain from (e.g., ⟨𝐴† 𝑎,𝑏⟩ = ⟨𝑎,𝐴𝑏⟩) are called
rewrite rules.
For the example (4.1), there are a large number of axiomatic rewrite rules available (4.2) and still more rules derived from these.
We can formulate the equation rewriting problem for two expressions Γ ⊢ 𝑙=𝑟 as finding a path in the graph E whose vertices are expressions in Γ and whose edges are generated by a set of rewrite rules 𝑅 (such as those in (4.2)). Any free variables in 𝑅 are substituted with correctly typed expressions to produce ground rewrite rules that are then closed under symmetry, transitivity, congruenceA relation ~ is congruent when 𝑥~𝑦 implies 𝑡⦃𝑧 ↦ 𝑥⦄ ~𝑡⦃𝑧 ↦ 𝑦⦄ for all valid expressions 𝑥, 𝑦 and 𝑡 where 𝑡 has a free variable 𝑧..
A central part of automated theorem proving (ATP) is constructing equality proofs such as (4.1) from (4.2) automatically.
This can be done with well-researched techniques from the field of term rewriting systems[BN98[BN98]Baader, Franz; Nipkow, TobiasTerm rewriting and all that (1998)publisher Cambridge University Press(link)].
These techniques take advantage of the fact that computers can perform many operations per second, and large search spaces can be explored quickly, though heuristic functions are still needed to prevent a combinatorial explosion.
Many domains - such as checking that two expressions are equal using the ring axioms - also have specialised decision procedures available for them.
I'll call these approaches to solving equalities machine-oriented; this contrasts with human-oriented as discussed in Section 2.6.
In accordance with the research goals of this thesis (Section 1.2), the purpose here is to investigate alternative, human-like ways of producing equality proofs.
As motivated in Section 1.1, this serves the purpose of improving the usability of proof assistants by making the proofs generated more understandable (Section 2.5).
The goal of this chapter is not to develop methods that compete with machine-oriented techniques to prove more theorems or prove them faster.
Instead, I want to focus on the abstract reasoning that a human mathematician typically carries out when they encounter an equality reasoning problem such as (4.1).
With this in mind, the goal of this chapter is to create an algorithm which:
can solve simple equality problems of the kind that an undergraduate
might find easy;
does not encode any domain-specific knowledge of mathematics. That is,
it does not invoke specialised procedures if it detects that the
problem lies in a particular domain such as Presburger arithmetic;
is efficient in the sense that it does not store a large state and
does not perform a significant search when a human would not.
Typically, existing ATP methods do not scale well with the number of competing rules introduced, as one would expect of algorithms that make use of significant amounts of brute-force search.
If we can devise new architectures that solve simple equalities with less search, then it may be possible to scale up these techniques to larger problems and improve the efficiency of established ATP methods.
This chapter presents the subtask algorithm which has some success with respect to the above goals.
The algorithm is written in Lean 3 [MKA+15[MKA+15]de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; et al.The Lean theorem prover (system description) (2015)International Conference on Automated Deduction(link)] and can be found on GitHub.
The work in this chapter also appears as a paper published in KI 2019 [AGJ19[AGJ19]Ayers, E. W.; Gowers, W. T.; Jamnik, MatejaA human-oriented term rewriting system (2019)KI 2019: Advances in Artificial Intelligence - 42nd German Conference on AI(link)].
In the remainder of the chapter I give a motivating example (Section 4.2) followed by a description of the algorithm (Section 4.3).
The algorithm is then contrasted with existing approaches (Section 4.4) and evaluated against the above goals (Section 4.5).
4.2. Example
Let us begin with a motivating example (4.1) in elementary linear algebra.
We have to solve the goal of the Box(4.3) using the rewrite rules given in (4.2).
To do this, a human's proving process might proceed as follows:
The key aspect of the thought process in List 4.4 is the setting of intermediate aims, such as obtaining certain subexpressions when one does not immediately see how to obtain the entire expression.
Let's do this by creating a tree of subtasks Figure 4.5.
The tree in Figure 4.5 represents what the algorithm does with the additivity-of-adjoint problem (4.3).
It starts with the subtask create_all ⟨𝐴† 𝑢+𝐴† v,x⟩ at ①.
Since it cannot achieve that in one application of an available rule, it creates a set of subtasks and then chooses the one that is most promising: later in Section 4.3, I will explain how it generates and evaluates possible subtasks.
In this case the most promising subtask is create𝐴† 𝑢, so it selects that in ② and identifies a rewrite rule - the definition of adjoint: ∀ 𝑤𝑧, ⟨𝐴† 𝑤,𝑧⟩ = ⟨𝑤,𝐴𝑧⟩ - that can achieve it; adding use ⟨𝑢,𝐴?𝑧⟩ = ⟨𝐴† 𝑢,?𝑧⟩ to the tree at ③.
The ?𝑧 that appears at ③ in Figure 4.5 is a metavariableThat is, a placeholder for an expression to be chosen later. See Section 2.4 for background information on metavariables. that will in due course be assigned to 𝑥.
Now the process repeats on ③, a set of subtasks are again created for the lhs of ⟨𝑢,𝐴?𝑧⟩ = ⟨𝐴† 𝑢,?𝑧⟩ and the subtask create𝐴?𝑧 is selected (④).
Now, there does exist a rewrite rule that will achieve create𝐴?𝑧: ⟨𝐴† (𝑢+𝑣),𝑥⟩ = ⟨𝑢+𝑣,𝐴𝑥⟩, so this is applied and now the algorithm iterates back up the subtask tree, testing whether the new expression ⟨𝑢+𝑣,𝐴𝑥⟩ achieves any of the subtasks and whether any new rewrite rules can be used to achieve them.
In the next section, I will provide the design of an algorithm that behaves according to these motivating principles.
4.3. Design of the algorithm
The subtasks algorithm may be constructed as a search over a directed graph S.
The subtask algorithm's state 𝑠:S has three components ⟨𝑡,𝑓,𝑐⟩:
a tree 𝑡𝑠:Tree(Task) of tasks (as depicted in Figure 4.5)
a 'focussed' node 𝑓:Address(𝑡𝑠) in the tree𝑡𝑠 and 𝑓 are implemented as a zipper [Hue97]. Zippers are described in Appendix A..
an expression 𝑐:Expr called the current expression (CE) which represents the current left-hand-side of the equality chain.
The subtasks algorithm provides the edges between states through sound manipulations of the tree and current expression.
Each task in the tree corresponds to a predicate or potential rule application that could be used to solve an equality problem.
Given an equational reasoning problem Γ ⊢ 𝑙=𝑟, the initial state 𝑠₀:S consists of a tree with a single root node CreateAll𝑟 and a CE 𝑙. We reach a goal state when the current expression 𝑐 is definitionally equalThat is, the two expressions are equal by reflexivity. to 𝑟.
The first thing to note is that if we project 𝑠:S to the current expression 𝑐, then we can recover the original equational rewriting problem E by taking the edges to be all possible rewrites between terms. One problem with searching this space is that the number of edges leaving an expression can be infiniteFor example, the rewrite rule ∀ 𝑎𝑏,𝑎=𝑎-𝑏+𝑏 can be applied to any expression with any expression being substituted for 𝑏.
The typical way that this problem is avoided is to first ground all available rewrite rules by replacing all free variables with relevant expressions.
The subtasks algorithm does not do this, because this is not a step that humans perform when solving simple equality problems.
Even after grounding, the combinatorial explosion of possible expressions makes E a difficult graph to search without good heuristics.
The subtasks algorithm makes use of the subtasks tree 𝑡 to guide the search in E in a manner that is intended to match the process outlined in List 4.4 and Figure 4.5.
A task 𝑡:Task implements the following three methods:
refine:Task → (ListTask) creates a list of subtasks for a given task. For example, a task create(𝑥+𝑦) would refine to subtasks create𝑥, create𝑦. The refinement may also depend on the current state 𝑠 of the tree and CE. The word 'refinement' was chosen to reflect its use in the classic paper by Kambhampati [KKY95[KKY95]Kambhampati, Subbarao; Knoblock, Craig A; Yang, QiangPlanning as refinement search: A unified framework for evaluating design tradeoffs in partial-order planning (1995)Artificial Intelligence(link)]; a refinement is the process of splitting a set of candidate solutions that may be easier to check separately.
test:Task → Expr → Bool which returns true when the given task 𝑡:Task is achieved for the given current expression 𝑒:Expr. For example, if the current expression is 4+𝑥, then create𝑥 is achieved. Hence, each task may be viewed as a predicate over expressions.
Optionally, execute:Task → OptionRewrite which returns a Rewrite object representing a rewrite rule from the current expression 𝑐ᵢ to some new expression 𝑐ᵢ₊₁ (in the context Γ) by providing a proof 𝑐ᵢ =𝑐ᵢ₊₁ that is checked by the prover's kernel. Tasks with execute functions are called strategies. In this case, test must return true when execute can be applied successfully, making test a precondition predicate for execute. As an example, the use(𝑥=𝑦) task performs the rewrite 𝑥=𝑦 whenever the current expression contains an instance of 𝑥.
This design enables the system to be modular, where different sets of tasks and strategies can be included.
Specific examples of tasks and strategies used by the algorithm are given in {#the-main-subtasks}.
Given a state 𝑠:S, the edges leading from 𝑠 are generated using the flowchart shown in Figure 4.6.
Let 𝑓 be the focussed subtask for 𝑠.
In the case that test(𝑓) is true the algorithm 'ascends' the task tree.
In this branch, 𝑓 is tagged as 'achieved' and the new focussed task is set as parent of 𝑓.
Then, it is checked whether any siblings of 𝑓 that were marked as achieved are no longer achieved (that is, there is a sibling task 𝑡 tagged as achieved but test(𝑡) is now false).
The intuition behind this check on previously achieved subtasks is that once a sibling task is achieved, it should not be undone by a later step because the assumption is that all of the child subtasks are needed before the parent task can be achieved.
In the case that test(𝑓) is false, meanwhile, the algorithm 'explores' the task tree by finding new child subtasks for 𝑓.
To do this, refine(𝑓) is called to produce a set of candidate subtasks for 𝑓. For each 𝑡 ∈ refine(𝑓), 𝑡 is inserted as a child of 𝑓 provided that test(𝑡) is false and 𝑡 does not appear as an ancestor of 𝑓. Duplicate children are removed. Finally, for each subtask 𝑡, a new state is yielded with the focus now set to 𝑡.
Hence 𝑠's outdegreeThe outdegree of a vertex 𝑣 in a directed graph is the number of edges leaving 𝑣. in the graph will be the number of children that 𝑓 has after refining.
Now that the state space S, the initial state 𝑠₀, the goal states and the edges on S are defined, we can perform a search on this graph with the help of a heuristic function h:S → [0, ∞] to be discussed in Section 4.3.2.
The subtasks algorithm uses greedy best-first search with backtracking points.
However, other graph-search algorithms such as A⋆ or hill-climbing may be used.
4.3.1. The defined subtasks
In this section I will provide a list of the subtasks that are implemented in the system and some justification for their design.
4.3.1.1.create_all𝑒
The create_all:Expr → Task task is the root task of the subtask tree.
Refine: returns a list of create𝑏 subtasks where each 𝑏 is a minimal subterm of 𝑒 not present in the current expression.
Test: true whenever the current expression is 𝑒. If this task is achieved then the subtasks algorithm has succeeded in finding an equality chain.
Execute: none.
The motivation behind the refinement rule is that since 𝑏 appears in 𝑒 but not in the current expression, then it must necessarily arise as a result of applying a rewrite rule. Rather than include every subterm of 𝑒 with this property, we need only include the minimal subterms with this property since if 𝑏 ⊂ 𝑏', then test(create𝑏) ⇐ test(create𝑏'). In the running example (4.3), the subtasks of create_all ⟨𝐴† 𝑢+𝐴† 𝑣,𝑥⟩ are create(𝐴† 𝑢) and create(𝐴† 𝑣).
4.3.1.2.create𝑒
The create task is achieved if the current expression contains 𝑒.
Refine: returns a list use(𝑎=𝑏) subtasks where 𝑒 overlaps with 𝑏 (see further discussion below). It can also return reduce_distance subtasks in some circumstances.
Test: true whenever the current expression is 𝑒.
Execute: none.
Given a rewrite rule 𝑟: ∀ (..𝑥𝑠),𝑎=𝑏, say that an expression 𝑒 overlaps with the right hand side of 𝑟 when there exists a most-general substitution σ on 𝑟's variables 𝑥𝑠 such that
𝑒 appears in σ(𝑏);
𝑒 does not appear in σ(𝑎);
𝑒 does not appear in σ.
This last condition ensures that the expression comes about as a result of the term-structure of the rule 𝑟 itself rather than as a result of a substitution.
The process of determining these rules is made efficient by storing the available rewrite rules in a term indexed datastructure [SRV01[SRV01]Sekar, R; Ramakrishnan, I.V.; Voronkov, AndreiTerm Indexing (2001)Handbook of automated reasoning(link)].
Additionally, as mentioned, create𝑒 can sometimes refine to yield a reduce_distance subtask. The condition for this depends on the distance between two subterms in a parent expression 𝑐:Expr, which is defined as the number of edges between the roots of the subterms -- viewing 𝑐's expression tree as a graph. If two local variables 𝑥, 𝑦 are present exactly once in both the current expression and 𝑒, and the distance between them is greater in the current expression, then reduce_distance𝑥𝑦 is included as a subtask.
In order to handle cases where multiple copies of 𝑒 are required, create has an optional count argument that may be used to request an nth copy of 𝑒.
4.3.1.3.use(𝑎=𝑏)
This is the simplest strategy. It simply represents the subtask of using the given rewrite rule.
Refine: Returns a list of create𝑒 subtasks where each 𝑒 is a minimal subterm of 𝑎 not present in the current expression. This is the same refinement rule that is used to create subtasks of the create_all task.
Test: True whenever the rule 𝑎=𝑏 can be applied to the current expression.
Execute: Apply 𝑎=𝑏 to the current expression. In the event that it fails (for example if the rule application causes an invalid assignment of a metavariable) then the strategy fails.
4.3.1.4.reduce_distance(𝑥,𝑦)
reduce_distance is an example of a greedy, brute-force strategy. It will perform any rewrite rule that moves the given variables closer together and then terminate.
Refine: returns the empty list. That is, there are no subtasks available.
Test: True whenever there is only one instance of 𝑥 and 𝑦 in the current expression and there exists a rewrite rule that will move 𝑥 closer to 𝑦.
Execute: repeatedly applies rewrite rules greedily moving 𝑥 and 𝑦 closer together, terminating when they can move no further together.
4.3.2. Heuristics
In this section I present the heuristic function developed for the subtasks algorithm.
The ideas behind this function are derived from introspection on equational reasoning and some degree of trial and error on a set of equality problems.
There are two heuristic functions that are used within the system, an individual strategy heuristic and an 'overall-score' heuristic that evaluates sets of child strategies for a particular task.
Overall-score is used on tasks which are not strategies by performing a lookahead of the child strategies of the task.
The child strategies 𝑆₁,𝑆₂ ⋯ are then scored individually through a scoring system, scoring higher if they:
achieve a task higher in the task tree;
achieve a task on a different branch of the task tree;
have a high degree of term overlap with the current expression. This
is measured using symbol counting and finding largest common
subterms;
use local variables and hypotheses;
can be achieved in one rewrite step from the current expression.
The intuition behind all of these is to give higher scores to strategies that are salient in some way, either by containing subterms that are present in the current expression or because other subtasks are achieved.
From these individual scores, the score for the parent task of 𝑆₁,𝑆₂... is computed as follows:
If there is only one strategy then it scores 10.
If there are multiple strategies, it discards any scoring less than -5.
If there are positive-scoring strategies then all negative-scoring strategies are discarded.
The overall score is then set to be 5 minus the number of strategies in the list.
The intention of this procedure is that smaller sets of strategies should be preferred, even if their scores are bad because it limits choice in what to do next.
The underlying idea behind the overall-scoring heuristic is that often the first sensible strategy found is enough of a signpost to solve simple problems.
That is, once one has found one plausible strategy of solving a simple problem it is often fruitful to stop looking for other strategies which achieve the same thing and to get on with finding a way of performing the new strategy.
4.3.3. Properties of the algorithm
The substasks algorithm is sound provided sound rewrite rules are produced by the function execute:Task → OptionRewrite.
That is, given an equation to solve Γ ⊢ 𝑙=𝑟 and given a path 𝑠₀ ↝ 𝑠₁ ↝ ... ↝ 𝑠ₙ in S where 𝑠₀ is the initial state defined in
By forgetting the subtask tree, a solution path in S can be projected to a solution path in E, the equational rewriting graph. This projected path is exactly a proof of 𝑙=𝑟; it will be composed of a sequence 𝑙 ≡ 𝑐₀=𝑐₁=...=𝑐ₙ ≡ 𝑟 where 𝑐ᵢ is the current expression of 𝑠ᵢ.
Each equality in the chain holds either by the assumption of the proofs returned from execute being sound or by the fact that the current expression doesn't change between steps otherwise.
The next question to ask is whether S is complete with respect to E. That is, does S contain a path to the solution whenever E contains one?
The answer to this depends on the output of refine. If refine always returns an empty list of subtasks then S is not complete, because no subtasks will ever be executed.
The set of subtasks provided in Section 4.3.1 are not complete. For example the problem 1-1=𝑥+-𝑥 will not solve without additional subtasks since the smallest non-present subterm is 𝑥, so create𝑥 is added which then does not refine further using the procedure in Section 4.3.1.
In Section 4.6 I will discuss some methods to address this.
4.4. Qualitative comparison with related work
There has been a substantial amount of research on the automation of solving equality chain problems over the last decade.
The approach of the subtasks algorithm is to combine these rewriting techniques with a hierarchical search.
In this section I compare subtasks which with this related work.
4.4.1. Term Rewriting
One way to find equality proofs is to perform a graph search using a heuristic.
This is the approach of the rewrite-search algorithm by Hoek and Morrison [HM19[HM19]Hoek, Keeley; Morrison, Scottlean-rewrite-search GitHub repository (2019)https://github.com/semorrison/lean-rewrite-search], which uses the heuristic of string edit-distance between the strings' two pretty-printed expressions.
The rewrite-search algorithm does capture some human-like properties in the heuristic, since the pretty printed expressions are intended for human consumption.
The subtasks algorithm is different from rewrite-search in that the search is guided according to achieving sequences of tasks.
Since both subtasks and rewrite-search are written in Lean, some future work could be to investigate a combination of both systems.
A term rewriting system (TRS) 𝑅 is a set of oriented rewrite rules.
There are many techniques available for turning a set of rewrite rules in to procedures that check whether two terms are equal.
One technique is completion, where 𝑅 is converted into an equivalent TRS 𝑅' that is convergent.
This means that any two expressions 𝑎, 𝑏 are equal under 𝑅 if and only if repeated application of rules in 𝑅' to 𝑎 and 𝑏 will produce the same expression.
Finding equivalent convergent systems, if not by hand, is usually done by finding decreasing orderings on terms and using Knuth-Bendix completion [KB70[KB70]Knuth, Donald E; Bendix, Peter BSimple word problems in universal algebras (1970)Computational Problems in Abstract Algebra(link)].
When such a system exists, automated rewriting systems can use these techniques to quickly find proofs, but the proofs are often overly long and needlessly expand terms.
Another method is rewrite tables, where a lookup table of representatives for terms is stored in a way that allows for two terms to be matched through a series of lookups.
Both completion and rewrite tables can be considered machine-oriented because they rely on large datastructures and systematic applications of rewrite rules.
Such methods are certainly highly useful, but they can hardly be said to capture the process by which humans reason.
Finally, there are many normalisation and decision procedures for particular domains, for example on rings [GM05[GM05]Grégoire, Benjamin; Mahboubi, AssiaProving equalities in a commutative ring done right in Coq (2005)International Conference on Theorem Proving in Higher Order Logics(link)].
Domain specific procedures do not satisfy the criterion of generality given in Section 4.1.
4.4.2. Proof Planning
Background information on proof planning is covered in Section 2.6.2.
The subtasks algorithm employs a structure that is similar to a hierarchical task network (HTN) [Sac74[Sac74]Sacerdoti, Earl DPlanning in a hierarchy of abstraction spaces (1974)Artificial intelligence(link), Tat77[Tat77]Tate, AustinGenerating project networks (1977)Proceedings of the 5th International Joint Conference on Artificial Intelligence.(link), MS99[MS99]Melis, Erica; Siekmann, JörgKnowledge-based proof planning (1999)Artificial Intelligence(link)]. The general idea of a hierarchical task network is to break a given abstract task (e.g., "exit the room") in to a sequence of subtasks ("find a door" then "go to door" then "walk through the door") which may themselves be recursively divided into subtasks ("walk through the door" may have a subtask of "open the door" which may in turn have "grasp doorhandle" until bottoming out with a ground actuation such as "move index finger 10°").
This approach has found use for example in the ICARUS robotics architecture [CL18[CL18]Choi, Dongkyu; Langley, PatEvolution of the ICARUS cognitive architecture (2018)Cognitive Systems Research(link), LCT08[LCT08]Langley, Pat; Choi, Dongkyu; Trivedi, NishantIcarus user’s manual (2008)(link)].
HTNs have also found use in proof planning [MS99[MS99]Melis, Erica; Siekmann, JörgKnowledge-based proof planning (1999)Artificial Intelligence(link)].
The main difference between the approach used in the subtasks algorithm and proof planning and hierarchical task networks is that the subtasks algorithm is greedier: the subtasks algorithm generates enough of a plan to have little doubt what the first rewrite rule in the sequence should be, and no more.
I believe that this reflects how humans reason for solving simple problems: favouring just enough planning to decide on a good first step, and then planning further only once the step is completed and new information is revealed.
A difference between HTNs and subtasks is that the chains of subtasks do not necessarily reach a ground subtask (for subtasks this is a rewrite step that can be performed immediately).
This means that the subtasks algorithm needs to use heuristics to determine whether it is appropriate to explore a subtask tree or not instead of relying on the task hierarchy eventually terminating with ground tasks. The subtasks algorithm also inherits all of the problems found in hierarchical planning: the main one being finding heuristics for determining whether a subtask should be abandoned or refined further. The heuristics given in Section 4.3.2 help with this but there are plenty more ideas from the hierarchical task planning literature that could be incorporated also. Of particular interest for me are the applications of hierarchical techniques from the field of reinforcement learningA good introductory text to modern reinforcement learning is Reinforcement Learning; An Introduction by Sutton and Barto [SB18b]. Readers wishing to learn more about hierarchical reinforcement learning may find this survey article by Flet-Berliac to be a good jumping-off point [Fle19].[SB18b]Sutton, Richard S; Barto, Andrew GReinforcement learning: An introduction (2018)publisher MIT press(link)[Fle19]Flet-Berliac, YannisThe Promise of Hierarchical Reinforcement Learning (2019)The Gradient(link).
4.5. Evaluation
The ultimate motivation behind the subtasks algorithm is to make an algorithm that behaves as a human mathematician would.
I do not wish to claim that I have fully achieved this, but we can evaluate the algorithm with respect to the general goals that were given in Chapter 1.
Scope: can it solve simple equations?
Generality: does it avoid techniques specific to a particular area of mathematics?
Reduced search space: does the algorithm avoid search when finding proofs that humans can find easily without search?
Straightforwardness of proofs: for easy problems, does it give a proof that an experienced human mathematician might give?
The method of evaluation is to use the algorithm implemented as a tactic in Lean on a library of thirty or so example problems.
This is not large enough for a substantial quantitative comparison with existing methods, but we can still investigate some properties of the algorithm.
The source code also contains many examples which are outside the abilities of the current implementation of the algorithm.
Some ways to address these issues are discussed in Section 4.6.
Table 4.7 gives some selected examples.
These are all problems that the algorithm can solve with no backtracking.
Table 4.7
subtask's performance on some example problems. Steps gives the number of rewrite steps in the final proof. Location gives the file and declaration name of the example in the source code.