问题描述
我想通过归纳证明在Coq中两个阶乘函数是等效的。
I want to prove that two factorial functions are equivalent in Coq using induction.
基本情况 n = 0 很容易，但是，归纳情况更加复杂。我知道，如果我可以将（visit_fac_v2 n'（n * a））重写为 n *（visit_fac_v2 n'a），我会做的。但是，将此想法转换为Coq会给我带来麻烦。
The base case n = 0 is easy, however, the induction case is more complicated. I see, that if I could rewrite (visit_fac_v2 n' (n * a)) to n * (visit_fac_v2 n' a), I would be done. However, translating this idea into Coq causes me troubles.
如何在Coq中证明这一点？
How would one go about proving this in Coq?
Fixpoint fac_v1 (n : nat) : nat :=
match n with
| 0 => 1
| S n' => n * (fac_v1 n')
end.
Fixpoint visit_fac_v2 (n a : nat) : nat :=
match n with
| 0 => a
| S n' => visit_fac_v2 n' (n * a)
end.
Definition fac_v2 (n : nat) : nat :=
visit_fac_v2 n 1.
Proposition equivalence_of_fac_v1_and_fac_v2 :
forall n : nat,
fac_v1 n = fac_v2 n.
Proof.
Abort.
推荐答案
在证明直接-样式函数及其基于累加器的等效项相等，是为了说明一个更强的不变性，对于累加器可能持有的任何值，它应该都是正确的。
A typical thing to do when proving that a direct-style function and its accumulator-based equivalent are equal is to state a stronger invariant which ought to be true for any value the accumulator may hold.
然后，您可以将其专门化为函数调用的值，从而获得您感兴趣的语句作为更通用语句的推论。
You can then specialise it to the value the function is called with thus obtaining the statement you are interested in as a corollary of the more general one.
此处的一般语句如下：
Theorem general_equivalence_of_fac_v1_and_fac_v2 :
forall n a : nat,
a * fac_v1 n = visit_fac_v2 n a.
其证明非常简单（您必须小心并确保归纳在简介之前，因为您希望归纳假设对 any 有效a ）：
And its proof is fairly straightforward (you do have to be careful and ensure that induction comes before intro a because you want the induction hypothesis to be valid for any a):
Proof. intros n; induction n; intro a. - simpl ; ring. - simpl ; rewrite <- IHn ; ring. Qed.
您的命题是这个更笼统的定理的直接结果。
Your proposition is a direct consequence of this more general theorem.
这篇关于Coq：使用归纳证明两个阶乘函数相等的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！