MATH300 in Lean 4

Chapter 3: Writing Proofs

Finally! We are going to write some proofs. In the following two chapters, we will use the tactics we learned from the first two chapters to write the lean code version of the proofs from the textbook. Another way of saying that is to formalize the theorems from the textbook, which sounds pretty cool!

Calculational Proofs

Before we dive into those different proof techniques, let's first take a look at the kind of proofs we've dealt with over the past 10 years: calculational proofs. Maybe we can get some inspirations from that.

-- 3.0.01 (complicated way) Prove that (x + y) * (x + y) = x * x + (x * y + y * x) + y * y
example {x y : ℝ} : (x + y) * (x + y) = x * x + (x * y + y * x) + y * y := by
  calc
    _ = (x + y) * x + (x + y) * y := by exact mul_add (x + y) x y  -- 5. The Distributive Law
    _ = x * (x + y) + y * (x + y):= by rw [mul_comm (x + y) x, mul_comm (x + y) y]  -- 3. Commutativity
    _ = x * x + x * y + (y * x + y * y) := by rw [mul_add x x y, mul_add y x y]  -- 5. The Distributive Law
    _ = x * x + (x * y + (y * x + y * y)) := by rw [add_assoc (x * x) (x * y) (y * x + y * y)]  -- 4. Associativity
    _ = x * x + ((x * y + y * x) + y * y) := by rw [← add_assoc (x * y) (y * x) (y * y)]  -- 4. Associativity
    _ = x * x + (x * y + y * x) + y * y := by rw [← add_assoc (x * x) (x * y + y * x) (y * y)]  -- 4. Associativity

If you want to prove an equality, you can use the calc keyword, and then follow this structure to do the calculation step by step. Note that for each step you need to show the tactics you use to make such progress (after := by). These commands can be found in first chapter's EPIs table.

Well, it looks really complicated, right? Here is a simple version:

-- 3.0.01 (simple way) Prove that (x + y) * (x + y) = x * x + (x * y + y * x) + y * y
example {x y : ℝ} : (x + y) * (x + y) = x * x + (x * y + y * x) + y * y := by
  ring

Yes, just type ring, and the goal will be closed. It applies all the basic properties of integers we use in the calc version implicitly. You don't need to do the algebra by yourself anymore.

So why did I show you the complicated way? Well, first of all, calc is just a command you'd better know as a Lean user. And most importantly, the calculational proof shows that in order to prove something, it is common to make progress step by step, which therefore leads to the discussion about "direct proofs".

3.1. Direct Proofs

Theorem 3.1. If a and b are even integers, then a + b is even.

The textbook gives a clear proof of this theorem. Let's see how we code a "Lean version" of this proof.

-- theorem 3.1. If a and b are even integers, then a + b is even.
theorem c3_1 {a b : ℤ} (h1 : Even a) (h2 : Even b) : Even (a + b) := by
  cases' h1 with k1 h1
  cases' h2 with k2 h2
  use k1 + k2
  rw [h1, h2]
  ring

If you find it hard to understand the proof, try thinking about the definition of "even" as logical expression. That is, think about "even a" as "∃ k1 : ℤ, a = k1 + k1". Which tactic should you use to pull out something from a statement with existential quantifier? What about the goal?

Theorem 3.2. Suppose a, b, and c are integers. If a|b and b|c, then a|c.

-- theorem 3.2. Suppose a, b, and c are integers. If a|b and b|c, then a|c.
theorem c3_2 {a b c : ℤ} (h1 : a ∣ b) (h2 : b ∣ c) : a ∣ c := by
  cases' h1 with k h1
  cases' h2 with l h2
  use k * l
  rw [h2, h1]
  ring

That's it! We've successfully formalized two theorems from the textbook. Note that we use the "theorem" command here, instead of the "example" command we used before. The statement with "theorem" command can be used later. Remember the EPI's table? All the commands we gave you are theorems from the Mathlib!

So...How to use a theorem?

A theorem typically looks like this:

theorem_name {a b c ... : Type} (h : prop) ... : content := ...

Seems a little bit abstract. Let's see some real examples. To EPI 3 - commutativity, the theorem is called add_comm in Mathlib. If you find that theorem in Mathlib, or if you move your cursor over the theorem in VS Code, it should look like this:

