More easy Lean proofs [difficulty : quite easy]

Pure mathematics is all about proofs, so we have to learn how to do proofs.

Let’s start with a super-abstract proof. Let’s just take three random mathematical true/false propositions P, Q and R, and let’s say that we know that P implies Q, and that Q implies R. Can we deduce that P implies R in Lean? Let’s take a look at this. Oh — to get the cute little arrow try writing “\to ” and to get the cool and sign try “\and “.

-- anything after two minus signs like this is a comment.

variables P Q R : Prop -- P, Q, R are now true/false statements.

-- Reminder : ∧ means "and".

theorem basic_logic : (P → Q) ∧ (Q → R) → (P → R) :=
begin
admit
end


Here “admit” means “I haven’t done that proof yet”. Sort-of like admitting defeat.

If you click here you’ll open a version of Lean running in your browser, with the above code pasted in.

OK so here is the strategy for proving this. First of all, we establish that P → Q and that Q → R. We want to prove that P → R, so we assume P, we deduce Q from P → Q and then we deduce R from Q → R

In Lean, it looks like this.

-- anything after two minus signs like this is a comment.

variables P Q R : Prop -- P, Q, R are now true/false statements.

-- Reminder : ∧ means "and".

theorem basic_logic : (P → Q) ∧ (Q → R) → (P → R) :=
begin
intro H, -- H is "P implies Q and Q implies R"
have HPQ : P → Q,
exact H.left,
have HQR : Q → R,
exact H.right,
clear H, -- we don't need it any more

-- We now have hypothesis HPQ, which is P -> Q
-- and hypothesis HQR, which is Q -> R.
-- We want to prove P -> R so let's assume P
-- and deduce R.

intro HP,
have HQ : Q,
exact HPQ HP, -- apply P->Q to P to get Q.
-- now we can get the goal
exact HQR HQ
end

This is hard to understand if you do not have the code running in a Lean session, so try it out, or, even better, get Lean running on a computer near you and cut and paste it in (who knows if this will work).

We can skip steps. Here are some shorter versions.

variables P Q R :  Prop

theorem basic_logic : (P → Q) ∧ (Q → R) → (P → R) :=
begin
intro H, -- H is "P implies Q and Q implies R"
intro HP, -- we want P -> R so let's assume P.
have HQ : Q,
exact H.left HP, -- apply P->Q to P to get Q.
-- now we can get the goal
exact H.right HQ
end

(click here)
or even

variables P Q R :  Prop

theorem basic_logic : (P → Q) ∧ (Q → R) → (P → R) :=
begin
intros H HP,
exact H.right (H.left HP)
end

(click here).

Try and figure out how this works. “Intros” is just introducing more than one thing at once. The thing in the brackets in the last but one line evaluates to a proof that Q is true.

Here’s another example. We need to talk about “not”. The idea is that not P is supposed to be the opposite of P — i.e. if P is true then not P is false, and if P is false then not P is true. There’s a really cute way to do this in logic — we can define not P to be P → false. This works because (true implies false) is false, and (false implies false) is true.

In VS Code or Lean online, you can write \not instead of not, and it will give you some weird symbol, which is the notation used by some computer scientists and logicians.

The contrapositive of the statement P → Q is not Q → not P. The contrapositive of a statement should follow from the statement itself, so we should be able to prove this:

variables P Q : Prop

example : (P → Q) → (¬ Q → ¬ P) :=
begin
admit
end


Try firing this up, and use the intro (or intros) commands to see how many hypotheses you can introduce. If you keep using “intro” to introduce as many hypotheses as you can all at once, then a funny thing happens!

variables P Q : Prop

example : (P → Q) → (¬ Q → ¬ P) :=
begin
intro HPQ, -- HPQ is P implies Q
intro HnQ, -- HnQ is "not Q"
-- our goal is now "not P", i.e. "P implies false".
intro HP, -- this is hypothesis P.
admit
end

Run this in Lean, click on “admit” and see what happens.

Rather weirdly, our goal (the thing we’re supposed to be proving) is now the word “false”, which apparently means that our job is to prove something which isn’t true. This sounds tricky, until you realise that we are allowed to assume a bunch of hypotheses which actually can’t all be true, so this is really just what a mathematician would call a proof by contradiction.

