14 - Disquality Again

We've just seen how a lemma can be applied to a proof goal. 

Here we'll see how lemmas can be applied to hypotheses too.

Task

Given a natural number $n<5$, show that

$$n\ne 5$$

This is the very same task as the previous post.

Maths

We're going to use the same lemma we used in the previous chapter. For natural numbers $a$ and $b$, 

$$a<b⟹a\ne b$$

Previously we considered the proof goal $n\ne 5$, and used this lemma to say that proving $n<5$ was sufficient.

This time we'll consider the hypothesis $n<5$, and say that $n\ne 5$ follows directly as a result of that lemma.

The following diagram makes clear this difference. We can see the lemma builds half a bridge from our hypothesis. Do compare it to the diagram from the previous post.

Let's write a proof that applies the lemma to the hypothesis.

$$\begin{array}{rlrl}\text{(1)}& n& <5& & \text{hypothesis}\text{(2)}& n& \ne 5& & \text{proof objective }& & & \\ \text{(3)}& a<b& ⟹a\ne b& & \text{existing lemma}& & & \\ \text{(4)}& n& \ne 5& & \text{lemma }(\text{3})\text{ applied to }(\text{1})& & & \\ ◻& n<5& ⟹n\ne 5& & \text{by lemma }(\text{3})\end{array}$$

Again, this may look a little over-done, but the small steps will help us write a Lean proof. 

• We start with the hypothesis $n<5$, and our proof objective $n\ne 5$. 
• We know about a lemma (3) applicable to natural numbers, that if $a<b$ then $a\ne b$. 
• The lemma's antecedent $a<b$ matches our hypothesis (1), which immediately gives us $n\ne 5$.

Let’s explain some terminology. In an implication $P⟹Q$, $P$ is called the antecedent, and $Q$ the consequent.

Code

The following Lean program proves that a natural number $n\ne 5$, given $n<5$.

-- 14 - Lemma: Not Equal from Less Than

import Mathlib.Tactic

example {n : ℕ} (h : n < 5) : n ≠ 5 := by
  apply ne_of_lt at h
  exact h

The Lean proof is almost exactly the same as the previous post's proof.

The only difference is the lemma ne_of_lt is pointed at the hypothesis h by adding at h.

This small change is significant. It changes the hypothesis h from h : n < 5 to h : n ≠ 5, as we'll see in the Infoview.

This new hypothesis exactly matches the proof goal, so exact h works just as before to complete the proof.

Infoview

Placing the cursor before apply ne_of_lt at h shows the original hypothesis.

n : ℕ
h : n < 5
⊢ n ≠ 5

Moving the cursor to the beginning of the next line after apply ne_of_lt at h shows the hypothesis has been replaced.

n : ℕ
h : n ≠ 5
⊢ n ≠ 5

---

Easy Exercise

Write a Lean program to prove $n\ne 5$, given $n>5$, where $n$ is a natural number.

Use the same the lemma for “not equal from greater than” you found for the last post's exercise, and apply it to the hypothesis.