add_comm.{u_1} {G : Type u_1} [inst✝ : AddCommSemigroup G] (a b : G) : a + b = b + a

Well, after the theorem name add_comm, you don't need to worry about anything in curly braces { } and square brackets [ ]. Those are called "implicit arguments", which Lean can infer by itself. You only need to start from things with parentheses ( ). Here, before the colon :, we see that (a b : G). "G" refers to "Group", which you will learn in MATH 402 if you take that, but we don't need to worry about that for now. Just remember that the set of integers is a group under addition. Only for this class, anytime you see G, you can just think of it as ℤ. Therefore, given two integers as arguments to the theorem add_comm a b, it will return everything after the colon :. In this case, add_comm a b gives us a + b = b + a, a statement we can use by rw or exact tactic.

Another example is the theorem we proved above. Move your cursor over the theorem name, you can see that:

c3_1 {a b : ℤ} (h1 : Even a) (h2 : Even b) : Even (a + b)

Start from the parentheses: there are two hypotheses enclosed by hypotheses. Therefore, we need to give two propositions as arguments to the theorem, where the two propositions both indicate that an integer is even. In our proof, if we have two propositions (h1 : Even a) (h2 : Even b), we can then use this command:

c3_1 h1 h2

which returns the things after the colon : Even (a + b), which is a statement we can use.

Last important reminder: remember the conditional statements from chapter 2? If we have P → Q, we can call P the "assumption" and Q the "conclusion". Well, we saw many examples that assumptions are in the parentheses before the colon for each theorem. And in fact: (h : P) : Q and P → Q are internally the same in Lean! Therefore, to use a theorem like th{...} : P → Q, if we type th P, it will return Q, which is exactly the same as how th{...} (h : P): Q works! If we have a biconditional statement like th{...} : P ↔ Q, the command th.1 stands for P → Q, and th.2 stands for Q → P, so th.1 P will return Q.

In short, if you want to use a theorem, just give it everything specified in the parentheses in order, and then it will return the statement after the colon for you to use. We will do some practice in the next section. You may find the EPIs table from chapter 1 to be helpful!

3.1.1. Structure your proof in Lean

Let's continue our discussion about the "step-by-step" proof from the beginning of this chapter. The two examples above are relatively simple and don't require much reasoning. Oftentimes, however, a proof consists of many intermediate steps. We all want lives to be easy, so if our goal is (P → Q), we always want to check if there exists a theorem that is exactly the same as our goal, and then use our lovely exact tactic to close the goal directly. Unfortunately, for most of the time we need to show an entire logic chain in order to prove something. For example, to prove that (P → Q), we need to show that (P → R → S → T → U → V → W → ... → Q). If you find this to be frustrating, then ...... welcome to Mathematics.

Let's take a simple example to see why this "logic chain" works.

-- 3.1.01 If P → R, and R → Q, then P → Q.
example {P Q R : Prop} (h1 : P → R) (h2 : R → Q) : P → Q := by
  intro h
  apply h2
  apply h1
  exact h

Using the tactics we learned before, we proved that "If P → R, and R → Q, then P → Q." In fact, as you follow this pattern, you can have as many intermediate propositions as you want. As long as the logic chain begins with P and ends with Q, you can always show that (P → Q). Therefore, we've proved that "a chain of implications" does work. And most importantly, we are now able to use Lean to prove something that's not proved in the textbook! That's amazing!!

Let's see a real example of it. Consider this statement: If a and b are even integers, then 2 | a + b. De ja vu? It's actually equivelent to theorem 3.1. - "if a and b are even, then a + b is even." (a + b is even ≡ ∃ k, a + b = 2k ≡ 2 | a + b). In fact, 2 divides any even integer! Therefore, we can first use the result from theorem 3.1. to show that if a and b are both even, then a + b is even, and then unfold the definition of even number and divisibility of prove that 2 | a + b, which means: in order to prove (Even a ∧ Even b → 2 | a + b), we can add an intermediate step: (Even a ∧ Even b → Even (a + b) → 2 | a + b).

