11 - Existence

The aim of an existence proof is simply to show something exists. 

Task

Show there exists a natural number n, such that

$$n^2+1=10$$

You may see this written in mathematical notation, where the symbol \exists  means “there exists”.

$$\mathrm{\exists }n\in \mathbb{N}[n^2+1=10]$$

The essence of an existence proof is to demonstrate an object exists that satisfies any given conditions. Calculating, deriving, or even guessing, what that object is, is not the central point.

Maths

For our task, intuition tells us that $n$ can't be larger than $10$, and after some mental trial and error we find that $n=3$ works. We have found our example.

We don't need to justify how we arrived at our example. We only need to show it satisfies the condition $n^2+1=10$.

Let's write a proof, making clear each step. 

$$\begin{array}{rlrl}\mathrm{\exists }n\in \mathbb{N}& [n^2+1=10]& & \text{proof objective}\\ & & & \\ \text{(1)}& \text{use }n=3& & & \text{chosen example}{n}^2+1& =(3{)}^2+1& & \text{using }(\text{1})\\ ◻& & =10& & \text{by arithmetic }\end{array}$$

We first state the proof objective, which includes the condition $n^2+1=10$ any example must meet.

We then choose $n=3$, and show by arithmetic that indeed $n^2+1=10$. 

Code

The following Lean program proves there exists a natural number $n$ such that $n^2+1=10$.

-- 11 - Existence proof

import Mathlib.Tactic

example : ∃ n: ℕ, n^2 + 1 = 10 := by
  use 3
  calc
    3^2 + 1 = 10 := by norm_num

The proof header is a little different from the ones we've looked at recently. Here, there is no separate definition of variable types, and no hypothesis. The entire theorem is in the proof objective. 

The proof objective ∃ n: ℕ, n^2 + 1 = 10 says that there exists a natural number n, such that n^2 + 1 = 10.

The next step is to choose an example that meets this condition. The instruction use 3 tells Lean that we propose 3 as that example.

The Infoview will confirm that use 3 changes the proof goal from ∃ n, n^2 + 1 = 10 to 3^2 + 1 = 10.

We can use a simple calc section to show by arithmetic that 3^2 + 1 is indeed 10, completing the proof. 

Bad Example

Let's see what happens if we choose a bad example, say $n=4$. This means changing the code to use 4.

Placing the cursor after use 4 shows the proof goal.

⊢ 4 ^ 2 + 1 = 10

This goal is impossible to prove, because $17$ is not $10$.

Simpler Code

The following is a shorter version of our Lean program.

-- 11 - Existence proof

import Mathlib.Tactic

example : ∃ n: ℕ, n^2 + 1 = 10 := by
  use 3
  norm_num

The goal at the point of the previous calc section was ⊢ 3^2 + 1 = 10. This is simple enough to apply the norm_num tactic to prove. It doesn't really need a calc section, which is better suited to derivations that require several steps.

As with all code, it is better to be clear and unambiguous than overly concise. This use of one-line tactics should only be done when the context is simple and clear for anyone reading your code - including your future self.

---

Easy Exercise

Write a Lean program to prove there exists a natural number greater than $5$.

In mathematical notation, the proof objective is as follows, and should translate into Lean code fairly directly.

$$\mathrm{\exists }n\in \mathbb{N}[n>5]$$

As an optional extra challenge, try writing the proof in the concise form shown above.

10 - "And" Goal

Here we look at a proof goal that is a conjunction.

Task

For integer $x$, given that $x=-1$, show that

$$(x^2=1)\wedge (x^3=-1)$$

Maths

Recall that $P\wedge Q$ being true means both $P$ and $Q$ must be true. 

That means we have to prove both $x^2=1$ and $x^3=-1$ are true, given the hypothesis $x=-1$. 

Let's write a step by step proof.

$$\begin{array}{rlrl}\text{(1)}& x& =-1& & \text{given fact}(x^2=1)& \wedge (x^3=-1)& & \text{proof objective }\\ & & & \\ x^2& =(-1{)}^2& & \text{using fact }(\text{1})\\ \text{(2)}& & =1& & \text{using arithmetic }& & & \\ x^3& =(-1{)}^3& & \text{using fact }(\text{1})\\ \text{(3)}& & =-1& & \text{using arithmetic }& & & \\ ◻& (x^2=1)& \wedge (x^3=-1)& & \text{using results }(\text{2},\text{3})\end{array}$$

We have shown both $x^2=1$ and $x^3=-1$, and so the proof goal $(x^2=1)\wedge (x^3=-1)$ is true.

