文脈に帰納的な項の値を加えるCoctactact

Question

私はこの問題の簡単な例を与えるだけで、私は証明したいと思うと思いますforall f : nat -> bool, exists i j, i<>j /\ f i = f j.明白なことはf 0, f 1, f 2,の値をチェックし、それに応じて進んでください。しかし、単にdestruct (f 0)と言うと、f 0は下位には出現しないため、Coqは目標を変更しません。そのため、私は現在、f 0の価値について何の情報も求めていません。理想的には、Coqが証人をコンテキストに追加して、それを追跡できるようにしたいと思います。

私がこれらの問題を回避するために行ってきたことは、補助的な補題bool_destruct : forall b : bool, b = false \/ b = trueを証明することでした。さて、私がdestruct (bool_destruct (f 0))と言うなら、Coqは希望するHを文脈に追加します。当然ながら、これはそれぞれの誘導型に対してこのような補題を証明しなければならないときには面倒です。したがって、私は、これらの状況を処理する素晴らしい戦術があるのだろうかと思っています。

Answer 1

すでに破壊戦術は、あなたが望むものをサポートしています。

destruct (f 0) eqn:f_is0. 

bool_destructあなたは、例えば、それがために同様のアイデアプラスcaseのパターン一般化機能を作るほど悪くはない使用してのあなたのアイデアmath-compでは、カスタムの破壊ビューを提供するために戦術が使用されます。