主页 / coding / 问题 / 77426613
Accepted
Random Citizen
Asked: 2023-11-05 23:52:47 +0800 CST

为什么“专门化”在证明中不是无效策略？

  • 772

在软件基础书籍（已存档）中specialize，引入了该策略作为简化假设的一种方法。

我不明白，为什么这是证明中的有效步骤。

提供的示例增加了我的困惑：

Theorem specialize_example: forall n,
     (forall m, m*n = 0)
  -> n = 0.
Proof.
  intros n H.
  specialize H with (m := 1).
  simpl in H.
  rewrite add_comm in H.
  simpl in H.
  apply H. Qed.

当我用 替换假设时(forall m, m*n = 0) -> n = 0.，1*n = 0 -> n = 0.我发现我们现在正在成功证明n=0新假设。

我不明白为什么这被接受作为原始定理的证明forall n, (forall m, m*n = 0) -> n = 0.。我们现在不是在继续证明一个新定理吗forall n, 1*n = 0 -> n = 0.？

新定理的证明如何推广为原定理的有效证明？

文中将该specialize策略描述为“本质上只是和的组合”assertapply。也许使用and而
不是将这个（或使用的另一个示例）的证明脚本重写specialize为另一个证明脚本可能会清除问题。assertapplyspecialize

coq

2 个回答

  1. Best Answer

    我们现在不是在继续证明一个新定理吗forall n, 1*n = 0 -> n = 0？

    事实上，这就是你首先要证明的。但随后您可以回到原来的定理并查看起点(forall m, m*n = 0)。如果这个陈述是正确的，那么它就意味着1*n = 0你的新定理意味着什么n=0。因此证明了原定理

    (forall m, m*n = 0) -> 1*n = 0 -> n=0

    （我不知道 coq 语言，所以如果上面的行在语法上不正确，它只是在数学意义上表示A=>B=>C）。去掉两个箭头之间的中间部分就是原来的定理。

    你的新定理比原来的定理更强，因为它需要更少的假设来得出相同的结论。

    • 2

  2. [我宁愿将其作为评论发布，但我仍然太新了。]

    我不愿意回答你问题的第一部分，以免破坏练习：逻辑基础尤其是一个旅程和一个进展，而不是食谱纲要，以及该练习的智力组成部分，而不是破坏它，我认为是至关重要的。

    至于你对这种变换的有效性的怀疑，也许我明白你的意思：如果我们要证明一个对所有 n 都成立的定理，那么我们怎么能只对某些 n 证明它呢？但现在请注意，我们上面专门讨论的并不是 n，那么如果您还认为应用假设而不是目标是如何工作的......

    • 0

相关问题