破壞應用謂詞函數的結果

Question

我是Coq的新手，對於破壞策略有個疑問。假設我有一個count功能纔是最重要的自然數列表的給定的自然數中出現的次數：

Fixpoint count (v : nat) (xs : natlist) : nat := 
    match xs with 
    | nil => 0 
    | h :: t => 
     match beq_nat h v with 
     | true => 1 + count v xs 
     | false => count v xs 
     end 
    end. 

我想證明下面的定理：

Theorem count_cons : forall (n y : nat) (xs : natlist), 
    count n (y :: xs) = count n xs + count n [y]. 

如果我證明了n = 0的類似定理，我可以簡單地將y破壞爲0或S y'。對於一般情況，我想要做的是破壞（beq_nat n y）爲真或假，但我似乎無法讓它起作用 - 我錯過了一些Coq語法。

任何想法？

Answer 1

您的代碼被打破

Fixpoint count (v : nat) (xs : natlist) : nat := 
match xs with 
    | nil => 0 
    | h :: t => 
    match beq_nat h v with 
    | true => 1 + count v xs (*will not compile since "count v xs" is not simply recursive*) 
    | false => count v xs 
    end 
end. 

你可能是指

Fixpoint count (v : nat) (xs : natlist) : nat := 
match xs with 
    | nil => 0 
    | h :: t => 
    match beq_nat h v with 
    | true => 1 + count v t 
    | false => count v t 
    end 
end. 

使用destruct然後讓你的解決方案一個完美的方法。但是，你需要記住幾件事

• destruct是句法的，也就是說它取代了表達在你的目標/假設中的術語。所以，你通常首先需要像simpl（在這裏工作）或unfold。
• 條款的順序很重要。 destruct (beq_nat n y)與destruct (beq_nat y n)不一樣。在這種情況下，你想第二個

一般問題是destruct是愚蠢的，所以你必須做自己的智慧。

不管怎麼說，開始你的證明

intros n y xs. simpl. destruct (beq_nat y n). 

一切都會好的。