Code

The following Lean program proves $(x^2=1)\vee (x^3=1)$ follows from $x=-1$.

-- 10 - Conjunctive "and" Goal

import Mathlib.Tactic

example {x : ℤ} (h : x = -1) : x^2 = 1 ∧ x^3 = -1 := by
  constructor
  · calc
      x^2 = (-1)^2 := by rw [h]
      _ = 1 := by norm_num
  · calc
      x^3 = (-1)^3 := by rw [h]
      _ = -1 := by norm_num

As is very familiar now, the proof header declares the variable types, establishes the hypothesis, and defines the overall proof objective. The objective here is a conjunction, and uses the symbol ∧ to denote “logical and”. 

The next step is to split the two parts of the conjunctive proof goal into two separate goals, each to be proven one after another. The instruction constructor does precisely this.

The Infoview will confirm that constructor replaces the single goal x^2 = 1 ∧ x^3 = 1 with two new goals, x^2 = 1 and x^3 = -1.

The rest of the proof has two calc structures, one after the other, to show x^2 = 1 and x^3 = -1. Focussing dots are used to make clear there are two sub-proofs to support the overall proof.

Infoview

Placing the cursor before the constructor instruction shows the original proof goal.

x : ℤ
h : x = -1
⊢ x ^ 2 = 1 ∧ x ^ 3 = -1

Placing the cursor on the next line after constructor confirms the proof goal has been replaced by two smaller goals.

x : ℤ
h : x = -1
⊢ x ^ 2 = 1

x : ℤ
h : x = -1
⊢ x ^ 3 = -1

This is another example of manipulating the proof goal into a form that is easier to prove.

---

Easy Exercise

A longer conjunction could be $P\wedge Q\wedge R\wedge S$. The instruction constructor splits this into two goals, $P$ and $Q\wedge R\wedge S$.

For integer $x$, given that $x=-1$, write a Lean program to show that 

$$(x^3=-1)\wedge (x^4=1)\wedge (x^5=-1)$$

The proof will require two uses of constructor.

09 - "Or" Goal

We've seen that a hypothesis can be a disjunction or a conjunction. 

Here we look at a slightly more interesting scenario, a proof goal that is a disjunction.

Task

For integer $x$, given that $x=-1$, show that 

$$(x^2=1)\vee (x^3=1)$$

Maths

Our initial reaction might be concern at seeing $x^3=1$. Clearly $(-1{)}^3=1$ is not true. 

Remember that $P\vee Q$ being true means at least one of $P$ and $Q$ is true. If $Q$ is false, but $P$ is true, then the disjunction $P\vee Q$ is still true.

Given the hypothesis $x=-1$, if we can prove $x^2=1$ is true, then we'll have proven the disjunction $(x^2=1)\vee (x^3=1)$ is also true.

Let's write a step by step proof.

$$\begin{array}{rlrl}\text{(1)}& x& =-1& & \text{given fact}\text{(2)}& (x^2=1)& \vee (x^3=1)& & \text{proof objective }& & & \\ \text{(3)}& x^2& =1& & \text{sufficient goal }(\text{2})& & & \\ x^2& =(-1{)}^2& & \text{using fact }(\text{1})\\ & =1& & \text{using arithmetic }\\ & & & \\ ◻& (x=-1)& ⟹(x^2=1)\vee (x^3=1)& & \end{array}$$

Once we state that it is sufficient to prove $(x^2=1)$ in order to prove $(x^2=1)\vee (x^3=1)$, the rest of the proof continues in the familiar way we've seen before.

Choice

If the proof objective were $(x^2=1)\vee (x^3=-1)$, then both statements $x^2=1$ and $x^3=-1$ can be proven to be true. 

We can choose which one of the two statements we want to prove. We don't need to prove both, because proving one is sufficient for a disjunction.

Code

The following Lean program proves $(x^2=1)\vee (x^3=1)$ follows from $x=-1$.

-- 09 - Disjunctive "or" Goal

import Mathlib.Tactic

example {x : ℤ} (h : x = -1) : x^2 = 1 ∨ x^3 = 1 := by
  left
  calc
    x^2 = (-1)^2 := by rw [h]
    _ = 1 := by norm_num

As usual, the proof header declares the variable types, establishes the hypothesis, and defines the overall proof objective. The objective here is a disjunction, and uses the symbol $\vee$  to denote “logical or”. 

We state our intention to prove only the “left” part of the disjunction. The instruction left does precisely this. 

