Lecture 18: Proving with tactics

1 Purpose

Learning how to use tactics to construct proofs

2 Outline

2.1 Tactics

Up to now, we’ve mostly been writing proofs as explicit terms, but that is something that we will actually do quite rarely. It turns out, rather than constructing the terms directly, which for complicated proofs, might be rather involved, we can instead invoke higher-level tactics that will construct a term for us.

Today, we’re going to focus primarily on the "Lean Infoview", and how it, along with tactics, allow us to much more easily, and interactively, construct proofs.

We can switch into "tactic mode" at any point using the keyword by. On their own, tactics can make our code harder to read, as they allow you to leave out details apparent in the terms, but the "Lean Infoview" provides interactive feedback that results in a really nice environment for constructing proofs. You’ve already seen one tactic, rfl, which we used for unit tests in the current homework. rfl performs evaluation on both sides, and then solves trivial equalities: equalities that are the exact same on both sides.

Let’s see how this works:

example : 1 + 1 = 2 := by rfl

example creates anonymous (unnamed) theorems.

To learn more about tactics, let’s see a slightly more involved example, returning to our simple theorem about And:

def and_2'' : forall {P  Q : Prop}, P ∧ Q -> Q := 
  by intros P Q _
     cases ‹P ∧ Q›
     exact ‹Q›

Here, we use three tactics. The first, intros, takes identifiers from the goal and moves them into the premise of the proof. This corresponds, in the underlying term, to a function with identifiers. Here we give explicit names to the propositions P and Q, but giving no name to the conjunction, indicated by an underscore.

The Infoview will always have some number of goals (none if the proof is complete), and each one will have assumptions or premises (or hypotheses) that are available to use in the proof of that goal. The assumptions are separate from the obligation by a turnstile \vdash, and the goal is the proposition that we are trying to prove. This is all shown under the "Tactic state" header.

We then do case analysis on one of my hypotheses: which one? The one we didn’t give a name to, and so we refer to it by its type, which Lean allows me to do using "french quotes" (typed as \f< and \f>): provided there is only one hypothesis with that type, this is not ambiguous, and it can be easier to read. Case analysis on a pair will then give me hypotheses for the two conjuncts. Note that it does not manipulate the goal in this case, but simply changes the form of the hypotheses. If we did case analysis on a disjunction (also known as a sum), we would get multiple goals, as there would be multiple different cases to consider. Case analysis in tactics corresponds to pattern matching in the underlying terms, though the Infoview state can make it a bit easier to manage.

At this point, we can complete the proof by saying we want the one with type Q, using the tactic exact. This is a tactic that takes a term, and if it matches the goal, it completes the proof. It is the way to go back into "term mode" from "tactic mode" (it is the inverse of by in this way). All of the proofs we did before we started using tactics could be done "in tactic mode" by using a single invocation of exact, though it would be a bit pointless.

There are many other ways we could write this. First, we could use the tactic assumption to complete the proof: it looks for a hypothesis that matches the goal.

def and_2''' : ∀ {P  Q : Prop}, P ∧ Q -> Q := 
  by intros P Q _
     cases ‹P ∧ Q›
     assumption

We also could have given an explicit name to the conjunction, and referred to that with cases:

def and_2'''' : forall {P  Q : Prop}, P ∧ Q -> Q := 
  by intros P Q pq
     cases pq
     assumption

We can also be more precise with my case analysis. Conjunctions are created with And.intro, which has two fields, so we can pattern match to get:

def and_2''''' : forall {P  Q : Prop}, P ∧ Q -> Q := 
  by intros P Q pq
     cases pq with | intro a b => exact b

This form of cases is very close to how match looks in the term language. When doing case analysis on something like And, knowing which case we are in doesn’t do much (as there is only one), but as we’ll see below, when doing case analysis on inductive types with multiple constructors (like Or), we will want to be able to identify the case of our proof. While we can write it in the matching style, we can also simply identify the case we want to work on with case:

def and_2'''''' : forall {P  Q : Prop}, P ∧ Q -> Q := 
  by intros P Q pq
     cases pq
     case intro a b => exact b

This is very similar, but can be easier to read. In general, if there are multiple (named) goals we can switch to one of them with case, and we don’t actually have to bind any variables (they will be anonymous), so we could do this proof as:

def and_2''''''' : forall {P  Q : Prop}, P ∧ Q -> Q := 
  by intros P Q pq
     cases pq
     case intro =>
      exact ‹Q› 

3 Re-doing a propositional logic proof

Let’s prove a theorem that you did in HW1:

\neg (P \lor Q) \equiv \neg P \land \neg Q

Here we’ve written \equiv as "if-and-only-if" double implication, rather than propositional equality. Both allow Lean to rewrite.

theorem demorgan1 : forall {P Q : Prop}, ¬(P ∨ Q) ↔ ¬P ∧ ¬Q :=
  by intros P Q
     constructor
     case mp => intro
                constructor
                case left => 
                  intro; apply ‹¬(P ∨ Q)›; apply Or.inl; assumption
                case right => 
                  intro; apply ‹¬(P ∨ Q)›; apply Or.inr; assumption
     case mpr => intro
                 intro
                 cases ‹¬ P ∧ ¬ Q› 
                 cases ‹P ∨ Q›
                 case inl => apply ‹¬P›; assumption
                 case inr => apply ‹¬Q›; assumption

Here we used two new tactics:

Interestingly, the other proof that you did:

\neg (P \land Q) \equiv \neg P \lor \neg Q

cannot be done in the core logic of Lean. The issue is that it is not constructive; it can be done if we add classical axioms.

Stepping back: proofs here vs. proofs with truth tables

Now that we’ve seen a few proofs, including doing a proof that you did in propositional logic, it’s important to understand the difference between proofs in Lean and proofs in propositional logic.

In propositional logic, all variables can be either true or false, and thus any formula can be computed via a finite truth table. In a higher order logic like Lean, propositional variables are not either true or false, but rather, they are either provable or not provable. For a statement to be provable, it means that we have constructed a proof term with that type, but that type may involve data of arbitrary size, and thus the truth or falseness of a given statement cannot be determined by a finite truth table. Thus while the proof we just did of one of De Morgan’s laws is syntactically the same as what you did in HW1, it is a much more powerful proof, as it holds for any provable propositions, not just for T/F propositional variables. Another way to think about this is that Lean has propositional logic embedded, by way of the boolean data type. Thus, our proof from HW1 was the following:

theorem demorganprop : 
  forall {P Q : Bool}, not (or P Q) = and (not P) (not Q) :=
    by intros P Q
       cases P <;> cases Q <;> rfl

Here we can see a new tactic: <;>, which is used to chain tactics together by applying what follows to everything that comes out of the former. Here we can see that by doing case analysis on the two boolean inputs, we can complete the proof trivially, as once we have constants, simply evaluating the expression will give us the result.

Attemptying to do that for the other proof will fail, as we cannot do case analysis on Prop: it is not an inductive type with a finite number of constructors.