So how can we construct the intermediate steps of a proof in Lean? For most of the time, we want to prove (P → Q), but we don't have the hypotheses like (h1 : P → R) and (h2 : R → Q) that are explicitly written in the problem, so we need to have our own hypotheses as the intermediate steps by using the have tactic.

-- 3.1.04 If a and b are even integers, then 2 ∣ a + b
example {a b : ℤ} (h1 : Even a) (h2 : Even b) : 2 ∣ a + b := by
  have h3 : Even (a + b) := by
    exact c3_1 h1 h2
  cases' h3 with k h4
  use k
  rw [h4]
  ring

Remember: our first step is to prove that a + b is an even integer. To add this intermediate step, we use the have tactic, and give this step a name. Since it will become the third hypothesis of this statement, we name it h3 here. After the colon we state the content of this step: Even (a + b). Finally, we type := by to indicate that we are going to prove it. As you hit "enter" + "tab", you will see that in the "current proof state" in your Lean Infoview window, the goal becomes the statement we are proving in this step. This is a subgoal of our whole proof. We use indentation to indicate that we are proving a subgoal, and Lean's current proof state will only show the subgoal to help us focus on it. In this case, since the subgoal is already proved in this Lean file, we can use the theorem directly by the exact tactic. We named this theorem "c3_1" above, which takes two hypotheses (h1 : Even a) (h2 : Even b) and outputs the result Even (a + b). (We've seen how to use a theorem.) In this case, "c3_1" needs to take two arguments that are the hypotheses to show that a and b are even, so we type c3_1 h1 h2, and it will return the output (Even (a + b)). Since it's exactly the same as this subgoal, we use exact tactic. After we complete the proof of a subgoal, we exit this indentation block, and Lean will show us the main goal again. Then you can use this new hypothesis and some tactics to close this main goal as usual.

3.2. Proof by Cases (a.k.a. proof by exhaustion)

From last chapter, we've shown that in order to prove things like ((P ∨ Q) → R), we need to prove that (P → R) ∧ (Q → R). You can draw a truth table to show that these two statements are actually logically equivalent, but we have three variables here, so our truth table has 2^3 = 8 rows, and it becomes very tedious to draw a truth table for it. Let's see if we can apply some properties of logic to prove this equivelance.

• Law of Implication: P → Q ≡ ¬P ∨ Q
• De Morgan's Laws (1): ¬(P ∧ Q) ≡ ¬P ∨ ¬Q
• De Morgan's Laws (2): ¬(P ∨ Q) ≡ ¬P ∧ ¬Q
• Distributive Laws (1): P ∧ (Q ∨ R) ≡ (P ∧ Q) ∨ (P ∧ R)
• Distributive Laws (2): P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R)

We've seen the first three properties from the last chapter. You might be unfamiliar with the last two properties, but it's not difficult to memorize them: they are very similar to the distrubutive law in arithmetic.

Applying these properties, we have:

(P ∨ Q) → R ≡ ¬(P ∨ Q) ∨ R ≡ (¬P ∧ ¬Q) ∨ R ≡ (¬P ∨ R) ∧ (¬Q ∨ R) ≡ (P → R) ∧ (Q → R).

We've proved the underlying logic of proof by cases!

Theorem 3.3. The product of two consecutive integers is even.

The textbook first states the fact that an integer is either even or odd. Well, we can't just do the same thing in Lean: we need to prove it or use the theorem that's proved somewhere else. We will prove its contrapositive later in this chapter, but for now let's use the theorem from Mathlib. You might have already seen that we imported "Mathlib.Data.Int.Parity" at the beginning of the file. It has the following theorem we will use:

Int.even_or_odd (n : ℤ) : Even n ∨ Odd n

It states that an integer is even or odd. If we type Int.even_or_odd n, where n is an integer declared ealier, it will output Even n ∨ Odd n. This is all we need!

-- 3.2.01 (Theorem 3.3.) The product of two consecutive integers is even.
theorem c3_3 (n : ℤ) : Even (n * (n + 1)) := by
  have h : Even n ∨ Odd n := by
    exact Int.even_or_odd n
  cases' h with heven hodd
  · cases' heven with k heven
    use k * (n + 1)
    rw [heven]
    ring
  · cases' hodd with k hodd
    use n * (k + 1)
    rw [hodd]
    ring

