Propositions

What we will learn here.

Brief summary: A proposition is a true/false statement. Here we will learn how to prove basic abstract propositions in Lean. We will learn notation: if P and Q are propositions, then P → Q means “P implies Q”, P ∧ Q means “P and Q”, P ∨ Q means “P or Q”, and ¬ P means “not P”. For each of these concepts we will learn how to construct them and how to eliminate them in Lean. For example, given proofs of P and Q we will learn how to construct a proof of P ∧ Q, and conversely given a proof of P ∧ Q we will learn how to eliminate it by turning it into a proof of P and a proof of Q. We will learn the use of the following basic tactics: exact, assumption, intro, left, right, cases and split.

Introduction

A proposition is a true/false statement, like \(2+2=4\) or \(2+2=5\). Rather than working with specific propositions here, we will just work with variables called things like P or Q or R. So P could represent the statement \(2+2=1000\) and Q could represent the statement of Fermat’s Last Theorem.

Here’s an example of a situation you might run into in Lean:

P Q R : Prop,
HP : P,
HQ : Q,
⊢ P

See the “turnstile” symbol `` ⊢``? The stuff before that is our assumptions. The stuff after it is what we have to prove. In the situation above, P Q R : Prop means that we’re assuming that we have three propositions P, Q and R. We also are assuming HP : P and HQ : Q, which means that we are also assuming that we have two proofs: HP is a proof of P and HQ is a proof of Q. Our goal, the thing we want to prove, is P. Well this is pretty easy to do, because one of the things we already have is HP, a proof of P. So we can prove P by writing exact HP, or assumption (both work).

Try it for yourself (assuming you have an internet connection). Here is the code which puts Lean into the situation above, and instead of the proof I have written sorry. Click “try it!” below and a new window will open running a live Lean session. You might want to rig it so that you can see both this window and the Lean window at the same time.

try it!

example (P Q R : Prop) (HP : P) (HQ : Q) : P :=
begin
  sorry,
end

Wait for the Lean window to stop saying “(running)” at the top. You should see a complaint on the right that we used sorry, and you might spot that example is underlined in green. This means that Lean is unhappy – you have not proved the theorem yet. Now change the sorry, on the left to exact HP, and check that Lean is happy that you’ve proved the theorem (i.e. solved the goal). Lean is happy when there is nothing underlined in red or green on the left. If you move your cursor to after the word end you will see no output at all on the right – this is another indication that Lean is happy. exact is an example of a tactic, and between the begin and end of a proof Lean expects tactics, separated by commas.

Change your proof to exact HQ, and see that Lean becomes unhappy again: HQ is not a proof of P. Change it to assumption, and it’s happy once more. Change it to exact P, and it doesn’t work – P is the statement, not the proof. Lean wants the proof of P, which is HP. Don’t confuse a statement and its proof. You can see the difference between a proposition and its proof; P : Prop means “the type of P is Prop”, which is a fancy way of saying that P is a proposition (a true/false statement)

Change your proof back to a correct proof, e.g. exact HP,, and then click around a bit. See that sometimes there is no output on the right, and sometimes Lean prints something? If you are in the middle of the proof (e.g. if your cursor is just after the word begin) then Lean prints the goal, which has not been proved yet: the proof happens one line later. Move your cursor up and down the arrow keys and see how the output on the right changes.

Implications P → Q (intro, apply)

If P and Q are propositions, then so is P → Q, pronounced “P implies Q”. Here is the truth table for P → Q:

P	Q	P → Q
T	T	T
T	F	F
F	T	T
F	F	T

We’re ready to see how to work with P → Q in Lean. The high-powered summary: to construct it, we use intro, and to eliminate it we use apply. Let me explain much more about what I mean.

First, let’s assume we have a proof of P → Q. Let’s see how to deduce a proof of Q from a proof of P.

try it!

theorem easy (P Q : Prop) (HP : P) (HPQ : P → Q) : Q :=
begin
  sorry,
end

Click “try it!” to try solving this goal. Delete sorry, and see Lean complaining that there are unsolved goals. Lean’s state looks like this:

