Simple arithmetic identities on Nat

Stream: new members

[Ayhon]

I'm having trouble proving the following proposition, which should be simple enough.

h: Nat |- 2 + (2 ^ h - 1) + (2 ^ h - 1) = 2 ^(h+1)

Using simpl_arith reduces the left hand side to 2 * (2 ^ h - 1) + 2 = 2 ^ (h + 1), and I have been trying to continue from there by using calc, but it has been a bit more involved that I had expected at first. Does anyone know of a simple way of solving these kinds of simple arithmetic identities?

[Edward van de Meent]

the characteristic that makes this kind of statement more involved than usual, is that it involves a subtraction where it is not immediately clear that the left operand is at least the right operand. in this case, you will somewhere need to make use of the fact that 2 ^ h is at least 1 for all h.
as such, i'd assume the best way to go about this is to make sure 2 ^ h is the only expression containing h, use have to add to the context that 1 <= 2 ^ h, then use generalize 2 ^ h = z at this ⊢. from that point on, i think the omega tactic should suffice.

[Edward van de Meent]

concretely:

import Mathlib
example (h: Nat) : 2 + (2 ^ h - 1) + (2 ^ h - 1) = 2 ^(h+1) := by
  rw [pow_add,pow_one]
  have : 1 ≤ 2 ^ h := Nat.one_le_pow h 2 (Nat.zero_lt_two)
  generalize 2 ^ h = z at this ⊢
  omega

[Sébastien Gouëzel]

You don't even need the generalize step, as omega will treat 2 ^ h like an atom.

[Scott Carnahan]

You can use rw? to find a result that reduces 2 ^ (h + 1), e.g., rw [Nat.two_pow_succ]
Then, use have : 1 ≤ 2 ^ h := by exact? to get Nat.one_le_two_pow.

[Edward van de Meent]

yea, i just feel like these theorems are more generally applicable and therefore good to know about. (although i did have to search for Nat.zero_lt_two ironically :upside_down: )

[Ayhon]

I had never heard of omega before. What does it do?

[Edward van de Meent]

it is a tactic which proves (in)equalities of natural numbers

[Edward van de Meent]

see also the hover-text

[Henrik Böving]

Edward van de Meent said:

it is a tactic which proves (in)equalities of natural numbers

*linear (in)equalities