Theorem 3.4. (Elementary Properties of Absolute Value). Suppose a and b are integers. Then:

• (a) |a| ≥ 0.
• (b) |−a| = |a|.
• (c) −|a| ≤ a ≤ |a|.
• (d) |a|^2 = a^2.
• (e) |ab| = |a||b|.
• (f) |a| ≤ |b| if and only if −|b| ≤ a ≤ |b|.

If you look at the proofs in the textbook, you should notice that they all assume that an integer is either "greater than or equal to 0" or "less than 0". We will use a theorem from Mathlib to achieve that:

lt_or_le.{u} {α : Type u} [inst✝ : LinearOrder α] (a b : α) : a < b ∨ b ≤ a

Again, just look at things in the parentheses: (a b : α). Before chapter 5, please take my words: I will always give you the right theorem, so don't worry about what α means here (just think of "α" as "ℤ"). Therefore, if we let b be 0, then the command lt_or_le a 0 will return a < 0 ∨ a ≥ 0, which is all we need for the following proofs! In chapter 5, I will explain more about what {α : Type u} means here. By that time, you should be able to understand any theorem and later look for theorems by yourself. Let's take time :)

To prove these theorems, let me introduce two new powerful tactics for you.

3.2.01 rcases

To prove (b), we will need three cases: a < 0 ∨ a = 0 ∨ 0 < a. You might want to use cases' tactic, but here is an upset fact: cases' can only seperate a statement to two statements. In this case, it is only able to split the output to a < 0 and a = 0 ∨ a > 0, as Lean pull out statements from logical connectives in order. Frustratingly, you need to use cases' again to split the second statement to two statements.

Is there one way to seperate the cases all at once? There is! We can do this recursively by rcases command. "r" stands for "recursive".

If the hypothesis is h : P ∨ Q ∨ R, type rcases h with hp | hq | hr to seperate the hypothesis to hp: P, hq: Q, and hr: R. If the hypothesis is h : P ∧ Q ∧ R, type rcases h with ⟨hp hq hr⟩ to seperate the hypothesis to hp: P, hq: Q, and hr: R. In short, | for disjunctions, and ⟨⟩ for conjunctions. In VS Code, type "\<" for "⟨" and "\>" for "⟩". This tactic is a recursive version of cases', so it can do everything that cases' can do. Feel free to stick to it.

3.2.02 linarith

The proof in the textbook use the fact that if a < 0, then -a > 0. This is an example of linear inequality. For any goal as linear equalities and linear inequalities, with enough information provided in the assumptions, you can use the linarith tactic. For example, if the assumptions are (h1 : a < b) and (h2 : b < c) and your goal is a < c, just type linarith. It will close the goal immediately. Keep in mind that the expression should be linear, which means the variables are linearly combined. It's a powerful tactic, but don't use it everywhere blindly.

Also, some axioms about absolute value and integers for you (I omit some unimportant information). Note that you've seen the fifth command at EPI - 8. If you type lt_trichotomy a 0, you will get a < 0 ∨ a = 0 ∨ a > 0 .

abs_of_neg ... (h : a < 0) : |a| = -a
abs_of_nonneg ... (h : 0 ≤ a) : |a| = a
abs_of_pos ... (h : 0 < a) : |a| = a
abs_of_nonpos ... (h : a ≤ 0) : |a| = -a
lt_trichotomy ... (a b : α) : a < b ∨ a = b ∨ b < a

-- 3.2.02 |a| ≥ 0.
theorem c3_4_a {a : ℤ} : |a| ≥ 0 := by
  have h : a < 0 ∨ a ≥ 0 := by
    exact lt_or_le a 0
  cases' h with h1 h2
  · rw [abs_of_neg h1]
    linarith
  · rw [abs_of_nonneg h2]
    exact h2

-- 3.2.03. |-a| = |a|
theorem c3_4_b {a : ℤ} : |-a| = |a| := by
  have h : a < 0 ∨ a = 0 ∨ a > 0 := by
    exact lt_trichotomy a 0
  rcases h with h1 | h2 | h3
    · have h : -a > 0 := by
        linarith
      rw [abs_of_pos h, abs_of_neg h1]
    · rw [h2]
      norm_num
    · have h : -a < 0 := by
        linarith
      rw [abs_of_neg h, abs_of_pos h3]
      ring

