兑现一笔款项并使其匹配假设

发布于 2025-01-21 20:34:12 字数 242 浏览 3 评论 0原文

除了时代6以外，我已经展开了所有内容，但是我很难摆脱额外的“ +1”，这阻止了我重写

1个子目标 n：nat ihn：6 * sum_n2 n = n *（n + 1） *（2 * n + 1） SN：S n = n + 1 ______________________________________（1/1） 6 * s（n + n *（n + 1） + sum_n2 n）=（n + 1） *（n + 1 + 1） *（2 *（n + 1） + 1）

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

以歌曲疗慰 2025-01-28 20:34:12

这看起来像是一个教程练习，因此这取决于您拥有哪种引理。 COQ具有搜索功能，可以帮助您找到引理。

以下是您如何使用标准库引理解决此问题的一个示例 - 可能对您不起作用，例如早期的SF章节具有自己的NAT定义和引理。但是搜索功能应显示您拥有的同等引理。

Require Import PeanoNat.

Axiom sum_n2: nat->nat.

Example E1 : forall (n : nat) (IHn : 6 * sum_n2 n = n * (n + 1) * (2 * n + 1)),
  6 * S (n + n * (n + 1) + sum_n2 n) = (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1).
Proof.
  intros.
  Search (S _) (_ + 1).
  rewrite <- (Nat.add_1_r (n + n * (n + 1) + sum_n2 n)).
  Search (_ * (_ + _)).
  rewrite (Nat.mul_add_distr_l 6).
  rewrite (Nat.mul_add_distr_l 6).
  rewrite IHn.

  (* You should do this manually as well - just a preview on how one does this after going through the exercises *)
  Require Import Lia.
  lia.

这也表明您可以向引理者提出争论，以更好地控制它们的应用位置。

如果稍后使用COQ，则只需使用LIA策略（用于线性整数算术），该策略也可以立即释放您的目标（没有上述重写）。但是您应该练习并手动做。

您可能想查看手册中的搜索功能（ https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq：cmd.search ）。

This looks like a tutorial exercise, so this depends a bit on which lemmas you have. Coq has a search function to help you find lemmas.

Below is an example on how you would solve this using standard library lemmas - which might not work for you, e.g. early SF chapters have their own nat definitions and lemmas. But the Search function should show you equivalent lemmas you have.

Require Import PeanoNat.

Axiom sum_n2: nat->nat.

Example E1 : forall (n : nat) (IHn : 6 * sum_n2 n = n * (n + 1) * (2 * n + 1)),
  6 * S (n + n * (n + 1) + sum_n2 n) = (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1).
Proof.
  intros.
  Search (S _) (_ + 1).
  rewrite <- (Nat.add_1_r (n + n * (n + 1) + sum_n2 n)).
  Search (_ * (_ + _)).
  rewrite (Nat.mul_add_distr_l 6).
  rewrite (Nat.mul_add_distr_l 6).
  rewrite IHn.

  (* You should do this manually as well - just a preview on how one does this after going through the exercises *)
  Require Import Lia.
  lia.

This also shows that you can give arguments to lemmas to better control where they are applied.

If you use Coq later, you will just use the lia tactic (for Linear Integer Arithmetic) which can also discharge your goal right away (without the above rewrites). But you should practice and do it manual.

You might want to have a look at the Search function in the manual (https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Search).

回复收藏 0 原文

~没有更多了~