Sum of exponents with same base

Question

How can I prove the following statement in Coq?

forall x: nat,
x >= 1 -> 2 * 2 ^ (x - 1) = 2 ^ x.

I found lemma pow_add_r in module NZPow but for some reason I can´t use it.

Thanks, Marcus.

Answer 1

I just saw your answer, but here is an explanation why your initial attempt didn't work, and how to make it run:

You can't directly use Nat.pow_add_r because your goal neither contains a term of the shape a ^ (b + c) nor a ^ b * a ^ c. You have to help Coq to recognize this pattern. In the following script, I first change 2 into 2 ^ 1, then use the lemma you provided.

Require Import Arith.

Lemma foo: forall x: nat, x >= 1 -> 2 * 2 ^ (x - 1) = 2 ^ x.
Proof.
intros x hx.
(* I only want to rewrite one occurrence of 2 *)
pattern 2 at 1; rewrite <- (Nat.pow_1_r 2). 
(* now my goal is 2 ^ 1 * 2 ^ (x-1) = 2 ^ x *)
rewrite <- Nat.pow_add_r.
(* now my goal is 2 ^ (1 + (x - 1)) = 2 ^ x 
   since x >= 1, we can rewrite the first term and conclude *)
now rewrite le_plus_minus_r.
Qed.

PS: you can Require Import Nat if you don't want to prefix the lemmas like I did.

Answer 2

Just managed to build a proof, in case anyone is interested:

Lemma add_exp:
forall n: nat,
n >= 1 -> 2 * 2 ^ (n - 1) = 2 ^ n.
Proof.
destruct n.
- intros H.
  omega.
- intros H.
  assert (H1: n = 0 \/ n >= 1) by omega.
  destruct H1 as [H1 | H1].
  + subst.
    simpl.
    reflexivity.
  + simpl.
    rewrite <- minus_n_O.
    rewrite <- plus_n_O.
    reflexivity.
Qed.

Best Regards, Marcus.