Nats vs. Lists 的关联性证明答案

【问题标题】：Associativity proof on Nats vs. ListsNats vs. Lists 的关联性证明
【发布时间】：2018-02-27 19:15:41
【问题描述】：

我正在比较 Nats 和 Lists 的关联性证明。

Lists 上的证明是归纳法

lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
by (induct xs) auto

但是，关于 Nats 的证明是

lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
by (rule add_assoc)

为什么我不需要对nat_add_assoc 证明进行归纳？是因为自然数上发生了一些自动化吗？

【问题讨论】：

【解决方案1】：

nat 上的关联性证明也是通过归纳法完成的。

在Nat.thy你可以找到

instantiation nat :: comm_monoid_diff

这是伊莎贝尔的说法nat 具有类型类comm_monoid_diff。下面的定义和引理表明，自然数是加法下的可交换幺半群，并且还有减法。

在这个区块中你可以找到证明：

instance proof
  fix n m q :: nat
  show "(n + m) + q = n + (m + q)" by (induct n) simp_all

然后实例化给我们在nat 上的引理add_assoc。

【讨论】：

好吧，这仍然不能解释如何在不明确使用归纳策略的情况下完成相同的证明。
当你写rule add_assoc时，这意味着你只需应用定理add_assoc。基本上，您使用的是已在其他地方证明的定理。正如 ammbauer 指出的那样，那个证明是通过归纳完成的，所以你当然不必再次进行归纳。事实上，我不确定为什么nat_add_assoc 甚至存在，因为它实际上与add_assoc 专用于nat 相同。可能是历史原因。
哦，谢谢！这说得通！它掩盖了名字！我虽然它正在对要证明的定理进行递归调用！
没有阴影，因为nat_add_assoc 和add_assoc 不一样。