我如何证明两个斐波纳契实现在Coq中是相同的？ [英] How do I prove that two Fibonacci implementations are equal in Coq?

问题描述

我有两个斐波那契实现，见下面，我想证明在功能上是等价的。

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

我使用的教科书引入了Coq的以下语法，因此应该可以使用以下符号证明相等性：

 < definition> :: =< keyword> <标识符GT; ：< statement> <防爆> 
 
< keyword> :: =命题|引理|定理|推论
 
<语句> :: = {<量词> ;, *<表达> 
 
<量词> :: = forall {< identifier>} +：< type> 
 | forall {（{< identifier>} +：< type>}} + 
 
< proof> :: =证明。 {<策略>。*<结束>> 
 
<结束标准> :: = Qed。 |录取。 |中止。 
  

以下是两个实现：

  Fixpoint fib_v1（n：nat）：nat：= 
匹配n与
 | 0 => O 
 | S n'=>匹配n'与
 | O => 1 
 | S n''=> （fib_v1 n'）+（fib_v1 n''）
 end 
 end。 
 
固定点visit_fib_v2（n a1 a2：nat）：nat：= 
匹配n与
 | 0 => a1 
 | S n'=> visit_fib_v2 n'a2（a1 + a2）
结束。 
  

很显然，这些函数为基本情况计算相同的值 n = 0 ，但归纳情况更难？

我试过证明以下引理，但我被困在归纳例如：
$ b $ pre $ 引理about_visit_fib_v2：
forall ij：nat，
visit_fib_v2 i（fib_v1（S j） ）（（fib_v1j）+（fib_v1（Sj）））=（fib_v1（add_v1i（Sj）））。
证明。
归纳我as [|我'IHI']。

介绍j。
重写 - > （unfold_visit_fib_v2_0（fib_v1（S j））（（fib_v1j）+（fib_v1（Sj））））。
重写 - > （add_v1_0_n（S j））。
反身性。

介绍j。
重写 - > （unfold_visit_fib_v2_S i'（fib_v1（S j））（（fib_v1 j）+（fib_v1（S j））））。

被允许。


其中：

  Fixpoint add_v1（ij：nat）：nat：= 
与
匹配| O => j 
 | S i'=> S（add_v1 i'j）
结束。 
  

解决方案

警告：试图展示这种证明的主要思想，所以我不会坚持Coq的一些子集，而且我也不会手动进行算术。相反，我会使用一些证明自动化，即。 戒指策略。然而，随意提出其他问题，所以你可以将证明转换成适合你的目的。

我认为从一些概括开始比较容易：

 需要进口阿里。 （* for`ring` tactic *）
 
引理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）。 
证明。 
归纳n;介绍a0 a1。 
  - 简单;环。 
  - 用
（visit_fib_v2（S n）a1（a0 + a1））改变（visit_fib_v2（S（S n））a0 a1）。 
重写IHn。 SIMPL;环。 
 Qed。 
  

如果使用 ring 不适合您您可以使用 Arith 模块的引用来执行多个重写步骤。

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

$ p $ 定义fib_v2 n：= visit_fib_v2 n 0 1.

引理fib_v1_eq_fib2 n：
fib_v1 n = fib_v2 n。
证明。
破坏n。
- 反身性。
- 展开fib_v2。重写fib_v1_eq_fib2_generalized。
戒指。
Qed。


I've two Fibonacci implementations, seen below, that I want to prove are functionally equivalent.

I've already proved properties about natural numbers, but this exercise requires another approach that I cannot figure out.

The textbook I'm using have introduced the following syntax of Coq, so it should be possible to prove equality using this notation:

<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.

Here are the two implementations:

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.

It is pretty obvious that these functions compute the same value for the base case n = 0, but the induction case is much harder?

I've tried proving the following Lemma, but I'm stuck in induction case:

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.

解决方案

A note of warning: in what follows I'll to try to show the main idea of such a proof, so I'm not going to stick to some subset of Coq and I won't do arithmetic manually. Instead I'll use some proof automation, viz. the ring tactic. However, feel free to ask additional questions, so you could convert the proof to somewhat that would suit your purposes.

I think it's easier to start with some generalization:

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.

If using ring doesn't suit your needs, you can perform multiple rewrite steps using the lemmas of the Arith module.

Now, let's get to our goal:

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.

这篇关于我如何证明两个斐波纳契实现在Coq中是相同的？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！