gpt4 book ai didi

coq - 同底指数之和

转载 作者:行者123 更新时间:2023-12-02 14:01:44 25 4
gpt4 key购买 nike

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

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

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

谢谢,马库斯。

最佳答案

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

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

关于coq - 同底指数之和,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/31001900/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com