P Q : Prop,
HP : P,
HPQ : P → Q
⊢ Q

Our assumptions are that we have two propositions P and Q, and a proof (called HP) of P, and a proof (called HPQ) that P implies Q. You can get that implication arrow by writing \r (r for right) by the way. We want a proof of Q.

There are several ways to prove this theorem. The big question of course is how to use HPQ. You can use it by apply ing it:

try it!

theorem easy (P Q : Prop) (HP : P) (HPQ : P → Q) : Q :=
begin
  apply HPQ,
  sorry,
end

Applying HPQ, the proof of P → Q, turns the goal of proving Q to the new goal of proving P. apply is of course a tactic. You should be able to finish the job now, so replace the sorry and finish the proof. Then put your cursor at the beginning of a line and move up and down through the proof script – you will see the goal change as you move around.

An alternative approach is to regard HPQ as a function which sends proofs of P to proofs of Q. This is quite a weird way of thinking about what P → Q means at first, but Lean is happy to think about HPQ as a function this way. This means that HPQ(HP) is a proof of Q, so another way of proving the theorem is

try it!

theorem easy (P Q : Prop) (HP : P) (HPQ : P → Q) : Q :=
begin
  exact HPQ(HP),
end

We could even say that because HPQ is a function expecting a proof of P as input, we don’t even need the brackets, and can even write HPQ HP:

try it!

theorem easy (P Q : Prop) (HP : P) (HPQ : P → Q) : Q :=
begin
  exact HPQ HP,
end

Using apply, or evaluating a proof of P → Q at a proof of P, are two ways to eliminate (i.e. use) a proof of P → Q. What about the other way? What if our goal is to prove P → Q?

try it!

theorem prove_P_implies_Q (P Q : Prop) (HQ : Q) : P → Q :=
begin
  sorry,
end

To prove P → Q the idea is that we should assume we have a proof of P, and then simply try to prove Q. The way to do this in Lean is the intro tactic (by the way, lines which begin -- are just comments):

try it!

theorem prove_P_implies_Q (P Q : Prop) (HQ : Q) : P → Q :=
begin
  intro HP,
  -- we now have a proof HP of P in our assumptions
  -- and our goal is now to prove Q
  exact HQ,
end

The intro tactic is a constructor for P → Q – if our goal is P → Q then we can type intro HP and Lean then proves our goal, modulo some other simpler things (namely a proof of Q) which we can work on later.

Exercise (P → P)

Try proving this:

try it!

theorem P_implies_P (P : Prop) : P → P :=
begin
  sorry,
end

Exercise (intros)

Now see if you can prove this:

try it!

theorem needs_intros (P Q R : Prop) (HR : R) : P → (Q → R) :=
begin
  sorry,
end

A related question: what do you think P → Q → R means in Lean? It will surely either mean (P → Q) → R or P → (Q → R) (a fancy equivalent way of saying this is that → is either left associative or right associative): try replacing P → (Q → R) above with P → Q → R and see if the proof still works.

true, false, and ¬

Some propositions, like the Riemann Hypothesis and other hard maths questions, are currently open questions – we don’t know whether they’re true or false. At the other extreme, there is a proposition called true which is true by definition, and whose proof is called trivial:

try it!

theorem very_easy : true :=
begin
  exact trivial,
end

We could say that trivial is a constructor for true. At the other extreme, there is also a proposition called false, which is false, and if you can prove this without any hypotheses at all then you’ve either found a contradiction in mathematics, which would surprise many experts, or a serious bug in Lean, which I guess could be possible, but again is unlikely. Note that false has no constructors at all!

try it!

theorem very_hard : false :=
begin
  sorry,
end

On the other hand, given some hypotheses which don’t add up, we can indeed sometimes prove false using them. For example, false → false is true, indeed it’s a special case of P → P, so we should be able to prove it no problem:

try it!

theorem false_implies_false : false → false :=
begin
  intro Hfalse,
  exact Hfalse,
end

