(beginner maths) stating which things are natural numbers

Stream: new members

[rzeta0]

Here is a very very easy task:

Given $a = 4$, we want to prove $a>1$.

Here is a proof:

import Mathlib.Tactic

example {a: ℕ} (h1: a = 4) : a > 1 := by
  calc
    a = 4 := by rw [h1]
    _ > 1 := by norm_num

Notice how in the original statement I failed to state $a \in ℕ$. In fact it also failed to state $1 \in ℕ$.

I assume that in order for norm_num to work, we need to declare the type of objects it is being asked to reason over.

Questions: (apoligies, I'm no expert)

• Strictly speaking norm_num is being asked to reason about 4 and 1. Is it using h1 to infer that $4 \in ℕ$ ?
• How is it inferring that $1 \in ℕ$ ?
• Putting Lean aside and looking at the pure maths above, why don't mathematicians state that $1 \in ℕ$? (Am i overthinking it?)

[Damiano Testa]

With numerals, Lean defaults to Nat, when no type information is given. For instance, this works:

example : 4 > 1 := by norm_num

Hovering over 4 and 1 you should see what type Lean assigned to the numerals.

In your context, 4 could be deduced to be in Nat from a = 4 and 1 could be deduced to be in Nat as well from a > 1. In fact, if you try

example {a: Int} (h1: a = 4) : a > 1 := by
  calc
    a = 4 := by rw [h1]
    _ > 1 := by norm_num

you can see that now 1 and 4 are in Int.

[rzeta0]

Thanks Damiano - that is very helpful insight.

Can I ask why Lean defaults to Nat when no type is given - it seems like a recipe for error, or unfounded assumptions .. especially for software that is intended to be a theorem prover?

Is it because this was a feature of Lean, before it was used as a maths proof assistant?

[Damiano Testa]

I'm not sure what the motivation is, but it does not seem a strange convention that 1 means the natural number 1 to me.

[Henrik Böving]

Damiano Testa said:

With numerals, Lean defaults to Nat, when no type information is given. For instance, this works:

example : 4 > 1 := by norm_num

Hovering over 4 and 1 you should see what type Lean assigned to the numerals.

In your context, 4 could be deduced to be in Nat from a = 4 and 1 could be deduced to be in Nat as well from a > 1. In fact, if you try

example {a: Int} (h1: a = 4) : a > 1 := by
  calc
    a = 4 := by rw [h1]
    _ > 1 := by norm_num

you can see that now 1 and 4 are in Int.

I think this is mostly for usability. If we were to give the actual error here, which is some rambling about how an OfNat instance for this meta variable here could not be synthesized, a new user might get very scared if they just entered #check 1. We could of course also provide an error that explains the general issue but compared to this going with Nat feels fine to me? After all type inference will pick up on the fact that you are e.g. using an int to compare with a numeral and use the correct numeral type as you demonstrated.