6

私は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またはSy'に単純に破棄できます。一般的なケースでは、私がやりたいのは（beq_nat ny）をtrueまたはfalseに破棄することですが、それを機能させることができないようです。Coq構文の一部が欠落しています。

何か案は？

4

1 に答える 1

5

あなたのコードは壊れています

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)。この場合、2番目のものが必要です

一般的に問題はdestruct馬鹿げているので、自分で賢くする必要があります。

とにかく、あなたの証明を始めてください

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

そして、すべてが良いでしょう。

于 2011-12-27T03:58:37.723 に答える