After the intro Hfalse line, our state looks like this:

Hfalse : false
⊢ false

The moral is: you sometimes can prove false, but only if your assumptions don’t add up. In fact this is exactly what people do in the middle of a proof by contradiction.

But what is the point of having a proposition which is false? Well, I’ve already mentioned proofs by contradiction and we’ll come back to these in a minute. But also it comes up in Lean’s definition of “not” – if P is a proposition, then not P, written ¬ P in Lean (use \not to get the not symbol), is defined to mean P → false. Thinking about this, it makes sense: if P is true, then P → false is true → false, which is false, and on the other hand if P is false, then P → false means false → false, which is true.

Of course ¬ (¬ P) will have the same truth value as P. Let’s see if we can get Lean to prove that P implies ¬ (¬ P).

try it!

theorem not_not (P : Prop) : P → ¬ (¬ P) :=
begin
  sorry,
end

Our goal is an implication, so we can start with intro HP, and we will end up with the following state:

P : Prop,
HP : P
⊢ ¬¬P

Now our goal is ¬¬P and this is by definition ¬(¬P) which is by definition (¬P) → false. This is another implication, so we can eliminate it with the intro tactic again:

try it!

theorem not_not (P : Prop) : P → ¬ (¬ P) :=
begin
  intro HP,
  intro HnP,
  sorry,
end

Things are perhaps not looking good now, or at least they’re looking a bit weird. Lean’s state is this:

P : Prop,
HP : P,
HnP : ¬P
⊢ false

so our goal is something which can’t be proved. Actually that’s not quite true – our goal is something which can’t be proved given no hypotheses at all. But here we are still OK – our hypotheses are contradictory; we have a proof that P is true and also a proof that it’s not true, so we should be able to deduce a contradiction, which is the same thing as a proof of false. You might want to think about how to do this, before we move on.

The trick is that HnP is a proof of ¬P, or in other words a proof of P → false. Our goal is false, so we can apply HnP to reduce our goal from false to P. If this seems a bit weird, just imagine that Q was a random proposition, and our goal was Q. If we had a proof of P → Q we could apply this proof and reduce our goal to proving P. This is exactly what we’re doing here, in the special case that Q turns out to be false.

try it!

theorem not_not (P : Prop) : P → ¬ (¬ P) :=
begin
  intro HP,
  intro HnP,
  apply HnP,
  exact HP,
end

Remember – ¬ P is just another way of saying P → false.

Exercise (contrapositive)

The contrapositive of the proposition P → Q is the proposition ¬ Q → ¬ P. The contrapositive of an implication is equivalent to the implication itself. See if you can deduce the contrapositive of P → Q given a proof of P → Q.

try it!

theorem contrapositive
  (P Q : Prop) (HPQ : P → Q) : ¬ Q → ¬ P :=
begin
  sorry,
end

For a bonus point, can you come up with a three-line proof of this theorem which uses the intro tactic twice and then the exact tactic once?

Working with “or”: P ∨ Q

P ∨ Q is true if either P is true, or Q is true (or both). Here’s a truth table:

P	Q	P ∨ Q
T	T	T
T	F	T
F	T	T
F	F	F

How do we construct a proof of P ∨ Q? Well, there are two ways. We could either deduce it from a proof that P is true, or from a proof that Q is true. So there should be two constructors, that is, two ways of making progress if our goal is P ∨ Q. The corresponding two tactics are called left and right.

try it!

theorem P_implies_P_or_Q (P Q : Prop) (HP : P) : P ∨ Q :=
begin
  left,
  exact HP,
end

Exercise (right)

Try the other one for yourself:

try it!

theorem Q_implies_P_or_Q (P Q : Prop) (HQ : Q) : P ∨ Q :=
begin
  sorry,
end

Of course, deciding which constructor to use depends on the situation you are in. Choosing the wrong one can leave you in an impossible situation.

try it!

theorem dont_get_lost (P Q :Prop) (HQ : Q) : P ∨ Q :=
begin
  left,
  -- the goal is no longer provable!
  sorry
