3. Logic

In the last chapter, we dealt with equations, inequalities, and basic mathematical statements like “\(x\) divides \(y\).” Complex mathematical statements are built up from simple ones like these using logical terms like “and,” “or,” “not,” and “if … then,” “every,” and “some.” In this chapter, we show you how to work with statements that are built up in this way.

3.1. Universal Quantifier ∀ and `intro`

3.1.1. `intro`

To prove a statement with universal quantifier ∀, we need to use intro tactic.

theorem my_lemma4 :
    ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  -- useful theorems: ``abs_mul``, ``mul_le_mul``, ``abs_nonneg``, ``mul_lt_mul_right``, ``one_mul``
  intro x y ε epos ele1 xlt ylt
  calc
    |x * y| = |x| * |y| := sorry
    _ ≤ |x| * ε := sorry
    _ < 1 * ε := sorry
    _ = ε := sorry

intro give names to variables defined by the universal quantifiers and also unnamed hypotheses, so you can use them later in your proof.
- We can use any names we want; they do not have to be x, y, and ε.
- We have to introduce the variables (in the statement to be proved), even though they are marked implicit!
- Making some variables implicit means we can omit them when using my_lemma. But they are still an essential part of the statement when we prove the lemma.
Universal quantifiers may hide in definitions (in the statement to be proved). Lean will unfold definitions to expose them. It’s our job to check definitions and ``intro`` variables/hypotheses!

Example:

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

example (hfa : FnUb f a) (hgb : FnUb g b) : FnUb (fun x ↦ f x + g x) (a + b) := by -- lambda abstraction
  intro x  -- no need to apply ``intro`` to the FnUb in ``hfa`` and ``hgb`` since they are already proven.
  dsimp  -- simplification. (The “d” stands for “definitional.”)
  apply add_le_add
  apply hfa
  apply hgb

3.1.2. Example: `Monotone`

For another example of a hidden universal quantifier, Mathlib defines a predicate Monotone, which says that a function is nondecreasing in its arguments:

example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x := by
  intro a b aleb
  apply add_le_add
  apply mf aleb
  apply mg aleb

Try proving these, with either tactics or proof terms:

example {c : ℝ} (mf : Monotone f) (nnc : 0 ≤ c) : Monotone fun x ↦ c * f x :=
  sorry

example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f (g x) :=
  sorry

3.1.3. Example: Even/Odd Functions

A function \(f\) from \(\Bbb R\) to \(\Bbb R\) is said to be even if \(f(-x) = f(x)\) for every \(x\), and odd if \(f(-x) = -f(x)\) for every \(x\).

