naming variables in pen-paper maths proofs

Stream: new members

[rzeta0]

Consider the following:

$$\begin{align} a\le b\;&\lor\;b+1\le a&&\text{proof objective, }a,b\in\mathbb{N}\\ &&&\\ a\le b\;&\lor\;b<a&&\text{known lemma, }a,b\in\mathbb{N}\\ m+1\le n&\iff m<n&&\text{known lemma, }m,n\in\mathbb{N}\\ &&&\\ a\le b\;&\lor\;b+1\le a&&\text{apply lemma }(4)\text{ to }(3)\\ \end{align}$$

and compare it to

$$\begin{align} a\le b\;&\lor\;b+1\le a&&\text{proof objective, }a,b\in\mathbb{N}\\ &&&\\ c\le d\;&\lor\;d<c&&\text{known lemma, }c,d\in\mathbb{N}\\ m+1\le n&\iff m<n&&\text{known lemma, }m,n\in\mathbb{N}\\ &&&\\ a\le b\;&\lor\;b+1\le a&&\text{apply lemma }(10)\text{ to }(9)\\ \end{align}$$

The difference is that in the first example I'm using $a, b$ in lemma (3), but in the second example I'm using $c,d$ in lemma (9).

Question: Is the first example ok or is it frowned upon to use variables $a,b$ when they are also used in the proof objective?

I'm not formally educated in mathematics so I can only go by what I feel is about right. Here The first feels more natural as rewriting (3) matches the proof objective lexically, meaning reduced cognitive load.

Also, I don't think the variable names will cause confusion. Even being strictly mathematical, I don't think the first contains any false or conflicting statements.

[Ruben Van de Velde]

Is this a lean question?

[rzeta0]

should I move it to the "maths" channel?

[Dan Velleman]

Two suggestions:

1. Use more English. It took me a while to figure out that line (1) is the statement of the theorem you want to prove, and the proof starts on line (3).
2. Be explicit about quantifiers. You say that line (6) is justified by applying (4) to (3). That only makes sense if you are assuming that line (4) means $\forall m,n \in \mathbb{N}, m + 1 \le n \Leftrightarrow m < n$. You can then apply (4) with $m = b$ and $n = a$ to conclude that $b + 1 \le a \Leftrightarrow b < a$, and then combine that with (3) to get (6).
   But if that's what (4) means, then does (1) mean $\forall a,b \in \mathbb{N}, a \le b \vee b + 1 \le a$? If so, then the first step of your proof should be "Let $a$ and $b$ be arbitrary natural numbers" (corresponding to using intro in Lean). Lean will keep you honest about these things. For example, if you state your theorem as ∀ (a b : ℕ), a ≤ b ∨ b + 1 ≤ a, then it is only after you use intro a b that Lean will list a b : ℕ in the tactic state, which then allows you to use a and b as free variables in further steps. If you try to state (4) using have h4 : m + 1 ≤ n ↔ m < n := ... , then Lean will complain that it doesn't know what m and n are. But you can say have h4 : ∀ (m n : ℕ), m + 1 ≤ n ↔ m < n := by intro m n; rfl, and then h4 b a will be a proof of b + 1 ≤ a ↔ b < a.

To answer your original question about naming variables: If the variables are bound by quantifiers, then you can use whatever names you want: $\forall x, P(x)$ means the same thing as $\forall y, P(y)$. If the variables are free (not bound by quantifiers), then they should refer to particular objects that were introduced in either the statement of the theorem or earlier steps of the proof, and of course you must use the names of the objects you want to refer to.

[rzeta0]

Thanks @Dan Velleman

Your point (2) has caused me some anxiety!

The following is a lemma which I had assumed applies to "for all" a and b natural numbers. The lemma statement doesn't use ∀ in the conclusion, and the proof itself doesn't use intro.

Does this mean I have been deluding myself about what this, and the many other short lean proofs I've been working through as I go through Mechanics of Proof?

import Mathlib.Tactic

lemma Nat.le_or_succ_le (a b : ℕ): a ≤ b ∨ b + 1 ≤ a := by
  rw [Nat.add_one_le_iff]
  exact le_or_lt a b

[Kevin Buzzard]

Do you understand how the revert tactic does the opposite of the intro tactic? Try revert b and then revert a at the beginning of the proof (before the rewrite), and then look at the goal. Then try intro a and intro b and you're back where you started.

[Philippe Duchon]

rzeta0 said:

The following is a lemma which I had assumed applies to "for all" a and b natural numbers. The lemma statement doesn't use ∀ in the conclusion, and the proof itself doesn't use intro.

Your lemma (or the context in which you are stating and proving it) has no hypotheses describing any properties of parameters a and b, so if you manage to prove it, it means that your proof is valid for any a and b that match the explicit hypotheses - that is, that both are natural numbers, and that's all. In other words, you might as well have stated your lemma with universal quantifiers on both variables.

In fact, if you state your lemma with an explicit universal quantifier at the start, and you then #check it, you will see that Lean doesn't display the quantifier.

[Ruben Van de Velde]

In fact, let me show you a trick:

#check (Nat.le_or_succ_le)
  -- Nat.le_or_succ_le : ∀ (a b : ℕ), a ≤ b ∨ b + 1 ≤ a

[Ruben Van de Velde]

Without the parentheses, lean tries to be more clever in the output, but this shows that Nat.le_or_succ_le actually does prove a forall-statement

[Eric Wieser]

#check @Nat.le_or_succ_le works more generally for this trick

[rzeta0]

phew - I am relieved that without any quantifiers, lean assumes "for all".

I tested what you recommended with revert and can see that it "undoes" what lean might be doing by assuming "for all a b".

[Dan Velleman]

Sorry if my previous message caused confusion. But here's an example that illustrates the point I was trying to make. Here's a Lean proof that carries out the reasoning I think you were after in your original quesion:

example (a b : ℕ) (h3 : a ≤ b ∨ b < a)
    (h4 : ∀ (m n : ℕ), m + 1 ≤ n ↔ m < n) :
    a ≤ b ∨ b + 1 ≤ a := by
  rw [h4 b a]
  exact h3

The hypotheses h3 and h4 correspond to your (3) and (4), and I have made it explicit that (4) is supposed to apply to all m and n. Then h4 b a is a proof of b + 1 ≤ a ↔ b < a, and using that in rw changes the goal to a ≤ b ∨ b < a, which matches h3. In fact, you can just write rw [h4], and Lean will be smart enough to figure out that it needs to plug in b for m and a for n to make the rewriting work.

[Dan Velleman]

However, if you do it this way:

example (a b m n : ℕ) (h3 : a ≤ b ∨ b < a)
    (h4 : m + 1 ≤ n ↔ m < n) :
    a ≤ b ∨ b + 1 ≤ a := by
  rw [h4]
  exact h3

then it doesn't work. You get an error message at the rw step.

[Dan Velleman]

The tactic state at the beginning of the attempted proof of the second example is:

a b m n : ℕ
h3 : a ≤ b ∨ b < a
h4 : m + 1 ≤ n ↔ m < n
⊢ a ≤ b ∨ b + 1 ≤ a

This means a, b, m, and n stand for some fixed but unspecified natural numbers, and we are assuming that h3 and h4 are true of those natural numbers. But we aren't assuming h4 is true of all natural numbers m and n, so you can't plug in b for m and a for n as in the previous proof. That's why I thought your proposed proof, as you wrote it, was potentially misleading, and spelling out the quantifiers was helpful.