The textbook leaves (c) to (f) as exercises to you. However, the proof of next theorem (the Triangle Inequality) needs results from (c) to (f), so I will formalize all of them for you. You are welcome :)

Though you might just skim through the next 4 proofs in order to continue reading this chapter since some of them are REALLY long, I highly encourage you to check these proofs in details later for practice. All the Mathlib theorems used here are given either in this chapter or in EPIs table from chapter 1. You can always move your cursor over the theorems in VS Code to check their definitions since you already know how to read them!

-- 3.2.04. -|a| ≤ a ≤ |a|
theorem c3_4_c {a : ℤ} : -|a| ≤ a ∧ a ≤ |a| := by
  have h : a < 0 ∨ a ≥ 0 := by
    exact lt_or_le a 0
  cases' h with h1 h2
  · constructor
    · rw [abs_of_neg h1]
    linarith
    · rw [abs_of_neg h1]
    linarith
  · constructor
    · rw [abs_of_nonneg h2]
    linarith
    · rw [abs_of_nonneg h2]  

-- 3.2.05 |a|² = a²
theorem c3_4_d {a : ℤ} : |a|^2 = a^2 := by
  have h : a < 0 ∨ a ≥ 0 := by
    exact lt_or_le a 0
  cases' h with h1 h2
  · rw [abs_of_neg h1]
    ring
  · rw [abs_of_nonneg h2] 

-- 3.2.06 |ab| = |a||b|
theorem c3_4_e {a b : ℤ} : |a * b| = |a| * |b| := by
  have ha : a < 0 ∨ a = 0 ∨ a > 0 := by
    exact lt_trichotomy a 0
  rcases ha with ha1 | ha2 | ha3
  · have hb : b < 0 ∨ b = 0 ∨ b > 0 := by
      exact lt_trichotomy b 0
    rcases hb with hb1 | hb2 | hb3
    · have htemp : b * a > 0 * a:= by
        exact mul_lt_mul_of_neg_right hb1 ha1
      have hab : a * b > 0 := by
        linarith
      rw [abs_of_pos hab, abs_of_neg ha1, abs_of_neg hb1]
      ring
    · rw [hb2]
      norm_num
    · have htemp : b * a < 0 * a := by
        exact mul_lt_mul_of_neg_right hb3 ha1
      have hab : a * b < 0 := by
        linarith
      rw [abs_of_neg hab, abs_of_neg ha1, abs_of_pos hb3]
      ring
  · have hb : b < 0 ∨ b ≥ 0 := by
      exact lt_or_le b 0
    cases' hb with hb1 hb2
    · rw [ha2]
    norm_num
    · rw [ha2]
    norm_num
  · have hb : b < 0 ∨ b = 0 ∨ b > 0 := by
      exact lt_trichotomy b 0
    rcases hb with hb1 | hb2 | hb3
    · have htemp : a * b < 0 * b := by
        exact mul_lt_mul_of_neg_right ha3 hb1
      have hab : a * b < 0 := by
        linarith
      rw [abs_of_neg hab, abs_of_pos ha3, abs_of_neg hb1]
      ring
    · rw [hb2]
      norm_num
    · have htemp : 0 * b < a * b := by
        exact mul_lt_mul_of_pos_right ha3 hb3
      have hab : a * b > 0 := by
        linarith
      rw [abs_of_pos hab, abs_of_pos ha3, abs_of_pos hb3]

-- 3.2.07 |a| ≤ |b| iff -|b| ≤ a ≤ |b|
theorem c3_4_f {a b : ℤ} : |a| ≤ |b| ↔ -|b| ≤ a ∧ a ≤ |b| := by
  constructor
  · intro h1
    constructor
    · have ha : a < 0 ∨ a ≥ 0 := by
        exact lt_or_le a 0
      cases' ha with ha1 ha2
      · rw [abs_of_neg ha1] at h1
        linarith
      · rw [abs_of_nonneg ha2] at h1
        linarith
    · have ha : a < 0 ∨ a ≥ 0 := by
        exact lt_or_le a 0
      cases' ha with ha1 ha2
      · have htemp : |b| ≥ 0 := by
          exact c3_4_a
        linarith
      · rw [abs_of_nonneg ha2] at h1
        exact h1
  · intro h2
    cases' h2 with h21 h22
    have ha : a < 0 ∨ a ≥ 0 := by
      exact lt_or_le a 0
    cases' ha with ha1 ha2
    · rw [abs_of_neg ha1]
      linarith
    · rw [abs_of_nonneg ha2]
      linarith

