.. highlight:: lean .. _chapter_using_lean_as_a_proof_assistant: Using Lean as a Proof Assistant =============================== This chapter marks three shifts in the way we are using Lean. First, up to this point we have been using Lean as a programming language, whereas here we will begin to use Lean as a *proof assistant*. In the theory-implementation-application trichotomy that we used to describe this course, this marks a shift from using Lean to implement logical tools to using Lean as an important application of logic, one that is used to verify hardware, software, and complex systems as well as mathematical theorems. Finally, whereas up to now our focus has been on representing logical languages in Lean, now we are using Lean as a logical language itself. This can be viewed as a shift from treating logic as an *object language* to treating logic as a *metalanguage*, a distinction we will now explain. Imagine implementing one programming language, such as Lisp, in another programming language, like C++. In this scenario, we can characterize Lisp as being the object language, that is, the one that is being implemented, and C++ as the metalanguage, the one that is carrying out the implementation. What we did in :numref:`Chapter %s` is similar: we are used one logical system, Lean, to implement another one, propositional logic. Whether we care about logical languages or programming languages (or a combination of both), it's often the case that we use one language to implement or describe another. If we use Lean to implement a decision procedure for propositional logic, propositional logic is the object language, the target of our implementation. If we use propositional connectives (and more) to prove the correctness of that procedure in Lean, then in that case we are using propositional logic as part of the metalanguage, the thing we are using to achieve our goal. One goal of this chapter is to clarify the sense in which Lean itself is a logical system, which is to say, its language can be used to state mathematical theorems and prove them. Using a logical foundation like Lean's as both a programming language and a mathematical language brings a number of benefits: - It allows us to specify the behavior of computer programs in the same language that we write them. - It allows us to prove, rigorously, that our computer programs are correct, which is to say, that they meet their specifications. - It allows us to enforce preconditions on our programs. For example, we can write functions whose input is required to be a positive integer, a requirement that is enforced statically, at compile time. Compiler optimizations can make use of this knowledge. - It allows us to compute with objects in our mathematical libraries. - It gives us ways of using computation reliably in mathematical proofs. Although we will not discuss it in this course, Lean also serves as its own *metaprogramming language*, which means that we can use Lean to develop automation that can help us construct programs and proofs. In that way, Lean becomes a self-extending system, meaning that we can improve its support for programming and theorem proving using the system itself. Lean's logical foundation is powerful and expressive enough to carry out any mathematical argument, and proof assistants are now commonly used for hardware and software verification. This chapter, we introduce the basics of using Lean as a proof assistant by focusing on the treatment of propositional logic. :numref:`Chapter %s` will extend this to equational reasoning and proof by induction, but even that only scratches the surface. You can learn more about the use of Lean as a proof assistant in either `Mathematics in Lean `_ or `Theorem Proving in Lean 4 `_. You may also enjoy interactive tutorials, like the Natural Number Game, found on the `Lean Game Server `_. For the examples in this chapter, we use the following imports: .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: imports :end-before: -- end textbook Since importing a file also imports everything it depends on, these serve to make available to us a modest portion of Lean's mathematical library, Mathlib. .. _section_propositional_logic: Propositional logic ------------------- In Lean, we can declare variables that range over propositions and then use them to build more complicated propositions. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: Prop :end-before: -- end textbook Hovering over the symbols will give you options for typing them. Using ``\and``, ``\or``, ``\to``, ``\iff``, and ``\not`` will work. In Lean, you state a theorem with the keyword ``theorem``. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: id proof :end-before: -- end textbook What follows the keyword ``by`` is what is known as a *tactic proof*, that is, a list of commands that tells Lean how to construct a proof of the theorem. In the next section, we will say more about how proofs are represented in Lean and what tactics do underneath the hood. Here, instead, we will focus on how to use them. Stating a theorem creates a *goal*, namely, the theorem to be proved. If you put your cursor at the beginning of the line ``intro h``, the infoview window shows the following goal: .. code-block:: none P Q R S: Prop ⊢ P → P If you put your cursor at the end of the line, you will see that the goal has changed to: .. code-block:: none P Q R S: Prop h : P ⊢ P When the cursor is at the beginning of the line ``intro h``, the highlighting in the infoview window helpfully shows what is about to change, and when you move the cursor to the end of the line, the highlighting shows what has just changed. The notation should remind you of a sequent in natural deduction: the second goal says that we are given propositions ``P``, ``Q``, ``R``, and ``S`` together with the assumption that ``P`` holds, labelled as ``h``, and we are to prove ``P``. The command ``apply P`` finishes it off, leaving you with the happy message, "no goals." The label ``h`` is arbitrary, and you can use any valid identifier instead. It's conventional to use the letter ``h`` for hypotheses. The information before the turnstile is called the *context*. The right side of the sequent is also sometimes confusingly called the goal, but we will call it the *conclusion* of the sequent and reserve the term "goal" for the entire sequent. You can use the ``example`` keyword to prove a theorem without naming it: .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: id proof 2 :end-before: -- end textbook When an ``apply`` command finishes off the goal exactly, it is conventional to use the ``exact`` tactic instead: .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: id proof 3 :end-before: -- end textbook You can also end a proof with the ``done`` tactic, which does nothing but declare that there are no more goals. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: id proof 4 :end-before: -- end textbook It is often useful to put a ``done`` at the end of a proof while you are still writing it. Lean gives you an error message if the proof isn't over, and the error message tells you the goals that remain to be proved. It can be convenient to force Lean to put the error message on the ``done`` command rather than somewhere lower down in the file. You can then delete the ``done`` when you are finished with the proof. Notice, by the way, that you can learn more about a tactic by hovering over it in VS Code. The ``apply`` tactic can also be used to apply an implication. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: apply :end-before: -- end textbook In this example, applying the assumption ``P → Q`` to the goal reduces the task of proving ``Q`` to the task of proving ``P``. To prove a conjunction, we can use the ``constructor`` tactic: .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: and example :end-before: -- end textbook The command ``intro hP hQ`` is shorthand for writing ``intro hP`` followed by ``intro hQ``. The ``constructor`` tactic tells Lean we intend to prove ``P ∧ Q`` by proving each conjunct in turn. As a result, after that line, there are *two* goals to prove, one for each conjunct. The first period focuses on the first goal, which is solved using ``hP``, and the second period focuses on the second goal, which is using ``hQ``. Lean is whitespace sensitive, and once you focus on a goal, Lean expects you to maintain the indentation until the goal is solved. You can check that the proof still works if you delete the periods. Structuring a proof in this way, however, tends to make it more readable and robust. At this point, there is a trick that is worth mentioning. At any point in a proof, you can solve the current goal with the ``sorry`` tactic. You can prove any theorem at all using ``sorry``. It's cheating, and the squiggly line the editor puts underneath the name of the theorem tells you as much. But it is often a useful device when writing proofs, because it means you can temporarily close a goal to work on others, and then come back to it. The natural way to *use* a conjunction ``h : P ∧ Q`` in a hypothesis is to split it to the hypotheses ``hP : P`` and ``hQ : Q``. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: another and example :end-before: -- end textbook Here the angle brackets denote a conjunctive pattern for Lean to match ``h`` against, and the ``rcases`` tactic does the matching, removing ``h : P ∧ Q`` and replacing it with ``hP : P`` and ``hQ : Q``. The corresponding proof for disjunction is dual: .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: or example :end-before: -- end textbook Here we use a vertical bar with ``rcases h`` because the split is disjunctive, resulting in two goals: one in which we have ``hP : P`` in the context and one in which we have ``hQ : Q``. The ``right`` tactic tells Lean that we want to prove ``Q ∨ P`` by proving ``P``, and the ``left`` tactic tells Lean that we want to prove ``Q ∨ P`` by proving ``Q``. Notice that in contrast to casing on a conjunction, which results in one new goal and two new hypotheses, casing on a disjunction results in two new goals, each with one new hypothesis. Recall from :numref:`section_natural_deduction` that in the natural deduction proof system, rules for the connectives can be categorized as either introduction rules or elimination rules. Even though we have not yet clarified the relationship between natural deduction and Lean's internal logic, you should notice that the tactics we have given so far follow a similar pattern: - Given a goal of the form ``P → Q``, we can use the ``intro`` tactic to prove it. - Given a hypothesis of the form ``h : P → Q``, we can use the ``apply`` tactic to use it. - Given a goal of the form ``P ∧ Q``, we can use the ``constructor`` tactic to prove it. - Given a hypothesis of the form ``h : P ∧ Q``, we can use the ``rcases`` tactic to use it. - Given a goal of the form ``P ∨ Q``, we can use the ``left`` and ``right`` tactics to prove it. - Given a hypothesis of the form ``h : P ∨ Q``, we can use the ``rcases`` tactic to use it. In Lean, negation ``¬ P`` is defined to be ``P → False``. For most purposes, the two expressions are interchangeable. This means that you can prove ``¬ P`` by assuming ``P`` and deriving ``False``, and if you have ``hnp : ¬ P``, you an reduce the task of proving ``False`` to the task of proving ``P``. In the next example, the ``intro`` tactic implements the first strategy, and the ``apply`` tactic implements the second. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: negation :end-before: -- end textbook After the second ``intro``, we have ``h : P → Q``, ``hnQ : ¬ Q``, and ``hP : P`` in the context and ``False`` as the desired conclusion. Applying ``hnQ`` leaves us the goal of proving ``Q``, which we do using ``h`` and ``hP``. There is no introduction rule for falsity; there is no canonical way to prove ``False``! If we assume ``h : False``, we can reach any conclusion we want, using either ``contradiction`` or ``rcases h``. Intuitively, there is no proof of ``False``, so if we have ``h : False``, there are no cases to consider. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: ex falso :end-before: -- end textbook As a convenience, if you have ``h : P`` and ``hnP : ¬ P`` in the context, the contradiction tactic solves the goal automatically. The principles we have used before all fall within what is known as *intuitionistic* logic. Many mathematical arguments require *classical* logic, which is embodied in the *law of the excluded middle*, ``P ∨ ¬ P``. This is embodied in the ``by_cases`` tactic, which lets us split on cases. In the proof below, we have ``hP : P`` in the first case and ``hnP : ¬ P`` in the second. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: by_cases :end-before: -- end textbook Classical reasoning is also embodied in the ``by_contra`` tactic, which allows us to do proof by contradiction. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: by_contra :end-before: -- end textbook Applying ``by_contra hnP`` to a goal with conclusion ``P`` adds ``hnP : ¬ P`` to the context and asks us to prove ``False``. You can think of ``P ↔ Q`` as an abbreviation for ``(P → Q) ∧ (Q → P)``. It is not implemented exactly that way in Lean, but like a conjunction, the task of proving such a statement can be split into the forward and backward directions. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: iff :end-before: -- end textbook In the first example, the underscore omits a label for the hypothesis, since we don't needed it. If you use a label, Lean's built in linter will warn you that the label is unused. The hypothesis still appears in the context with an inaccessible name, and can be used by automation. If you replace the underscore with a dash (``-``), the ``rcases`` tactic clears it entirely from the context. The methods in this section are *complete* for classical propositional logic, which is to say, any proof in classical propositional logic can be carried out using these methods. That is not to say that these methods are the most *efficient*; Lean offers both automation and syntax for writing proofs more compactly. As far as automation is concerned, all the proofs in this section can be carried out using the ``tauto`` tactic, which stands for "tautology." .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/propositional_logic.lean :start-after: -- textbook: tauto :end-before: -- end textbook But writing propositional proofs by hand is a good way to learn how propositional logic works in Lean, and in more complicated proofs we often need to carry out simple logical manipulations by hand. .. _section_proof_terms: Proof terms ----------- Remember that, in Lean's foundation, everything is expression. In particular, if an expression ``P`` has type ``Prop``, then a term ``p`` of type ``P`` is interpreted as a proof of ``P``. Lean's proof language is therefore essentially the same as its programming language, which means that we can write proofs the same way we write programs. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean :start-after: -- textbook: proof terms :end-before: -- end textbook Instead of using the identifier ``def``, it is conventional to use the word ``theorem`` to name the proof of a proposition. Each keyword serves to assign an expression to an identifier; the main difference is that theorems are marked *opaque*, which means that they are generally not unfolded. A proof written this way is called a *proof term*. The tactic proofs described in the previous section are nothing more than instructions that tell the system how to construct such an expression. The syntax for proof terms, in turn, is closely related to natural deduction. The ``#explode`` command prints proof terms in a format that is closer to the presentation of natural deduction in :numref:`section_natural_deduction`. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean :start-after: -- textbook: exploding proof terms :end-before: -- end textbook Don't look too hard for an exact correspondence, because the details differ. But Lean's foundation can be seen as a vast generalization of natural deduction, giving rise to its uniform treatment of proofs and programs. The analogy between the two is known as the Curry-Howard correspondence, and it explains the fact that the introduction and elimination rules for the connectives look a lot like the constructors and destructors for the corresponding data types. The examples above show that the introduction and elimination rules for conjunction parallel the constructors and destructors for the pair data type, and the introduction and elimination rules for disjunction parallel the constructors and destructors for the sum data type. In Lean's foundation, the introduction and elimination rules for implication are exactly lambda abstraction and function application, respectively. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean :start-after: -- textbook: implication :end-before: -- end textbook In Lean, ``¬ P`` is defined to be ``P → False``. The following proof assumes ``P`` and ``¬ P``, concludes ``⊥``, and then uses the *ex falso* principle to conclude ``Q``. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean :start-after: -- textbook: negation and false :end-before: -- end textbook Lean allows the use of anonymous constructors and projections with proof terms just as with data: .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean :start-after: -- textbook: anonymous constructors :end-before: -- end textbook You can use proof terms in a tactic proof: .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean :start-after: -- textbook: tactics and proof terms :end-before: -- end textbook In fact, under the hood, a tactic proof is essentially a program that constructs the relevant proof. Here are some more examples: .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean :start-after: -- textbook: more tactics and proof terms :end-before: -- end textbook Lean's ``show_term`` tactic will show you the proof term that a tactic block produces, and it will even given you the option of clicking to replace the tactic block by an explicit use of that term. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean :start-after: -- textbook: show_term :end-before: -- end textbook You can read more about Lean expressions in `Theorem Proving in Lean 4 `_. For the most part, in this course, we will focus on tactic proofs, but you should feel free to use a proof term with ``apply`` or ``exact`` when you feel like it. More importantly, you should keep in mind that at the end of the day, what you are doing is constructing something like a natural deduction proof, represented as an expression in Lean's foundation. You can therefore think of Lean as an engine for manipulating expressions that can represent data types, statements, programs, and proofs. Tactics are pieces of automation that are designed to help us construct these expressions. .. _section_structured_proofs: Structured proofs ----------------- Tactics allow us to work backward to prove a goal by reducing it to simpler ones. Lean also provides a means of reasoning forward from hypotheses, using the ``have`` tactic: .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean :start-after: -- textbook: have :end-before: -- end textbook Here the first line of the proof states an intermediate goal of proving ``Q``. The result is named ``hQ``, which we are then free to use. Using ``have`` tends to make proofs more readable because the text displays the stepping stones to the main goal. It also tends to make proofs more robust, in that errors are localized to small, compartmentalized parts of the proof. If you omit the keyword ``by``, you can use a proof term to fill an easy ``have``: .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean :start-after: -- textbook: have again :end-before: -- end textbook You can even write ``have hQ := h1 h3`` in the second line of the first proof, omitting the type ascription, because Lean can figure that out. Of course, this sacrifices readability somewhat. You can generallly eliminate a ``have`` statement by inlining the result. For example, replacing ``hQ`` by ``h1 h3`` yields the first proof below: .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean :start-after: -- textbook: inlining the result :end-before: -- end textbook The proof ``by exact h2 (h1 h3)`` is equivalent to just presenting the proof term ``h2 (h1 h3)``, as we do in the second example. Lean also has a ``show`` tactic, which declares the goal we are about to solve. .. literalinclude:: ../../LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean :start-after: -- textbook: have and show :end-before: -- end textbook The ``show`` tactic mainly serves to make a proof more readable, though it does a little more work than we are letting on here. For example, if there are multiple goals left to prove, ``show`` fill focus on the first one that matches the given statement. Exercises --------- Complete the following proofs in Lean. .. code-block:: lean import Mathlib.Data.Real.Basic variable (P Q R S : Prop) example : P ∧ Q ∧ (P → R) → R := by sorry example : (P → Q) ∧ (Q → R) → P → r := by sorry example (h : P → Q) (h1 : P ∧ R) : Q ∧ r := by sorry example (h : ¬ (P ∧ Q)) : P → ¬ Q := by sorry example (h : ¬ (P → Q)) : ¬ Q := by sorry example (h : P ∧ ¬ Q) : ¬ (P → Q) := by sorry example (h1 : P ∨ Q) (h2 : P → R) : r ∨ Q := by sorry example (h1 : P ∨ Q → R) : (P → R) ∧ (Q → R) := by sorry example (h1 : P → R) (h2 : Q → R) : P ∨ Q → R := by sorry example (h : ¬ (P ∨ Q)) : ¬ P ∧ ¬ Q := by sorry example (h : ¬ P ∧ ¬ Q) : ¬ (P ∨ Q) := by sorry -- this one requires classical logic! example (h : ¬ (P ∧ Q)) : ¬ P ∨ ¬ Q := by sorry -- this one too example (h : P → Q) : ¬ P ∨ Q := by sorry