An edge case for (a - b : ℕ) in omega?

Stream: new members

[Deming Xu]

Hello! I’d like to show you this piece of code. It seems that omega relies on this "hint" line to prove the equation.

import Mathlib.Tactic

example (n : ℕ) : 2 * (2 ^ n - 1) + 1 = 2 * 2 ^ n - 1 := by
  have hint : 2 ^ n ≥ 1 := Nat.one_le_pow n 2 (show 2 > 0 by norm_num)
  omega

This proof is probably trickier than it seems, because in Lean subtraction on ℕ saturates.
For example, 3 - 5 = 0 because the negative number -2 gets truncated to 0.

Nat.sub_eq_zero_of_le {n m : ℕ} (h : n ≤ m) : n - m = 0

So in general a - 2 + 1 = a - 1 does not hold. However here a = 2*2^n, so a ≥ 2 and it does hold.

[Henrik Böving]

Omega only deals with linear arithmetic, domain knowledge about other arithmetics like 2^n never being zero is out of its scope