The Infoview will confirm that left replaces the goal x^2 = 1 ∨ x^3 = 1 with x^2 = 1.

The rest of the proof uses the familiar calc structure to show x^2 = 1. This matches the new proof goal, and because it is sufficient, the original goal x^2 = 1 ∨ x^3 = 1 is also proven.

Infoview

Placing the cursor before the left instruction shows the original proof goal.

x : ℤ
h : x = -1
⊢ x ^ 2 = 1 ∨ x ^ 3 = 1

Placing the cursor on the next line after left confirms the proof goal has been replaced by a smaller, but sufficient, goal.

x : ℤ
h : x = -1
⊢ x ^ 2 = 1

This manipulation of the proof goal might appear to be a hack, something to be discouraged. In fact, it is quite common, and considered quite normal.

---

Easy Exercise

A longer disjunction could be $P\vee Q\vee R\vee S$. The instruction left selects the left-most statement $P$ as the new goal. The instruction right selects the remainder $Q\vee R\vee S$ as the new goal. 

For integer $x$, given that $x=-1$, write a Lean program to show that 

$$(x=1)\vee (x^2=1)\vee (x^3=1)$$

Both the right and left instructions will be needed to write the proof.

08 - "And' Hypothesis

The previous task started with an “or” hypothesis. Here we'll look start with anl “and” hypothesis. 

Task

For integers $x$ and $y$, where the following is true

$$(x=5)\wedge (y=x+3)$$

show that

$$y=8$$

The symbol $\wedge$  means “logical and”. The statement $P\wedge Q$ means both $P$ and $Q$ are true. Statements of the form $P\wedge Q$ are called conjunctions.

Maths

Once we realise a hypothesis of the form $P\wedge Q$ is the same as hypotheses $P$ and $Q$ both being true, the proof proceeds just like our earlier examples with two hypotheses.

In this sense, conjunctive hypotheses are not particularly interesting, but we do need to learn how to handle them.

Let's write a proof, making clear each step.

$$\begin{array}{rlrl}\text{(1)}& (x=5)& \wedge (y=x+3)& & \text{given fact}& & & \\ \text{(2)}& x& =5& & \text{derived fact }(\text{1})\text{(3)}& y& =x+3& & \text{derived fact }(\text{1})& & & \\ y& =x+3& & \text{using fact }(\text{3})\\ & =(5)+3& & \text{using fact }(\text{2})\\ ◻& & =8& & \text{using arithmetic}\end{array}$$

From the single conjunctive hypothesis $(x=5)\wedge (y=x+3)$ we derive two smaller hypotheses, $x=5$ and $y=x+3$, both of which are true.

We start with $y=x+3$ from derived fact (3), and then use $x=5$ from derived fact (2) to finally conclude $y=8$.

Code

The following Lean program proves $y=8$ follows from $(x=5)\wedge (y=x+3)$.

-- 08 - Conjunctive "and" Hypothesis

import Mathlib.Tactic

example {x y : ℤ} (h : x = 5 ∧ y = x + 3) : y = 8 := by
  obtain ⟨ ha , hb ⟩ := h
  calc
    y = x + 3 := by rw [hb]
    _ = (5) + 3 := by rw [ha]
    _ = 8 := by norm_num

As usual, the proof header declares the variable types, establishes the hypothesis, and defines the overall proof goal. The hypothesis is a conjunction, and uses the symbol ∧ to denote “logical and”. 

The next step is to replace the conjunctive hypothesis with two smaller hypotheses. The instruction obtain ⟨ ha, hb ⟩ := h does this. It splits the conjunctive hypothesis h into ha and hb, and then removes h.

Notice the comma and angle brackets ⟨⟩ used to split a conjunction, unlike the vertical bar | and no brackets used to split a disjunction.

The rest of the proof uses the familiar calc structure to show y = 8. 

Infoview

Placing the cursor before the obtain instruction shows there is only one hypothesis g.

x y : ℤ
h : x = 5 ∧ y = x + 3
⊢ y = 8

Placing the cursor on the next line after obtain, confirms h has been replaced by ha and hb.

x y : ℤ
ha : x = 5
hb : y = x + 3
⊢ y = 8

Notice the hypothesis h has been entirely removed.

---

Easy Exercise

Write a Lean program to show that $y\ge 8$, given the conjunctive hypothesis

$$(x\ge 5)\wedge (y=x+3)$$

where $x$ and $y$ are integers.

07 - Proof By Cases

