如何证明 Coq 中的两个 Fibonacci 实现相等？

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

我已经证明了自然数的性质，但是这个练习需要另一种我无法弄清楚的方法。

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

Where:

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不适合您的需求，您可以执行多个rewrite使用引理的步骤Arith module.

现在，让我们实现我们的目标：

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.