def FnEven (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = f (-x)

def FnOdd (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = -f (-x)

example (ef : FnEven f) (eg : FnEven g) : FnEven fun x ↦ f x + g x := by
  intro x
  calc
    (fun x ↦ f x + g x) x = f x + g x := rfl
    _ = f (-x) + g (-x) := by rw [ef, eg]


example (of : FnOdd f) (og : FnOdd g) : FnEven fun x ↦ f x * g x := by
  sorry

example (ef : FnEven f) (og : FnOdd g) : FnOdd fun x ↦ f x * g x := by
  sorry

example (ef : FnEven f) (og : FnOdd g) : FnEven fun x ↦ f (g x) := by
  sorry

3.2. The Existential Quantifier

The existential quantifier, which can be entered as \ex in VS Code, is used to represent the phrase “there exists.” The formal expression ∃ x : ℝ, 2 < x ∧ x < 3 in Lean says that there is a real number between 2 and 3. (We will discuss the conjunction symbol, ∧, in Section 3.4.) The canonical way to prove such a statement is to exhibit a real number and show that it has the stated property. The number 2.5, which we can enter as 5 / 2 or (5 : ℝ) / 2 when Lean cannot infer from context that we have the real numbers in mind, has the required property, and the norm_num tactic can prove that it meets the description.

3.2.1. Prove Existence with `use`

use tactic provides the object to satisfy an existential quantifier, leaving the goal of proving the property.

example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
  use 5 / 2
  norm_num

You can give the use tactic proofs as well as data:

example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
  have h1 : 2 < (5 : ℝ) / 2 := by norm_num
  have h2 : (5 : ℝ) / 2 < 3 := by norm_num
  use 5 / 2, h1, h2

In fact, the use tactic automatically tries to use available assumptions as well.

example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 := by norm_num
  use 5 / 2

3.2.2. Use Existential Statements by Unpacking Information

Unpacking information in a hypothesis is very important. Lean and Mathlib provide a number of ways to do it.

3.2.2.1. `rcases` and `obtain`

Given the following statements:

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

def FnHasUb (f : ℝ → ℝ) :=
  ∃ a, FnUb f a

def FnHasLb (f : ℝ → ℝ) :=
  ∃ a, FnLb f a

theorem fnUb_add {f g : ℝ → ℝ} {a b : ℝ} (hfa : FnUb f a) (hgb : FnUb g b) :
    FnUb (fun x ↦ f x + g x) (a + b) :=
  fun x ↦ add_le_add (hfa x) (hgb x)

We can prove:

variable {f g : ℝ → ℝ}

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  rcases ubf with ⟨a, ubfa⟩  -- ``obtain ⟨a, ubfa⟩ := ubf`` also works
  rcases ubg with ⟨b, ubgb⟩  -- ``obtain ⟨b, ubgb⟩ := ubg`` also works
  use a + b
  apply fnUb_add ubfa ubgb

rcases / obtain unpacks the information in the existential quantifier. It destructure hypotheses or expressions.
- They introduces new variables (e.g. a) and/or hypotheses (e.g. ubfa) into the current proof state context, so we can use them later.
- The proof goal is unchanged.
Annotation ⟨a, ubfa⟩ is the pattern that describes the information that we expect to find when we unpack the main argument.

example (lbf : FnHasLb f) (lbg : FnHasLb g) : FnHasLb fun x ↦ f x + g x := by
  sorry

example {c : ℝ} (ubf : FnHasUb f) (h : c ≥ 0) : FnHasUb fun x ↦ c * f x := by
  sorry

(Similar to Universal quantifiers) Existential quantifiers may also hide in definitions (in the statement to be proved). It’s our job to be aware of them in definitions and unpace variables/hypotheses!

For example, divisibility is implicitly an “exists” statement.

example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by
  rcases divab with ⟨d, beq⟩
  rcases divbc with ⟨e, ceq⟩
  rw [ceq, beq]
  use d * e; ring


example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by
  -- ``rfl`` in place of a new identifier, rcases does the rewriting automatically
  rcases divab with ⟨d, rfl⟩
  rcases divbc with ⟨e, rfl⟩
  use d * e; ring

3.2.2.2. `rintro`

The rintro tactic is a combination of intro and rcases:

example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x := by
  -- we need intro because hypotheses ``FnHasUb f`` and ``FnHasUb g`` are unnamed
  rintro ⟨a, ubfa⟩ ⟨b, ubgb⟩  -- intro and immediately unpack
  exact ⟨a + b, fnUb_add ubfa ubgb⟩

example (x y : ℝ) (h : x - y ≠ 0) : (x ^ 2 - y ^ 2) / (x - y) = x + y := by
  field_simp [h]  -- clear denominators
  ring

3.3. Proving Statements of Negation: Counterexample, `by_contra`, `push_neg`, `contrapose`

¬ A abbreviates A → False, i.e., there are contradictions in the proof state context.
We prove ¬ A by introducing a hypothesis h : A via intro, and then proving False.
¬ has a low precedence:
- ¬ x < y: x is not less than y
- ¬ ∃ z, x < z ∧ z < y: there does not exist a z strictly between x and y.

Examples:

example (h : a < b) : ¬b < a := by
  intro h'  -- name ``b → a``
  -- Lean does not care if statements are indeed true or false. Lean only proves by local context.
  have : a < a := lt_trans h h'
  apply lt_irrefl a this

linarith scans the local context for linear (in)equality. When it detects that the system is inconsistent it produces a proof of False.

example (h : ∀ a, ∃ x, f x > a) : ¬FnHasUb f := by
  intro fnub
  rcases fnub with ⟨a, fnuba⟩
  -- rintro ⟨a, fnuba⟩
  rcases h a with ⟨x, hx⟩
  have : f x ≤ a := fnuba x
  linarith  -- linarith can prove either true or false

example (h : ∀ a, ∃ x, f x < a) : ¬FnHasLb f :=
  sorry

example : ¬FnHasUb fun x ↦ x :=
  sorry

Mathlib offers a number of useful theorems for relating orders and negations:

#check (not_le_of_gt : a > b → ¬a ≤ b)
#check (not_lt_of_ge : a ≥ b → ¬a < b)
#check (lt_of_not_ge : ¬a ≥ b → a < b)
#check (le_of_not_gt : ¬a > b → a ≤ b)

We can prove the negation of a universally quantified statement by giving a counterexample.

example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
  intro h
  -- we will now create a counterexample
  let f := fun x : ℝ ↦ (0 : ℝ)  -- adds a *local definition* to the context
  have monof : Monotone f := by sorry
  have h' : f 1 ≤ f 0 := le_refl _
  sorry

by_contra allows us to prove a goal Q by assuming ¬ Q and deriving a contradiction.

variable {α : Type*} (P : α → Prop) (Q : Prop)

example (h : ¬∀ x, P x) : ∃ x, ¬P x := by
  by_contra h'
  apply h
  intro x
  show P x
  by_contra h''
  exact h' ⟨x, h''⟩

push_neg can replace statements of negation with equivalent forms in which the negation has been pushed inward.
- push_neg at h restates the hypothesis h.

example (h : ¬∀ a, ∃ x, f x > a) : FnHasUb f := by
  push_neg at h
  exact h

example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
  dsimp only [FnHasUb, FnUb] at h  -- expand the definitions of ``FnHasUb`` and ``FnUb``
  push_neg at h
  exact h

contrapose transforms a goal A → B to ¬B → ¬A.
contrapose! runs contrapose and then pushes negations inside both A and B.

example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
  contrapose! h
  exact h

3.4. Proving and Using Conjunction

constructor allows you to prove A ∧ B by first proving A and then proving B.

example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by
  constructor
  · assumption  -- tells Lean to find an assumption/hypothesis that will solve the goal
  intro h
  apply h₁
  rw [h]

Using a statement of conjunctions requires unpacking parts, with rcases or rintro.

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  rcases h with ⟨h₀, h₁⟩
  contrapose! h₁
  exact le_antisymm h₀ h₁

example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬y ≤ x := by
  rintro ⟨h₀, h₁⟩ h'
  exact h₁ (le_antisymm h₀ h')

You can also unpack a hypothesis h : A ∧ B using h.left and h.right, or, equivalently, h.1 and h.2.

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  intro h'
  apply h.right
  exact le_antisymm h.left h'

To use a statement of both ∃ and ∧, you can unpact together.

example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y := by
  rintro ⟨z, xltz, zlty⟩
  exact lt_trans xltz zlty
  -- apply lt_trans
  -- · exact xltz
  -- exact zlty

To prove a statement of both ∃ and ∧, you can use the use tactic:

example : ∃ x : ℝ, 2 < x ∧ x < 4 := by
  use 5 / 2
  constructor <;> norm_num  -- <;> is a tactic-combinator: pipes every goal produced by the left tactic into the right tactic

example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by
  use 5  -- m
  use 7  -- n
  norm_num

The bi-implication A ↔ B can be considered as (A → B) ∧ (B → A), so you cal use constructor to unpack.

example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by
  constructor
  · contrapose!  -- ¬y ≤ x → x ≠ y
    rintro rfl
    rfl
  contrapose!  -- x ≠ y → ¬y ≤ x
  exact le_antisymm h

3.5. Disjunction

To prove a disjunction A ∨ B is to prove A or to prove B.
The left tactic chooses A, and the right tactic chooses B.

variable {x y : ℝ}

example (h : y > x ^ 2) : y > 0 ∨ y < -1 := by
  left
  linarith [pow_two_nonneg x]

example (h : -y > x ^ 2 + 1) : y > 0 ∨ y < -1 := by
  right
  linarith [pow_two_nonneg x]

To use a hypothesis of the form A ∨ B, we need rcases and also need to consider both cases. Here is the syntax:

rcases ⟨p ∨ q⟩ [args] with hp | hq
  -- two goals are now open:
  · goal, assuming hp : p
  · goal, assuming hq : q

In the next example, we tell Lean to use the name h on each branch.

example : x < |y| → x < y ∨ x < -y := by
  -- le_or_gt: a ≤ b ∨ b < a
  -- both the hypothesis and the goal has disjunction
  rcases le_or_gt 0 y with h | h  -- ``h`` in local context, name reused; we use | instead of ⟨, ⟩
  · rw [abs_of_nonneg h]
    intro h; left; exact h
  · rw [abs_of_neg h]
    intro h; right; exact h

You can also use rcases and rintro with nested disjunctions. When these result in a genuine case split with multiple goals, the patterns for each new goal are separated by a vertical bar.

example {x : ℝ} (h : x ≠ 0) : x < 0 ∨ x > 0 := by
  rcases lt_trichotomy x 0 with xlt | xeq | xgt
  · left
    exact xlt
  · contradiction
  · right; exact xgt

3.6. Sequences and Functional Equality

In Lean, we can represent a sequence \(s_0, s_1, s_2, \ldots\) of real numbers as a function s : ℕ → ℝ.

def ConvergesTo (s : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

3.6.1. `ext`

ext (function extensionality) enables us to prove an equation between functions by proving that their values are the same at all the values of their arguments: ∀ (x : Type), f x = g x → f = g

example : (fun x y : ℝ ↦ (x + y) ^ 2) = fun x y : ℝ ↦ x ^ 2 + 2 * x * y + y ^ 2 := by
  ext  -- introduces fresh variables for arguments of functions.
  ring

3.6.2. `congr`

congr allows us to prove the equation by reconciling the parts that are different:

example (a b : ℝ) : |a| = |a - b + b| := by
  congr  -- peels off the ``abs`` on each side
  ring

3.6.3. `convert`

convert applies a theorem to a goal when the conclusion of the theorem doesn’t fully match.

For example, suppose we want to prove a < a * a from 1 < a. A theorem in the library, mul_lt_mul_right, will let us prove 1 * a < a * a. Instead, the convert tactic lets us apply the theorem as it is, and leaves us with the task of proving the equations that are needed to make the goal match.

example {a : ℝ} (h : 1 < a) : a < a * a := by
  -- In mul_lt_mul_right, (a0 : 0 < a) : b < c ↔ b * a < c * a
  -- "h : 1 < a" vs. "b < c" => "assign" 1 to b and a to c => 1 * a < a * a
  -- but our goal is a < a * a! => the minimal change is to rewrite a to 1 * a
  convert (mul_lt_mul_right _).2 h
  -- what are mismatched goals left? 1) a = 1 * a; 2) 0 < a (what was left in _)
  · rw [one_mul]
  exact lt_trans zero_lt_one h

This example illustrates another useful trick: when we apply an expression with an underscore and Lean can’t fill it in for us automatically, it simply leaves it for us as another goal.

3. Logic

3.1. Universal Quantifier ∀ and intro

3.1.1. intro

3.1.2. Example: Monotone

3.1.3. Example: Even/Odd Functions

3.2. The Existential Quantifier

3.2.1. Prove Existence with use