具有相同基数的指数之和

Question

如何在Coq中证明以下陈述？

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

我pow_add_r在模块中找到了引理,NZPow但由于某种原因我无法使用它.

谢谢,马库斯.

Answer 1

我刚看到你的答案,但这里有一个解释为什么你的初步尝试不起作用,以及如何让它运行:

你无法直接使用,Nat.pow_add_r因为你的目标既不包含形状a ^ (b + c)也不包含形状a ^ b * a ^ c.你必须帮助Coq识别这种模式.在下面的脚本中,我首先2进入2 ^ 1,然后使用您提供的引理.

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:你可以,Require Import Nat如果你不想像我这样做前缀.