A proof by cases divides a task into separate cases, and proves each one leads to the desired conclusion. 

Task

Given the following fact about a real number $x$,

$$(x=3)\vee (x=-3)$$

our task is to show

$$x^2=9$$

The symbol $\vee$  means “logical or”. The statement $P\vee Q$ means either $P$ is true, or $Q$ is true, or possibly even both are true. 

Statements of the form $P\vee Q$ are called disjunctions.

Maths

Our aim is to show $x^2=9$ follows from the hypothesis $(x=3)\vee (x=-3)$. 

This hypothesis tells us that either $x=3$ is true, or $x=-3$ is true. We don't know which, so we have to consider both cases, and show the conclusion follows from each case.

The following illustrates this.

Let's write a proof by cases, making clear each step.

$$\begin{array}{rlrl}\text{(1)}& (x=3)& \vee (x=-3)& & \text{given fact}& & & \\ \text{(2)}& \text{case }x=3& & & \text{using fact }(\text{1})x^2& =(3{)}^2& & \text{using case }(\text{2})\\ & =9& & \\ & & & \\ \text{(3)}& \text{case }x=-3& & & \text{using fact }(\text{1})x^2& =(-3{)}^2& & \text{using case }(\text{3})\\ & =9& & \\ & & & \\ ◻& (x=3)\vee (x=-3)& ⟹x^2=9& & \end{array}$$

The given fact (1) splits into two cases, $x=3$ and $x=-3$. 

• The first case (2) is $x=3$. We want to prove something about $x^2$. This case gives us $x^2=(3{)}^2$, leading to the conclusion $x^2=9$.
• The second case (3) is $x=-3$. This gives us $x^2=(-3{)}^2$, also leading to the conclusion $x^2=9$.

The two possibilities $x=3$ and $x=-3$ are sufficient to fully cover the hypothesis $(x=3)\vee (x=-3)$. There is no third possibility. 

We have shown that, given the hypothesis, $x^2$ is indeed always $9$.

Code

The following Lean program proves $x^2=9$ follows from $(x=3)\vee (x=-3)$.

-- 07 - Proof by Cases

import Mathlib.Tactic

example {x : ℤ} (h : x = 3 v x = -3) : x^2 = 9 := by
  obtain ha | hb := h
  · calc
    x^2 = (3)^2 := by rw [ha]
    _ = 9 := by norm_num
  · calc
    x^2 = (-3)^2 := by rw [hb]
    _ = 9 := by norm_num

The proof header is no different to the ones we've seen before, setting out the variable type, the hypothesis, and the proof objective. The hypothesis is a disjunction, and uses the letter v to denote “logical or”. 

The next line is new. The obtain ha | hb := h splits the disjunction hypothesis h into ha and hb. These new hypotheses correspond to the two cases.

The Infoview will show that ha : x = 3 and hb : x = -3. 

We now need to show that each case, with ha and hb as hypotheses, leads to the desired conclusion . The two calc sections, one after the other, do exactly this.

In the first calc section, we start with x^2 because that is what we want to prove something about. We use the newly created hypothesis ha : x = 3 to justify x^2 = (3)^2, and then show this is 9 by simple arithmetic.

The second calc section is almost exactly the same, but uses the hypothesis for second case hb : x = -3.

Notice the calc sections have a dot preceding them, · calc. This focussing dot is considered good style when writing sub-proofs within a larger proof. They help us see, at a glance, the structure of the proof. In additional, the Infoview restricts information to the current goal. You can enter the focussing dot by typing \. and your Lean-enabled editor should turn it into a focussing dot.

Infoview

Placing the cursor before obtain shows only one goal, the overall proof goal.

1 goal
x : ℤ
h : x = 3 v x = -3
⊢ x ^ 2 = 9

Moving the cursor after the obtain instruction, just before the first · calc, shows the two sub-goals and their respective hypotheses ha and hb.

2 goals
case inl
x : ℤ
ha : x = 3
⊢ x ^ 2 = 9

case inr
x : ℤ
hb : x = -3
⊢ x ^ 2 = 9

Moving the cursor past the focussing dot, placing it just before calc, shows only the hypothesis relevant to the first case.

1 goal
case inl
x : ℤ
ha : x = 3
⊢ x ^ 2 = 9

---

Easy Exercise

Write a Lean program to prove $x^2-3x+2=0$, given

$$(x=1)\vee (x=2)$$

where $x$ is a real number. 

In your proof create two cases $x=1$ and $x=2$ from the given hypothesis $(x=1)\vee (x=2)$.