Coq：證明使用歸納的兩個因子函數的相等性

Question

我想證明使用歸納法的Coq中的兩個因子函數是等價的。

基本案例n = 0很容易，但是，歸納案例更加複雜。我明白了，如果我可以將(visit_fac_v2 n' (n * a))重寫爲n * (visit_fac_v2 n' a)，那我就完成了。但是，將這個想法轉化爲Coq會給我帶來麻煩。

如何在Coq上證明這一點？

Fixpoint fac_v1 (n : nat) : nat := 
    match n with 
    | 0 => 1 
    | S n' => n * (fac_v1 n') 
    end. 

Fixpoint visit_fac_v2 (n a : nat) : nat := 
    match n with 
    | 0 => a 
    | S n' => visit_fac_v2 n' (n * a) 
    end. 

Definition fac_v2 (n : nat) : nat := 
    visit_fac_v2 n 1. 

Proposition equivalence_of_fac_v1_and_fac_v2 : 
    forall n : nat, 
    fac_v1 n = fac_v2 n. 
Proof. 
Abort. 

Answer 1

一在證明直接函數和基於累加器的等價函數相等時，典型的做法是聲明一個更強的不變量，這對於累加器可能持有的任何值都應該是真實的。

然後，您可以將它專門化爲該函數的調用值，從而獲得您感興趣的語句，作爲更一般語句的推論。

一般在這裏的講話如下：

Theorem general_equivalence_of_fac_v1_and_fac_v2 : 
    forall n a : nat, 
    a * fac_v1 n = visit_fac_v2 n a. 

及其證明是相當簡單的（你必須要小心，確保因爲你想歸納假設爲有效的是induction來intro a前任何a）：

Proof. 
intros n; induction n; intro a. 
- simpl ; ring. 
- simpl ; rewrite <- IHn ; ring. 
Qed. 

你的主張是更一般的定理的一個直接後果。

Answer 2

在感應的情況下，你可以申請歸納假設和簡化的目標：

visit_fac_v2 n 1 + n * visit_fac_v2 n 1 = visit_fac_v2 n (S n) 

爲了證明這一點，你可以用下面的引理：

Lemma visit_fac_v2_extract: 
    forall n a : nat, 
    visit_fac_v2 n a = a * visit_fac_v2 n 1.