同底指数之和

Question

如何在 Coq 中证明下面的命题？

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

我在模块 NZPow 中找到了引理 pow_add_r，但由于某些原因我无法使用它。

谢谢，马库斯.

Answer 1

刚刚设法建立了一个证明，以防有人感兴趣：

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.

此致，马库斯.

Answer 2

我刚看到你的回答，但这里有一个解释为什么你最初的尝试没有成功，以及如何做到这一点运行:

您不能直接使用 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。

同底指数之和

Sum of exponents with same base

coq