end

If you take a wrong turn, you might be in trouble. Go back and try something else.

We’ve seen the two constructors for “or”, but what about the eliminator? In other words, how can we use a hypothesis of the form P ∨ Q? Let’s try and prove that P ∨ Q implies Q ∨ P.

try it!

theorem or_symmetry (P Q : Prop) : P ∨ Q → Q ∨ P :=
begin
  sorry,
end

Fire up a Lean session with the above code. Our first move is obvious – intro HPQ. But now we can’t use left or right next, because we don’t know which one we are supposed to be proving. We need to eliminate (i.e., use) HPQ first. We can do this with the cases tactic.

try it!

theorem or_symmetry (P Q : Prop) : P ∨ Q → Q ∨ P :=
begin
  intro HPQ,
  cases HPQ with HP HQ,
  sorry,
end

Try that. Wooah! Something weird happened!

2 goals
case or.inl
P Q : Prop,
HP : P
⊢ Q ∨ P

case or.inr
P Q : Prop,
HQ : Q
⊢ Q ∨ P

Instead of one goal, we now have two! In the first goal, we have a proof HP of P, and in the second we have a proof of Q. So now we want to go right in the first goal, and left in the second. What happens if we just type another tactic? Turns out it just gets applied to the goal at the top. So we could now finish the proof like this:

try it!

theorem or_symmetry (P Q : Prop) : P ∨ Q → Q ∨ P :=
begin
  intro HPQ,
  cases HPQ with HP HQ,
  right,
  exact HP,
  left,
  exact HQ,
end

But this is generally regarded as bad style. There are two approved ways to do this; the first is to indent two more spaces whenever a new goal appears, and then unindent when one disappears, like this:

try it!

theorem or_symmetry (P Q : Prop) : P ∨ Q → Q ∨ P :=
begin
  intro HPQ,
  cases HPQ with HP HQ,
    right,
    exact HP,
  left,
  exact HQ,
end

The second is to use squiggly brackets and deal with each goal individually:

try it!

theorem or_symmetry (P Q : Prop) : P ∨ Q → Q ∨ P :=
begin
  intro HPQ,
  cases HPQ with HP HQ,
  { right,
    exact HP,
  },
  { left,
    exact HQ,
  },
end

Try running the above code in the Lean Web Editor, and move your cursor around to see what these squiggly brackets do. It can get confusing if there is more than one goal, and this technique ensures that only one goal can be seen at a time.

What do you think cases does on a goal of the form P ∨ Q ∨ R? Try it and find out.

try it!

theorem or_experiment (P Q R : Prop) (HPQR : P ∨ Q ∨ R) : true :=
begin
  cases HPQR with H1 H2,
  sorry,
end

Operators like ∨ have an “associativity” in Lean, and ∨ is right-associative, which means that P ∨ Q ∨ R is parsed by Lean as P ∨ (Q ∨ R).

Exercise (or_associativity)

Try proving this:

try it!

theorem or_associative (P Q R : Prop) :
P ∨ (Q ∨ R) → (P ∨ Q) ∨ R :=
begin
  sorry,
end

Working with And (P ∧ Q)

If P and Q are propositions, then P ∧ Q is the proposition which is true exactly when both P and Q are true. Here is the truth table for and:

P	Q	P ∧ Q
T	T	T
T	F	F
F	T	F
F	F	F

If our goal is of the form P ∧ Q, then the tactic we use to construct a proof of it is split. Before you run the following code, think a little about what should happen after the split statement:

try it!

theorem and_definition (P Q : Prop) (HP : P) (HQ : Q) : P ∧ Q :=
begin
  split,
  -- what will the state be now?
  sorry,sorry,
end

The split tactic turns our one goal of proving P ∧ Q into two goals, namely P and Q.

Exercise (and_definition)

Finish the above proof.

So split can be thought of as a constructor. What about the eliminator? It’s just cases again. In contrast to the and example, cases doesn’t create two goals from one – it just creates two hypotheses from one. Here is a proof of symmetry of and:

try it!

