ring_nf failure

Stream: mathlib4

[Ben Goodrich]

I am baffled by this example:

import Mathlib

example : 2 ^ (2 ^ (k + 1) - 2 + 1) = 2 ^ (2 ^ (k + 1) - 1) := by
  ring_nf

which does not close the goal (and neither does simp_arith, etc.). The tactics that seem obvious to me write the left-hand side in a variety of forms that are not the right-hand side.

Also, if someone could tell me how to add 1 to -2 in this context, I would appreciate it.

[Ruben Van de Velde]

What type are you working in?

[Luigi Massacci]

The problem is the nasty Nat subtraction. Here is the first thing I could think of that works:

import Mathlib

example : 2 ^ (2 ^ (k + 1) - 2 + 1) = 2 ^ (2 ^ (k + 1) - 1) := by
  congr
  have : 2 ≤ 2^(k+1) := le_self_pow₀ (show 1 ≤ 2 by norm_num) (show k + 1 ≠ 0  by linarith)
  omega

[Ben Goodrich]

Luigi Massacci said:

The problem is the nasty Nat subtraction. Here is the first thing I could think of that works:

import Mathlib

example : 2 ^ (2 ^ (k + 1) - 2 + 1) = 2 ^ (2 ^ (k + 1) - 1) := by
  congr
  have : 2 ≤ 2^(k+1) := le_self_pow₀ (show 1 ≤ 2 by norm_num) (show k + 1 ≠ 0  by linarith)
  omega

Thank you. I figured the issue had something to do with types, but I was surprised that none of Lean's obvious tactics recognized that the exponents were natural numbers for any natural number k.

[Luigi Massacci]

I’m not sure I understand what you mean, but keep in mind that if you replace k+1 with k in your statement then it becomes untrue, which is not at all obvious to someone not familiar with lean, so it’s not that surprising the automation needs an extra hint

[Luigi Massacci]

(deleted)

[Kevin Buzzard]

The issue is not the exponents, the issue is that subtraction of naturals is a pathological operation in Lean: from how you're speaking it seems that you might think that the example says something simpler than what it says, which is "2^(("the number which is 2^(k+1)-2 if this is non-negative, else zero" + 1) = 2^("the number which is 2^(k+1)-1 if this is non-negative, else 0")". In particular what you have written is far more convoluted than how it looks and thus Lean will have a hard time proving it.

[Luigi Massacci]

Kevin Buzzard said:

The issue is not the exponents, the issue is that subtraction of naturals is a pathological operation in Lean: from how you're speaking it seems that you might think that the example says something simpler than what it says, which is "2^(("the number which is 2^(k+1)-2 if this is non-negative, else zero" + 1) = 2^("the number which is 2^(k+1)-1 if this is non-negative, else 0")". In particular what you have written is far more convoluted than how it looks and thus Lean will have a hard time proving it.

I should have probably underlined the relation between the two things for @Ben Goodrich. The +1 by « coincidence » saves you from the pathology of nat substraction, and could give the idea that some trivial algebraic manipulations and integer simplifications to get things to a normal form are all that is required, while really there is some more sophisticated case analysis going on under the hood. You can witness that by the fact that the « obvious » proof should « obviously » work when replacing k+1 with k, but it doesn’t and indeed can’t

[Ben Goodrich]

Thank you Kevin and Luigi for clarifying that the example I wrote was far more convoluted than how it seemed in my head.

[Kevin Buzzard]

For example if you change from naturals to systems of numbers where subtraction is not pathological (for example the reals and integers) then ring solves the goal no problem:

import Mathlib

example (k : ℕ) : (2 : ℝ) ^ ((2 : ℤ) ^ (k + 1) - 2 + 1) = 2 ^ ((2 : ℤ) ^ (k + 1) - 1) := by
  ring

[Notification Bot]

10 messages were moved here from #general > "Missing Tactics" list by Floris van Doorn.