如何证明 Coq 中的两个斐波那契实现是相等的？答案

【问题标题】：How do I prove that two Fibonacci implementations are equal in Coq?如何证明 Coq 中的两个斐波那契实现是相等的？
【发布时间】：2016-11-13 07:15:50
【问题描述】：

我有两个斐波那契实现，如下所示，我想证明它们在功能上是等效的。

我已经证明了自然数的性质，但是这个练习需要另一种我想不通的方法。

我正在使用的教科书介绍了 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.

【问题讨论】：

请注意，您的语法中引用了未定义的产生式<tactic>。你知道任何战术吗？如果你还没有写过证明，这个证明在 Coq 中是不明显的……
我只知道关于加法的自然数策略。
标准库中+的定义与add_v1相同。

标签： functional-programming fibonacci coq

【解决方案1】：

警告说明：在下文中，我将尝试展示这种证明的主要思想，因此我不会坚持使用 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.

【讨论】：

是否可以仅使用“重写”和“应用”等简单操作来提供基本证明？我自己的想法是以下辅助引理：“forall i j : nat, visit_fib_v2 i (fib_v1 j) (fib_v1 (S j)) = (fib_v1 i + j)。”，但我被卡住了:-(
见this gist——你只需要intros、rewrite、reflexivity，也许是apply和几个辅助引理（它们可以完成simpl的工作）。跨度>
谢谢你，安东！您能否就如何证明我的“about_visit_fib_v2”给出提示，我已将其添加到我的问题中。我被困在感应案例中。如果我能让这个引理起作用，我已经完成了自己的证明！
我认为引理更难证明，因为它涉及斐波那契数的一些不那么琐碎的性质。
感谢您的支持@AntonTrunov。最后，让我问一下：证明“S n = n + 1”之类的东西的预定义 Coq 程序是否也有？在这里，我想将“S n”转换为“n + 1”，反之亦然，但我不知道如何做到这一点。我通常将这些事实陈述为“承认”。对于我围绕“+”的包装程序。

【解决方案2】：

@larsr 的 answer 启发了这个替代答案。

首先，我们定义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 在 cmets 中所建议的那样，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 原理基本上是说，如果我们可以证明P 对0 和1 的某些属性，并且如果对于每个自然数k > 1，我们可以在假设@ 的情况下证明P k 成立987654336@和P (k - 2)成立，那么我们可以证明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.

【讨论】：

我知道引理应该有一个更短的证明！ :-) 非常好！
引理的证明通过now induction n; firstorder.!
我建议使用enough 而不是（老式的）cut。另外，在这种特殊情况下，您可以将cut 及其证明替换为enough (P n /\ P (S n)) by tauto.
对。好吧，这是一个自动化程度较低的版本（通过介绍模式显式破坏并手动使用 exact）：enough (P n /\ P (S n)) as (H,_) by exact H. 无论如何，我发现这种风格（使用 enough 而不是 cut 和 @987654349 @当它的证明足够简单时）更具可读性。
您也可以这样做：enough (P n /\ P (S n)) as (?,_) by assumption. 但我认为这不是您要问的。您也可以使用?H 介绍模式来生成一个新名称，但它不如? 更好，因为您不确定它是什么。

【解决方案3】：

Anton 的证明非常漂亮，比我的要好，但无论如何它可能有用。

我没有提出泛化引理，而是加强了归纳假设。

假设最初的目标是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 发疯，因为这不是问题所在。

【讨论】：

【解决方案4】：

此证明脚本仅显示证明结构。解释证明的想法可能很有用。

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.

【讨论】：

我一定犯了一些复制/粘贴错误（我也遇到了错误）。希望它现在有效！

【解决方案5】：

有一个非常强大的库——math-comp 用 Ssreflect 形式证明语言编写，它又基于 Coq。在这个答案中，我提出了一个使用其设施的版本。这只是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.

【讨论】：

【解决方案6】：

这是另一个答案，类似于one using mathcomp，但这个答案使用“香草”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 原理和< 关系（也称为完全归纳）：

这一次我们只需要证明一个子目标，因为完全归纳的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.

【讨论】：