述語関数を適用した結果を破壊する

Question

私はCoqを初めて使い、破壊戦術について簡単に質問します。私は次の定理を証明したいと思います

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. 

：：私は自然数のリスト内の指定された自然数の出現回数をカウントcount機能を持っていると仮定し

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）をtrueまたはfalseに破棄することができますが、それを働かせることはできません.Coq構文の一部が欠落しています。

アイデア？あなたはおそらくdestructを使用し

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. 

を意味

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. 

が壊れているが、あなたのソリューションを取得するのに最適な方法です。しかし、あなたはそれがあなたの目標/仮定で表現されている用語を置き換えることがあり、

• destructが構文である心の中でいくつかのことを維持する必要があります。したがって、通常はsimpl（ここで動作）またはunfoldのようなものが最初に必要です。
• 用語の順序が重要です。 destruct (beq_nat n y)はdestruct (beq_nat y n)と同じではありません。この場合、2番目のものが必要です

一般的に問題はdestructがダムなので、自分でスマートを行う必要があります。

とにかく、あなたの証明

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

開始し、すべてが良いだろう。