Theorem 3.5. (The Triangle Inequality). If a and b are integers, then |a + b| ≤ |a| + |b|.

We will follow the flow of textbook's proof and make use of the theorems we proved above. You might see something wierd at the last step (starting from h4 part). No worries if you can't understand it! I will explain about that later.

-- 3.2.08 (Theorem 3.5) Triangle Inequality.
-- If a and b are integers, then |a + b| ≤ |a| + |b|
theorem c3_5 {a b : ℤ} : |a + b| ≤ |a| + |b| := by
  have h1a : -|a| ≤ a ∧ a ≤ |a| := by
    exact c3_4_c
  have h1b : -|b| ≤ b ∧ b ≤ |b| := by
    exact c3_4_c
  cases' h1a with h1a_left h1a_right
  cases' h1b with h1b_left h1b_right
  have h2_left : -|a| + (-|b|) ≤ a + b := by
    exact add_le_add h1a_left h1b_left  -- can also use linarith
  have h2_right : a + b ≤ |a| + |b| := by
    exact add_le_add h1a_right h1b_right  -- can also use linarith
  have h3 : -(|a| + |b|) ≤ a + b ∧ a + b ≤ |a| + |b| := by
    constructor
    · rw [neg_eq_neg_one_mul |a|, neg_eq_neg_one_mul |b|] at h2_left
      rw [← mul_add (-1) |a| |b|, ← neg_eq_neg_one_mul (|a| + |b|)] at h2_left
      exact h2_left
    · exact h2_right
  have h4 : |(|a| + |b|)| = |a| + |b| := by
    have h41 : |a| ≥ 0 := by
      exact c3_4_a
    have h42 : |b| ≥ 0 := by
      exact c3_4_a
    have h43 : |a| + |b| ≥ 0 := by
      exact add_le_add h41 h42
    exact abs_of_nonneg h43
  rw [← h4]
  rw [← h4] at h3
  exact (@c3_4_f (a + b) (|a| + |b|)).2 h3

1. Note that the textbook skips something at the last step: you cannot use the part (f) directly if you didn't show that "|a| + |b| = | |a| + |b| |". It might seem obvious to you, but Lean requires you to explicitly show this implicit step, which is why we have an additional step h4.

2. At the last line of code, when we use the theorem (f) (which we named it c3_4_f in this Lean file), we add an @ before it. If you remove this, Lean will throw an error to you. Remember we talked about "implicit arguments" somewhere in this chapter? When we define the theorem c3_4_f, we use {a b : ℤ} to indicate the variables in the statement, and since they are in curly braces instead of in parentheses, they are considered "implicit arguments", so we don't need to input the variables when we use this theorem: Lean will try to infer the correct arguments for us.

   In this case, however, our arguments are "too complicated" for Lean to infer. We want the two integer arguments to be "(a + b)" and "(|a| + |b|)". If Lean cannot figure out the correct arguments by itself, then we need to explicitly (manually) give these inputs. The way to do that is to add @ before the theorem we use. In this way, we can pretend that the theorem uses (a b : ℤ) instead of {a b : ℤ}, so we can give the correct inputs as arguments to the theorem.

3.3. Proof by contrapositive

• Theorem 3.6. Suppose n is an integer. If n² is even, then n is even.
• Theorem 3.7. Let n be an integer. If n² + 2n < 0, then n < 0.

Recall that P → Q ≡ ¬Q → ¬P. To change a goal from P → Q to ¬Q → ¬P in a Lean proof, use the contrapose! tactic.