theorem and_symmetric (P Q : Prop) : P ∧ Q → Q ∧ P :=
begin
  intro HPQ,
  cases HPQ with HP HQ,
  split,
  { exact HQ,},
  { exact HP,},
end

Exercise (transitivity of and)

Try this one.

try it!

theorem and_transitive (P Q R : Prop) :
(P ∧ Q) ∧ (Q ∧ R) → (P ∧ R) :=
begin
  sorry,
end

Dealing with iff (↔)

From the point of view of general abstract behaviour, iff (you can get the symbol with \iff in the Lean Web Editor) is rather like “and”. To prove P ∧ Q you need to supply two things – a proof of P and a proof of Q. Similarly, to prove P ↔ Q you have to supply both a proof of P → Q and of Q → P. So, just as with and, if your goal is P ↔ Q you can make progress using split, and if you have a hypothesis H : P ↔ Q you can use the tactic cases H with HPQ HQP, which will leave you with two new hypotheses HPQ : P → Q and HQP : Q → P. Try these.

Exercise (symmetry of iff)

try it!

theorem iff_symmetric (P Q : Prop) : (P ↔ Q) ↔ (Q ↔ P) :=
begin
  sorry
end

Exercise (transitivity of iff)

try it!

theorem iff_transitive (P Q R : Prop) :
(P ↔ Q) ∧ (Q ↔ R) → (P ↔ R) :=
begin
  sorry
end

The rewrite tactic

If you did the above exercise you might have found it a bit tedious. But in fact there are loads of tricks which you can use to make proofs shorter. To give you an example, here is an extremely short proof of iff_transitive :

try it!

theorem iff_transitive (P Q R : Prop) :
(P ↔ Q) ∧ (Q ↔ R) → (P ↔ R) :=
λ ⟨H1,H2⟩,by rwa H1

As you can see, Lean has lots of secrets, many of which have not yet been divulged. But here is one – the rewrite tactic, commonly abbreviated to rw.

try it!

theorem iff_transitive (P Q R : Prop) :
(P ↔ Q) ∧ (Q ↔ R) → (P ↔ R) :=
begin
  intro H,
  cases H with HPQ HQR,
  rw HPQ,
  exact HQR
end

What’s happening here is that because HPQ is a proof of (P ↔ Q), and hence a proof that P and Q are logically equivalent, you can use the rw tactic to replace any P in the goal with a Q. Before the rewrite, the goal was P ↔ R, and afterwards it is Q ↔ R, which is precisely HQR. Rewriting can be done with any iff statement and also any equality, and is a powerful and useful part of Lean’s armoury.

If all else fails

Mathematicians think of propositions as statements which can either be true or false. But surprisingly, we never used this assumption in the above arguments, we could always argue directly rather than proving things by checking that the truth tables worked out in every case. Assuming that a general proposition is either true or false actually has a name - it’s called the “law of the excluded middle”, and it is called classical.em (em for “excluded middle”) in Lean. Here’s an example which we cannot prove given the tools introduced above:

try it!

theorem not_not (P : Prop) :
¬ (¬ P) → P :=
begin
  sorry
end

This is hopeless to do with the tools we have, because ¬ (¬ P) is barely usable as a hypothesis, and we really have to approach this one on a case by case basis. The trick is to break into the two cases P true and P false. We can do this because classical.em P is exactly the statement P ∨ ¬ P, and we can just do cases on this.

try it!

theorem not_not (P : Prop) : ¬ (¬ P) → P :=
begin
  cases (classical.em P) with HP HnP,
  { intro HnnP,
    exact HP,
  },
  { intro HnnP,
    exfalso,
    apply HnnP,
    exact HnP
  }
end

Note exfalso, which changes an arbitrary goal into the goal false by applying false → Q, a statement which is true for any goal Q.

Exercise (contrapositive)

We proved earlier that P → Q implied its contrapositive, ¬ Q → ¬ P. Now show that ¬ Q → ¬ P implies P → Q!

try it!

theorem contra (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) :=
begin
  sorry
end