我如何證明兩個斐波納契實現在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.

來源

2016-11-13 Shuzheng

通知你引用一個未定義的生產''。你知道任何有關戰術的事情嗎？如果你還沒有寫出任何證據，這個證明在Coq中不會很明顯...... –

我只知道有關加法的自然數的策略。 – Shuzheng

標準庫中'+'的定義與'add_v1'相同。 –

的注意事項警告：在下面，我就來試圖展示這種證明的主要思想，所以我不會堅持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.

來源

2016-11-13 09:44:20

是否可以僅使用簡單操作（如「重寫」和「應用」）來提供基本證明？我自己的想法是下面的助手引理：「forall ij：nat， visit_fib_v2 i（fib_v1 j）（fib_v1（S j））=（fib_v1 i + j）。」，但我卡住了:-( – Shuzheng

請參閱[this gist]（https://gist.github.com/anton-trunov/84b63d4ca28c2698ed87b5c680974506） - 你只需要'intros'，'rewrite'，'reflexivity'，也許'apply'和幾個助手引理（這樣做工作簡單「） –

謝謝安東！您是否也提供了關於如何證明我的」about_visit_fib_v2「的提示，我已將其添加到了我的問題中。使這個引理工作，我做了我自己的證明！ – Shuzheng

安東的證據是很漂亮，比我的好，但也可能是有用的，反正。

我沒有提出泛化引理，而是加強了歸納假設。

說出最初的目標是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))

這個想法是在軟件基礎，其中一個確實證明了偶數章節中所說明。

因爲propostion往往很長，我做了一個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，因爲這不是問題是什麼。

來源

2016-11-14 15:46:37 larsr

@ larsr的answer啓發了這個替代答案。

首先，讓我們定義fib_v2：

Require Import Coq.Arith.Arith. 

Definition fib_v2 n := visit_fib_v2 n 0 1.

然後，我們將需要一個引理，這是相同@ larsr的回答fib_v2_lemma。我將它包括在內以保持一致性並展示另一種證據。

now induction n; firstorder.

，因爲數字的斐波納契數列的性質，這是非常：

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引理也可以通過以下令人印象深刻的一個班輪證明方便定義替代感應原理：

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假設P (k - 1)和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.

來源

2016-11-14 18:08:27

我知道引理應該有一個較短的證明！：-）非常好！ – larsr

引理的證明經過'現在的歸納n; firstorder.'！ – larsr

真的很酷！我將你的代碼合併到答案中。獎勵！ :) –

這個證明腳本只顯示了防爆結構。解釋證明的想法可能很有用。

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.

來源

2016-11-14 18:10:35 larsr

我一定做了一些複製/粘貼錯誤（我也有錯誤）。希望它現在可行！ – larsr

一切正常！這真的很棒！ –

有一個非常強大的庫 - math-comp寫的是反過來基於勒柯克的Ssreflect形式證明語言。在這個答案中，我提出了一個使用它的設施的版本。這只是一個簡化的this開發。所有功勞都歸原作者所有。

讓我們做我們的兩個功能部分進口和定義，數學-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.

來源

2016-11-15 10:06:04

這裏是另一種答案，類似於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.

來源

2016-11-18 10:55:59

我如何證明兩個斐波納契實現在Coq中是相等的？

回答

相關問題