我如何证明 Coq 中的两个 Fibonacci 实现相等？
How do I prove that two Fibonacci implementations are equal in Coq?
我有两个斐波那契实现，如下所示，我想证明它们在功能上是等价的。
我已经证明了自然数的性质，但是这个练习需要另一种我想不通的方法。
我使用的教科书介绍了以下 Coq 语法，因此应该可以使用这种表示法来证明相等性：
<definition> ::= <keyword> <identifier> : <statement> <proof>
<keyword> ::= Proposition | Lemma | Theorem | Corollary
<statement> ::= {<quantifier>,}* <expression>
<quantifier> ::= forall {<identifier>}+ : <type>
| forall {({<identifier>}+ : <type>)}+
<proof> ::= Proof. {<tactic>.}* <end-of-proof>
<end-of-proof> ::= Qed. | Admitted. | Abort.
下面是两个实现：
Fixpoint fib_v1 (n : nat) : nat :=
match n with
| 0 => O
| S n' => match n' with
| O => 1
| S n'' => (fib_v1 n') + (fib_v1 n'')
end
end.
Fixpoint visit_fib_v2 (n a1 a2 : nat) : nat :=
match n with
| 0 => a1
| S n' => visit_fib_v2 n' a2 (a1 + a2)
end.
很明显，这些函数在基本情况下计算相同的值 n = 0，但归纳情况要难得多？
我已经尝试证明以下引理，但我被困在归纳案例中：
Lemma about_visit_fib_v2 :
forall i j : nat,
visit_fib_v2 i (fib_v1 (S j)) ((fib_v1 j) + (fib_v1 (S j))) = (fib_v1 (add_v1 i (S j))).
Proof.
induction i as [| i' IHi'].
intro j.
rewrite -> (unfold_visit_fib_v2_0 (fib_v1 (S j)) ((fib_v1 j) + (fib_v1 (S j)))).
rewrite -> (add_v1_0_n (S j)).
reflexivity.
intro j.
rewrite -> (unfold_visit_fib_v2_S i' (fib_v1 (S j)) ((fib_v1 j) + (fib_v1 (S j)))).
Admitted.
其中：
Fixpoint add_v1 (i j : nat) : nat :=
match i with
| O => j
| S i' => S (add_v1 i' j)
end.
注意事项：在接下来的内容中，我将尝试展示此类证明的主要思想，因此我不会拘泥于 Coq 的某些子集，也不会手动进行算术运算。相反，我将使用一些证明自动化，即。 ring 策略。但是，请随时提出其他问题，以便您可以将证明转换成适合您目的的形式。
我认为从一些概括开始会更容易：
Require Import Arith. (* for `ring` tactic *)
Lemma fib_v1_eq_fib2_generalized n : forall a0 a1,
visit_fib_v2 (S n) a0 a1 = a0 * fib_v1 n + a1 * fib_v1 (S n).
Proof.
induction n; intros a0 a1.
- simpl; ring.
- change (visit_fib_v2 (S (S n)) a0 a1) with
(visit_fib_v2 (S n) a1 (a0 + a1)).
rewrite IHn. simpl; ring.
Qed.
如果使用 ring 不符合您的需要，您可以使用 Arith 模块的引理执行多个 rewrite 步骤。
现在，让我们实现目标：
Definition fib_v2 n := visit_fib_v2 n 0 1.
Lemma fib_v1_eq_fib2 n :
fib_v1 n = fib_v2 n.
Proof.
destruct n.
- reflexivity.
- unfold fib_v2. rewrite fib_v1_eq_fib2_generalized.
ring.
Qed.
安东的证明非常漂亮，比我的好，但无论如何它可能会有用。
我没有提出泛化引理，而是加强了归纳假设。
说原来的目标是Q n。然后我用
改变了目标
cut (Q n /\ Q (S n))
来自
Q n
至
Q n /\ Q (S n)
这个新目标微不足道地暗示了原来的目标，但是有了它归纳假设变得更强，所以可以重写更多。
IHn : Q n /\ Q (S n)
=========================
Q (S n) /\ Q (S (S n))
软件基础中对偶数进行证明的一章解释了这个想法。
因为命题通常很长，所以我制定了一个Ltac策略来命名又长又乱的术语。
Ltac nameit Q :=
match goal with [ _:_ |- ?P ?n] => let X := fresh Q in remember P as X end.
Require Import Ring Arith.
（顺便说一句，我将 vistit_fib_v2 重命名为 fib_v2。）
我需要关于 fib_v2.
一步的引理
Lemma fib_v2_lemma: forall n a b, fib_v2 (S (S n)) a b = fib_v2 (S n) a b + fib_v2 n a b.
intro n.
pattern n.
nameit Q.
cut (Q n /\ Q (S n)).
tauto. (* Q n /\ Q (S n) -> Q n *)
induction n.
split; subst; simpl; intros; ring. (* Q 0 /\ Q 1 *)
split; try tauto. (* Q (S n) *)
subst Q. (* Q (S (S n)) *)
destruct IHn as [H1 H2].
assert (L1: forall n a b, fib_v2 (S n) a b = fib_v2 n b (a+b)) by reflexivity.
congruence.
Qed.
congruence 策略处理来自一堆 A = B 假设和重写的目标。
证明定理非常相似。
Theorem fib_v1_fib_v2 : forall n, fib_v1 n = fib_v2 n 0 1.
intro n.
pattern n.
nameit Q.
cut (Q n /\ Q (S n)).
tauto. (* Q n /\ Q (S n) -> Q n *)
induction n.
split; subst; simpl; intros; ring. (* Q 0 /\ Q 1 *)
split; try tauto. (* Q (S n) *)
subst Q. (* Q (S (S n)) *)
destruct IHn as [H1 H2].
assert (fib_v1 (S (S n)) = fib_v1 (S n) + fib_v1 n) by reflexivity.
assert (fib_v2 (S (S n)) 0 1 = fib_v2 (S n) 0 1 + fib_v2 n 0 1) by
(pose fib_v2_lemma; congruence).
congruence.
Qed.
所有的样板代码都可以放在一个策略中，但我不想对 Ltac 发疯，因为那不是问题所在。
@larsr 的 启发了这个替代答案。
首先，让我们定义fib_v2:
Require Import Coq.Arith.Arith.
Definition fib_v2 n := visit_fib_v2 n 0 1.
然后，我们将需要一个引理，这与@larsr 的回答中的 fib_v2_lemma 相同。我将其包含在这里是为了保持一致性并展示替代证据。
Lemma visit_fib_v2_main_property n: forall a0 a1,
visit_fib_v2 (S (S n)) a0 a1 =
visit_fib_v2 (S n) a0 a1 + visit_fib_v2 n a0 a1.
Proof.
induction n; intros a0 a1; auto with arith.
change (visit_fib_v2 (S (S (S n))) a0 a1) with
(visit_fib_v2 (S (S n)) a1 (a0 + a1)).
apply IHn.
Qed.
正如 larsr 在评论中所建议的那样，visit_fib_v2_main_property 引理也可以通过以下令人印象深刻的一句话来证明：
now induction n; firstorder.
由于斐波那契数列中数字的性质，定义替代归纳法则非常方便：
Lemma pair_induction (P : nat -> Prop) :
P 0 ->
P 1 ->
(forall n, P n -> P (S n) -> P (S (S n))) ->
forall n, P n.
Proof.
intros H0 H1 Hstep n.
enough (P n /\ P (S n)) by tauto.
induction n; intuition.
Qed.
pair_induction 原理基本上是说，如果我们可以为 0 和 1 证明一些 属性 P 并且如果对于每个自然数 k > 1，我们可以在P (k - 1)和P (k - 2)成立的假设下证明P k成立，那么我们可以证明forall n, P n.
利用我们自定义的归纳原理，得到如下证明：
Lemma fib_v1_eq_fib2 n :
fib_v1 n = fib_v2 n.
Proof.
induction n using pair_induction.
- reflexivity.
- reflexivity.
- unfold fib_v2.
rewrite visit_fib_v2_main_property.
simpl; auto.
Qed.
此证明脚本仅显示证明结构。解释证明的想法可能很有用。
Require Import Ring Arith Psatz. (* Psatz required by firstorder *)
Theorem fibfib: forall n, fib_v2 n 0 1 = fib_v1 n.
Proof with (intros; simpl in *; ring || firstorder).
assert (H: forall n a0 a1, fib_v2 (S n) a0 a1 = a0 * (fib_v1 n) + a1 * (fib_v1 (S n))).
{ induction n... rewrite IHn; destruct n... }
destruct n; try rewrite H...
Qed.
有一个非常强大的库——math-comp written in the Ssreflect formal proof language that is in its turn based on Coq. In this answer I present a version that uses its facilities. It's just a simplified piece of this开发。所有功劳归于原作者。
让我们做一些导入和两个函数的定义，math-comp (ssreflect) 样式：
From mathcomp
Require Import ssreflect ssrnat ssrfun eqtype ssrbool.
Fixpoint fib_rec (n : nat) {struct n} : nat :=
if n is n1.+1 then
if n1 is n2.+1 then fib_rec n1 + fib_rec n2
else 1
else 0.
Fixpoint fib_iter (a b n : nat) {struct n} : nat :=
if n is n1.+1 then
if n1 is n2.+1
then fib_iter b (b + a) n1
else b
else a.
表达基本 属性 斐波那契数列的辅助引理：
Lemma fib_iter_property : forall n a b,
fib_iter a b n.+2 = fib_iter a b n.+1 + fib_iter a b n.
Proof.
case=>//; elim => [//|n IHn] a b; apply: IHn.
Qed.
现在，让我们来解决两个实现的等价问题。
这里的主要思想是，将以下证明与截至撰写本文时已提出的其他证明区分开来，我们执行
有点 complete induction，使用 elim: n {-2}n (leqnn n)。这给了我们以下（强）归纳假设：
IHn : forall n0 : nat, n0 <= n -> fib_rec n0 = fib_iter 0 1 n0
这里是主要引理及其证明：
Lemma fib_rec_eq_fib_iter : fib_rec =1 fib_iter 0 1.
Proof.
move=>n; elim: n {-2}n (leqnn n)=> [n|n IHn].
by rewrite leqn0; move/eqP=>->.
case=>//; case=>// n0; rewrite ltnS=> ltn0n.
rewrite fib_iter_property.
by rewrite <- (IHn _ ltn0n), <- (IHn _ (ltnW ltn0n)).
Qed.
这是另一个答案，类似于 ，但这个答案使用 "vanilla" Coq。
首先，我们需要一些导入、附加定义和一些辅助引理：
Require Import Coq.Arith.Arith.
Definition fib_v2 n := visit_fib_v2 n 0 1.
Lemma visit_fib_v2_property n: forall a0 a1,
visit_fib_v2 (S (S n)) a0 a1 =
visit_fib_v2 (S n) a0 a1 + visit_fib_v2 n a0 a1.
Proof. now induction n; firstorder. Qed.
Lemma fib_v2_property n:
fib_v2 (S (S n)) = fib_v2 (S n) + fib_v2 n.
Proof. apply visit_fib_v2_property. Qed.
为了证明主要引理，我们将对具有 < 关系的自然数使用标准的有根据的归纳法 lt_wf_ind 原理（a.k.a。完全归纳法）：
这次我们只需要证明一个子目标，因为完全归纳的 n = 0 情况总是空洞地为真。不出所料，我们的归纳假设如下所示：
IH : forall m : nat, m < n -> fib_v1 m = fib_v2 m
证明如下：
Lemma fib_v1_eq_fib2 n :
fib_v1 n = fib_v2 n.
Proof.
pattern n; apply lt_wf_ind; clear n; intros n IH.
do 2 (destruct n; trivial).
rewrite fib_v2_property.
rewrite <- !IH; auto.
Qed.
我有两个斐波那契实现，如下所示，我想证明它们在功能上是等价的。
我已经证明了自然数的性质，但是这个练习需要另一种我想不通的方法。
我使用的教科书介绍了以下 Coq 语法，因此应该可以使用这种表示法来证明相等性：
<definition> ::= <keyword> <identifier> : <statement> <proof>
<keyword> ::= Proposition | Lemma | Theorem | Corollary
<statement> ::= {<quantifier>,}* <expression>
<quantifier> ::= forall {<identifier>}+ : <type>
| forall {({<identifier>}+ : <type>)}+
<proof> ::= Proof. {<tactic>.}* <end-of-proof>
<end-of-proof> ::= Qed. | Admitted. | Abort.
下面是两个实现：
Fixpoint fib_v1 (n : nat) : nat :=
match n with
| 0 => O
| S n' => match n' with
| O => 1
| S n'' => (fib_v1 n') + (fib_v1 n'')
end
end.
Fixpoint visit_fib_v2 (n a1 a2 : nat) : nat :=
match n with
| 0 => a1
| S n' => visit_fib_v2 n' a2 (a1 + a2)
end.
很明显，这些函数在基本情况下计算相同的值 n = 0，但归纳情况要难得多？
我已经尝试证明以下引理，但我被困在归纳案例中：
Lemma about_visit_fib_v2 :
forall i j : nat,
visit_fib_v2 i (fib_v1 (S j)) ((fib_v1 j) + (fib_v1 (S j))) = (fib_v1 (add_v1 i (S j))).
Proof.
induction i as [| i' IHi'].
intro j.
rewrite -> (unfold_visit_fib_v2_0 (fib_v1 (S j)) ((fib_v1 j) + (fib_v1 (S j)))).
rewrite -> (add_v1_0_n (S j)).
reflexivity.
intro j.
rewrite -> (unfold_visit_fib_v2_S i' (fib_v1 (S j)) ((fib_v1 j) + (fib_v1 (S j)))).
Admitted.
其中：
Fixpoint add_v1 (i j : nat) : nat :=
match i with
| O => j
| S i' => S (add_v1 i' j)
end.
注意事项：在接下来的内容中，我将尝试展示此类证明的主要思想，因此我不会拘泥于 Coq 的某些子集，也不会手动进行算术运算。相反，我将使用一些证明自动化，即。 ring 策略。但是，请随时提出其他问题，以便您可以将证明转换成适合您目的的形式。
我认为从一些概括开始会更容易：
Require Import Arith. (* for `ring` tactic *)
Lemma fib_v1_eq_fib2_generalized n : forall a0 a1,
visit_fib_v2 (S n) a0 a1 = a0 * fib_v1 n + a1 * fib_v1 (S n).
Proof.
induction n; intros a0 a1.
- simpl; ring.
- change (visit_fib_v2 (S (S n)) a0 a1) with
(visit_fib_v2 (S n) a1 (a0 + a1)).
rewrite IHn. simpl; ring.
Qed.
如果使用 ring 不符合您的需要，您可以使用 Arith 模块的引理执行多个 rewrite 步骤。
现在，让我们实现目标：
Definition fib_v2 n := visit_fib_v2 n 0 1.
Lemma fib_v1_eq_fib2 n :
fib_v1 n = fib_v2 n.
Proof.
destruct n.
- reflexivity.
- unfold fib_v2. rewrite fib_v1_eq_fib2_generalized.
ring.
Qed.
安东的证明非常漂亮，比我的好，但无论如何它可能会有用。
我没有提出泛化引理，而是加强了归纳假设。
说原来的目标是Q n。然后我用
cut (Q n /\ Q (S n))
来自
Q n
至
Q n /\ Q (S n)
这个新目标微不足道地暗示了原来的目标，但是有了它归纳假设变得更强，所以可以重写更多。
IHn : Q n /\ Q (S n)
=========================
Q (S n) /\ Q (S (S n))
软件基础中对偶数进行证明的一章解释了这个想法。
因为命题通常很长，所以我制定了一个Ltac策略来命名又长又乱的术语。
Ltac nameit Q :=
match goal with [ _:_ |- ?P ?n] => let X := fresh Q in remember P as X end.
Require Import Ring Arith.
（顺便说一句，我将 vistit_fib_v2 重命名为 fib_v2。）
我需要关于 fib_v2.
Lemma fib_v2_lemma: forall n a b, fib_v2 (S (S n)) a b = fib_v2 (S n) a b + fib_v2 n a b.
intro n.
pattern n.
nameit Q.
cut (Q n /\ Q (S n)).
tauto. (* Q n /\ Q (S n) -> Q n *)
induction n.
split; subst; simpl; intros; ring. (* Q 0 /\ Q 1 *)
split; try tauto. (* Q (S n) *)
subst Q. (* Q (S (S n)) *)
destruct IHn as [H1 H2].
assert (L1: forall n a b, fib_v2 (S n) a b = fib_v2 n b (a+b)) by reflexivity.
congruence.
Qed.
congruence 策略处理来自一堆 A = B 假设和重写的目标。
证明定理非常相似。
Theorem fib_v1_fib_v2 : forall n, fib_v1 n = fib_v2 n 0 1.
intro n.
pattern n.
nameit Q.
cut (Q n /\ Q (S n)).
tauto. (* Q n /\ Q (S n) -> Q n *)
induction n.
split; subst; simpl; intros; ring. (* Q 0 /\ Q 1 *)
split; try tauto. (* Q (S n) *)
subst Q. (* Q (S (S n)) *)
destruct IHn as [H1 H2].
assert (fib_v1 (S (S n)) = fib_v1 (S n) + fib_v1 n) by reflexivity.
assert (fib_v2 (S (S n)) 0 1 = fib_v2 (S n) 0 1 + fib_v2 n 0 1) by
(pose fib_v2_lemma; congruence).
congruence.
Qed.
所有的样板代码都可以放在一个策略中，但我不想对 Ltac 发疯，因为那不是问题所在。
@larsr 的
首先，让我们定义fib_v2:
Require Import Coq.Arith.Arith.
Definition fib_v2 n := visit_fib_v2 n 0 1.
然后，我们将需要一个引理，这与@larsr 的回答中的 fib_v2_lemma 相同。我将其包含在这里是为了保持一致性并展示替代证据。
Lemma visit_fib_v2_main_property n: forall a0 a1,
visit_fib_v2 (S (S n)) a0 a1 =
visit_fib_v2 (S n) a0 a1 + visit_fib_v2 n a0 a1.
Proof.
induction n; intros a0 a1; auto with arith.
change (visit_fib_v2 (S (S (S n))) a0 a1) with
(visit_fib_v2 (S (S n)) a1 (a0 + a1)).
apply IHn.
Qed.
正如 larsr 在评论中所建议的那样，visit_fib_v2_main_property 引理也可以通过以下令人印象深刻的一句话来证明：
now induction n; firstorder.
由于斐波那契数列中数字的性质，定义替代归纳法则非常方便：
Lemma pair_induction (P : nat -> Prop) :
P 0 ->
P 1 ->
(forall n, P n -> P (S n) -> P (S (S n))) ->
forall n, P n.
Proof.
intros H0 H1 Hstep n.
enough (P n /\ P (S n)) by tauto.
induction n; intuition.
Qed.
pair_induction 原理基本上是说，如果我们可以为 0 和 1 证明一些 属性 P 并且如果对于每个自然数 k > 1，我们可以在P (k - 1)和P (k - 2)成立的假设下证明P k成立，那么我们可以证明forall n, P n.
利用我们自定义的归纳原理，得到如下证明：
Lemma fib_v1_eq_fib2 n :
fib_v1 n = fib_v2 n.
Proof.
induction n using pair_induction.
- reflexivity.
- reflexivity.
- unfold fib_v2.
rewrite visit_fib_v2_main_property.
simpl; auto.
Qed.
此证明脚本仅显示证明结构。解释证明的想法可能很有用。
Require Import Ring Arith Psatz. (* Psatz required by firstorder *)
Theorem fibfib: forall n, fib_v2 n 0 1 = fib_v1 n.
Proof with (intros; simpl in *; ring || firstorder).
assert (H: forall n a0 a1, fib_v2 (S n) a0 a1 = a0 * (fib_v1 n) + a1 * (fib_v1 (S n))).
{ induction n... rewrite IHn; destruct n... }
destruct n; try rewrite H...
Qed.
有一个非常强大的库——math-comp written in the Ssreflect formal proof language that is in its turn based on Coq. In this answer I present a version that uses its facilities. It's just a simplified piece of this开发。所有功劳归于原作者。
让我们做一些导入和两个函数的定义，math-comp (ssreflect) 样式：
From mathcomp
Require Import ssreflect ssrnat ssrfun eqtype ssrbool.
Fixpoint fib_rec (n : nat) {struct n} : nat :=
if n is n1.+1 then
if n1 is n2.+1 then fib_rec n1 + fib_rec n2
else 1
else 0.
Fixpoint fib_iter (a b n : nat) {struct n} : nat :=
if n is n1.+1 then
if n1 is n2.+1
then fib_iter b (b + a) n1
else b
else a.
表达基本 属性 斐波那契数列的辅助引理：
Lemma fib_iter_property : forall n a b,
fib_iter a b n.+2 = fib_iter a b n.+1 + fib_iter a b n.
Proof.
case=>//; elim => [//|n IHn] a b; apply: IHn.
Qed.
现在，让我们来解决两个实现的等价问题。
这里的主要思想是，将以下证明与截至撰写本文时已提出的其他证明区分开来，我们执行
有点 complete induction，使用 elim: n {-2}n (leqnn n)。这给了我们以下（强）归纳假设：
IHn : forall n0 : nat, n0 <= n -> fib_rec n0 = fib_iter 0 1 n0
这里是主要引理及其证明：
Lemma fib_rec_eq_fib_iter : fib_rec =1 fib_iter 0 1.
Proof.
move=>n; elim: n {-2}n (leqnn n)=> [n|n IHn].
by rewrite leqn0; move/eqP=>->.
case=>//; case=>// n0; rewrite ltnS=> ltn0n.
rewrite fib_iter_property.
by rewrite <- (IHn _ ltn0n), <- (IHn _ (ltnW ltn0n)).
Qed.
这是另一个答案，类似于
首先，我们需要一些导入、附加定义和一些辅助引理：
Require Import Coq.Arith.Arith.
Definition fib_v2 n := visit_fib_v2 n 0 1.
Lemma visit_fib_v2_property n: forall a0 a1,
visit_fib_v2 (S (S n)) a0 a1 =
visit_fib_v2 (S n) a0 a1 + visit_fib_v2 n a0 a1.
Proof. now induction n; firstorder. Qed.
Lemma fib_v2_property n:
fib_v2 (S (S n)) = fib_v2 (S n) + fib_v2 n.
Proof. apply visit_fib_v2_property. Qed.
为了证明主要引理，我们将对具有 < 关系的自然数使用标准的有根据的归纳法 lt_wf_ind 原理（a.k.a。完全归纳法）：
这次我们只需要证明一个子目标，因为完全归纳的 n = 0 情况总是空洞地为真。不出所料，我们的归纳假设如下所示：
IH : forall m : nat, m < n -> fib_v1 m = fib_v2 m
证明如下：
Lemma fib_v1_eq_fib2 n :
fib_v1 n = fib_v2 n.
Proof.
pattern n; apply lt_wf_ind; clear n; intros n IH.
do 2 (destruct n; trivial).
rewrite fib_v2_property.
rewrite <- !IH; auto.
Qed.