Also, we need to use the fact that "an integer is not even if and only if it's odd". This is obvious (and vice versa), but Lean is extremely rigorous, so we need to prove this fact... It requires proof by contradiction, which we will cover later, so for now let's just use the existing theorems from Mathlib. This theorem is from another package called "Mathlib.Data.Int.Parity", which is why we imported it at the begining of this Lean file.

Int.odd_iff_not_even {n : ℤ} : Odd n ↔ ¬Even n
We will also need this one, but later: Int.even_iff_not_odd {n : ℤ} : Even n ↔ ¬Odd n

-- 3.3.01 (Theorem 3.6) Suppose n is an integer. If n² is even, then n is even.
theorem c3_6 {n : ℤ} : Even (n^2) → Even n := by
  contrapose!
  intro h
  rw [← Int.odd_iff_not_even]
  rw [← Int.odd_iff_not_even] at h
  cases' h with k h
  use (2*k^2+2*k)
  rw[h]
  ring

-- 3.3.02 (Theorem 3.7) Let n be an integer. If n² + 2n < 0, then n < 0.
theorem c3_7 {n : ℤ} : n^2 + 2 * n < 0 → n < 0 := by
  contrapose!
  intro h1
  have h2 : 0 ≤ n^2 := by
    exact sq_nonneg n
  linarith

3.4. Proof by contradiction

That's it! This is my favorite form of proof :) Let's see why and how it works.

Let's first introduce two new terms: tautology and contradiciton. A tautology is always true, while a contradiction is always false. For example:

We can see that (P ∨ ¬P) is true in all cases, so (P ∨ ¬P) is a tautology.

We can see that (P ∧ ¬P) is false in all cases, so (P ∧ ¬P) is a contradiction. (These two results are also called "Negation Laws".)

Now let's see the definition of proof by contradiction from the textbook: In a proof by contradiction, we use the fact that a statement and its negation have opposite truth values. To prove that P is true, suppose instead that not(P) is true and apply logic, definitions, and previous results to arrive at a conclusion you know to be false. Then you may conclude that not(P) must be FALSE and thus P must be TRUE.

In short: To prove P, we need to show that (¬P → C), where C stands for contradiction. Let's draw a truth table:

P and (¬P → C) are logically equivalent, which shows why proof by contradiction works.

If we want to prove by contradiction in Lean 4, we need two steps: first step is to negate the goal and make it as a new hypothesis (assume the negation of our goal); second step is to change our goal to "false", which is how Lean denotes contradiction. Luckily, there is a tactic called by_contra that can complete these two steps at once.

-- 3.4.01 If P is true, then P is true
example {P : Prop} (h : P) : P := by
  by_contra h1
  contradiction

We can just use exact h to close the goal, but for a demo of proof by contradiction in Lean, let's use by_contra h1 here, which creates a new hypothesis h1 : ¬P, (which is the negation of the original goal ⊢ P), and changes the goal to ⊢ False.

OK, so now we have two hypotheses: h : P and h1 : ¬P. The contradiction is so obvious! Whenever we see a contradiction in our hypotheses, we can use contradiction tactic to close the goal immediately.

Remark: contradiction can close any goal with contradictory hypotheses. Remember that if the hypothesis is false, the the statement is vacuously true, right? In other words, you don't have to use contradiction tactic for every proof by contridition. See the example below.

• Theorem 3.8. No integer is both even and odd.

-- 3.4.02 (Theorem 3.8.) No integer is both even and odd.
theorem c3_8 (n : ℤ) : ¬(Even n ∧ Odd n) := by
  by_contra h
  cases' h with heven hodd
  cases' heven with k h1
  cases' hodd with l h2
  rw [h1] at h2
  have h3 : 2 * (k - l) = 1 := by
    linarith
  have h4 : (2 : ℤ) ∣ 1 := by
    use (k - l)
    exact h3.symm
  norm_num at h4  

Note that to the fourth to last line, we use (2 : ℤ) instead of simply 2. Since Lean treats the non-negative integers as natural numbers by default, this expression will be the divisibility about natural numbers, which is more complicated than divisibility about integers in Lean (we will see more about that in chapter 6). Therefore, we need to explicitly tell Lean that the 2 here is an integer in this way.

To the second to last line, we use the symm command after the dot. Any time you want to use the symmetry of an equation, just use this command.

