coq (或一般)中的定理可以在不使用先前证明的引理的情况下被证明吗？
由于coq中的证明是简单的高度复杂的函数，可以通过各种方式中的任何一种来构建，因此似乎有必要为每个既不涉及先前证明的定理也不涉及assert语句的定理提供coq证明。
例如，在没有任何引理的情况下，证明自然数加法的交换性是很简单的，即使有引理可以让它变得更简单：
Theorem plus_comm' :
forall n m : nat, n + m = m + n.
Proof.
induction n.
intro m. simpl. induction m.
reflexivity.
simpl. rewrite <- IHm. reflexivity.
intro m. simpl. rewrite -> IHn. induction m.
reflexivity.
simpl. rewrite <- IHm. reflexivity.
Qed.但是，当我尝试为乘法的交换性做同样的事情时，我不可避免地会遇到这样的情况，我需要一个关于加法的事实。
Theorem mult_comm' :
forall n m : nat, n * m = m * n.
Proof.
induction n.
intro m. simpl. induction m.
reflexivity.
simpl. apply IHm.
intro m. simpl. rewrite -> IHn. induction m.
reflexivity.
simpl. rewrite <- IHm. f_equal.
(* left with goal:
m + (n + m * n) = n + (m + m * n)
*)
Abort.为什么？
回答 2
Stack Overflow用户
发布于 2016-03-16 20:18:39
Coq的逻辑享有cut-elimination，这意味着任何涉及中间引理(即带有beta-redexes的λ项)的证明都可以通过归约算法转换为直接证明(即范式中的项)。
然而，这可能是以指数爆炸为代价的:例如，减少power 2 100 (在应用于2和100的函数power中，将产生一个大小为2 ^ 100的项，从一个大小为1 + 2 + 100的项开始)。
如果您正在尝试编写校对搜索算法，您可能希望了解一下聚焦。考虑到你似乎想要专注于归纳证明，你可能也想看看Boyer &Moore的证明者。
Stack Overflow用户
发布于 2016-03-16 10:21:31
当然，有一个没有引理或断言的证明，只要有这样一个证明来证明你的目标，m + (n + m * n) = n + (m + m * n)。这里有一个，尽管它不是很清楚：
remember (m*n) as o.
clear.
generalize dependent o.
generalize dependent m.
induction n; simpl; try reflexivity.
simpl.
intros m o.
rewrite <- (IHn m o).
remember (n+o) as p.
clear.
generalize dependent p.
induction m; simpl; try reflexivity.
intros p; rewrite (IHm p).
reflexivity.为什么你“需要”一个引理的问题可以从另一个角度来看：
看看这个关于multiplication.Part的交换性的证明，它证明了关于加法的一个有趣的事实，你可以在不改变值的情况下将括号打乱。这似乎在其他证据中显示了一点！也许这一事实将是一个有用的包装与一个名称。然后我们可以一遍又一遍地参考它，读者就会明白我们在说什么，它不需要每次都需要新的证明。
让我们将辅助事实称为“引理”。我们将移动它的过程称为“重构”。
https://stackoverflow.com/questions/36025161
复制相似问题
腾讯云开发者
