Wednesday, October 30, 2024

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 \neq 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\implies a\ne b$$

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

This time we'll consider the hypothesis $n<5$, and say that $n\ne5$ 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{align}n&<5&&\text{hypothesis}\tag{1}\label{14.1}\\n&\neq5&&\text{proof objective }\tag{2}\label{14.2}\\&&&\\a<b&\implies a\neq b&&\text{existing lemma}\tag{3}\label{14.3}\\&&&\\n&\ne5&&\text{lemma }(\ref{14.3})\text{ applied to }(\ref{14.1})\tag{4}\label{14.4}\\&&&\\n<5&\implies n\neq5&&\text{by lemma }(\ref{14.3})\tag*{\(\Box\)}\end{align}$$

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\ne5$. 
  • 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\ne5$.

Let’s explain some terminology. In an implication $P\implies 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\ne5$, 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.


at