The textbook uses a theorem from EPIs table to show that "2 ∣ 1" is a contradiction. Since it's a numerical expression, we can also use norm_num. If norm_num is used on a false expression, it will return "False", which can therefore close our goal.

• Theorem 3.9. √2 is irrational.

To prove that square root of 2 is irrational is a little bit complicated if we only want to use the definitions from Mathlib. For simplicity, we will prove its equivalence. That is, we will set the first few steps of proofs on textbook as our assumptions, so we transform the statement to:

• Suppose m, n are integers, where n ≠ 0 and m and n are not both even. Then 2n² ≠ m².

-- 3.4.03 (Theorem 3.9.) √2 is irrational.
theorem c3_9 {m n : ℤ} (h1 : n ≠ 0) (h2 : ¬(Even m ∧ Even n)) : 2 * n^2 ≠ m^2 := by
  by_contra h3
  have h4 : Even (m^2) := by
    use n^2
    linarith
  have h5 : Even m := by
    exact c3_6 h4
  have h6 : ∃ k, m = k + k := by
    cases' h5 with k h5
    use k
  cases' h6 with k h6
  have h7 : 2 * n^2 - 4 * k^2 = 0 := by
    rw [h3, h6]
    ring
  have h8 : n^2 = k^2 + k^2 := by
    linarith
  have h9 : Even (n^2) := by
    use k^2
  have h10 : Even n := by
    exact c3_6 h9
  have h11 : Even m ∧ Even n := by
    constructor
    · exact h5
    · exact h10
  contradiction

• Theorem 3.10. Let a be an integer. If a² is odd, then a is odd.

Proof by contrapositive is easy. We did similar proof earlier in this chapter. To prove by contradiction, the textbook uses the results from Exercise 3.1 (Note that there is a mistake in textbook: it's from 3.1(b) instead of 3.1(a)). So we will prove Exercise 3.1(a) first.

-- 3.4.04 (Theorem 3.10.) Let a be an integer. If a² is odd, then a is odd.

-- contrapositive

theorem c3_10_a {a : ℤ} : Odd (a^2) → Odd a := by
  contrapose!
  rw [← Int.even_iff_not_odd, ← Int.even_iff_not_odd]
  intro h
  cases' h with k h
  use 2 * k^2
  rw [h]
  ring

-- contradiction

-- Exercise 3.1(b)
theorem e3_1_b {a b : ℤ} (ha : Even a) (hb : Odd b) : Odd (a + b) := by
  cases' ha with k1 h1
  cases' hb with k2 h2
  use (k1 + k2)
  rw [h1, h2]
  ring

-- Then...
theorem c3_10_b {a : ℤ} : Odd (a^2) → Odd a := by
  intro h1
  by_contra h2
  rw [← Int.even_iff_not_odd] at h2
  have h3 : Odd (a + a^2) := by
    exact (e3_1_b h2 h1)
  have h4 : a + a^2= a * (a + 1) := by
    ring
  rw [h4] at h3
  have h5 : Even (a * (a + 1)) := by
    exact c3_3 a
  rw [Int.even_iff_not_odd] at h5
  contradiction

3.5. Proof of an if-and-only-if Statement

Suppose we want to prove (P ↔ Q) in Lean, and we know that (P ↔ Q) is the same as (P → Q) ∧ (Q → P), so our goal is actually a conjunction. Therefore, we need to use the constructor tactic to split our goal to (P → Q) and (Q → P). (you can review chapter 2 if you don't remember this)

• Theorem 3.11. Let a be an integer. Then a is odd if and only if a² − 1 is even.

-- 3.5.01 (Theorem 3.11.) Let a be an integer. Then a is odd if and only if a² −1 is even.
theorem c3_11 {a : ℤ} : Odd a ↔ Even (a^2 - 1) := by
  constructor
  · intro h1
    cases' h1 with k h1
    use (2 * k^2 + 2 * k)
    rw [h1]
    ring
  · contrapose!
    rw [← Int.even_iff_not_odd, ← Int.odd_iff_not_even]
    intro h2
    cases' h2 with k h2
    use 2 * k^2 - 1
    rw [h2]
    ring