Our hypotheses include both P and “P implies Q”, so we can deduce Q from these. Another hypothesis is “Q implies false”, so if we put it all together we can indeed prove “false”! Try it yourself, or see this in action here.

For an even cooler finish, we can use “contradiction”, which proves anything you like from two contradictory assmptions. Here is the proof using the contradiction tactic.

I need to say one more important thing. Clearly every proposition is either true or false, so in other words we should be able to prove this:

variable P : Prop

example : P ∨ ¬ P :=
begin
admit
end

How do we do this? Well, we can’t 😀 Computer scientists have a name for this basic fact — it’s apparently called “the law of the excluded middle”. Amazingly, this basic fact is not built into Lean by default, as apparently some computer scientists try and do mathematics without assuming it. We are mathematicians, so we will assume it. We can (and definitely should!) add it in as an axiom in fact.

axiom em (X : Prop) : X ∨ ¬ X -- no proof required, it's an axiom.

variable P : Prop

example : P ∨ ¬ P :=
begin
exact em P
end

This works.

Without assuming this as an axiom, “P or not P” is actually an unprovable statement for a general proposition P, in Lean. This just reflects the fact that Lean is designed for computer scientists as well as mathematicians. In fact more generally there is a “maths library” for Lean, called mathlib, which is not loaded into Lean by default, but which we as mathematicians will definitely need. I do not know how to load this library into the online version of Lean but I do know how to install it on a computer.

Questions 2 to 4 on M1F example sheet 1 might need to assume the law of the excluded middle. In fact, worrying about whether something assumes the Law of the Excluded Middle or not is not really a question for mathematicians, we just assume it.

Advertisements

About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.
This entry was posted in Learning Lean. Bookmark the permalink.

2 Responses to More easy Lean proofs [difficulty : quite easy]

  1. I used to believe in the law of the excluded middle, as well (on much the same basis — conforming to my group identity as a classical mathematician), but spending time with Lean I’ve changed my mind.

    I really like the interpretation of “implication” as a piece of machinery: claiming that P => Q is claiming that I have a _machine_ that takes as input a proof of the statement P, and produces as output a proof of the statement Q. Now the statement (not P) should be interpreted as a machine that takes a proof of P, and produces something that we all agree can’t possibly exist (“false”). Then the statement (not (not P)) is a machine, that takes as input a machine (turning proofs of P into absurdities), and produces an absurdity.

    It’s easy to construct a (not (not P)) machine from a proof of P: just take the machine for (not P) provided as input, and insert into it your given proof of P.

    On the other hand, you’re just not going to ever go in the other direction.

    It’s also surprisingly interesting how much of mathematics you can still “salvage” when you drop LEM, by tweaking definitions in mostly harmless ways. (I’m not expert here, just amused by the examples I’ve seen.)

    (I suspect you know all this, and are just dismissing Lean’s hesitancy about LEM to reassure everyone; I just wanted to mention this “machinery” explanation, as I think many mathematicians have not heard it.)

    Like

    • xenaproject says:

      Hi Scott. I completely understand this point of view; I haven’t explained it on the blog because my target audience is undergraduates, and the concept of the failure of excluded middle is a point of view which we do not even mention in the undergraduate curriculum here. In some sense my concern is that if mathematics undergraduates start wrestling with a world where LEM is false, then they might start getting confused about things which are simply not relevant to what we are trying to teach them. The last thing I want to do is to confuse them. We will be assuming the Law of the Excluded Middle throughout my course and example sheets. I do agree that the fact that the Feit-Thompson theorem has been proved without it is some quite substantial evidence that it may well not be necessary in things like the courses on finite groups and their representations. However my current understanding is that there are problems with even basic analysis like the Intermediate Value Theorem, and at this point in an undergraduate’s education all the “fixes” I have heard for these problems are not satisfactory to me as a mathematics educator. So LEM is staying, and any undergraduate who is curious about what happens when you drop it can just find out for themselves when they’re older (like we did!)

      In my undergraduate course I will simply be telling the students that there is a Platonic universe, and every proposition is either true or false. Not because I believe this is the best way to do mathematics, but because I believe that it is the best way to teach it to the audience which it is my job to teach. Note that this audience contains plenty of people who are forced to come as part of their degree, and whose interests might be far more towards what one might call the “applicable” or “applied” side of things.

      Like

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

w

Connecting to %s