変数のインスタンスを見つけることができません

Question

コンテキスト：私はSoftware Foundationsの演習で取り組んでいます。しかし、

negb (evenb (S n')) = evenb (S (S n')) 

私はrewrite -> neg_moveをステップ実行してみてください：

Theorem neg_move : forall x y : bool, 
    x = negb y -> negb x = y. 
Proof. Admitted. 

Theorem evenb_n__oddb_Sn : forall n : nat, 
    evenb n = negb (evenb (S n)). 
Proof. 
    intros n. induction n as [| n']. 
    Case "n = 0". 
    simpl. reflexivity. 
    Case "n = S n'". 
    rewrite -> neg_move. 

は、最後の行の前に、私のサブゴールはこれです：

evenb (S n') = negb (evenb (S (S n'))) 

そして私はこれにそれを変換したいですこのエラーが発生します。

Error: Unable to find an instance for the variable y.

これは本当にシンプルだと確信していますが、何が間違っていますか？ （私が完全に間違っていない限り、evenb_n__oddb_Snを解決するために何かを放棄しないでください）。

Answer 1

danportinが述べたように、Coqは、yをインスタンス化する方法がわからないことを伝えています。実際にrewrite -> neg_moveを実行するときには、negb xの一部をyに置き換えてください。今、yはCoqがここで使うはずのものは何ですか？それを理解することはできません。

一つの選択肢は、書き換え時に明示的にyをインスタンス化することです：

rewrite -> neg_move with (y:=some_term)

これは、書き換えを行い、施設を証明するように要求されます、ここでは、フォームx = negb some_termのサブゴールを追加します。

別のオプションは、書き換え時にneg_moveを特化することである。

rewrite -> (neg_move _ _ H)

ここHはタイプsome_x = negb some_yの用語でなければなりません。 xとyのパラメータがneg_moveの2つのワイルドカードをそれぞれHからsome_xとsome_yと推測できるので、私は2つのワイルドカードを入れました。 Coqは目標のnegb some_xの出現をsome_yで書き直そうとします。 しかし、あなたが最初

は（私が与えた最初のオプションは、あなたが rewrite -> (neg_move _ some_term)と同等でなければならないことに注意してください）...いくつかの追加負担であるかもしれない、あなたの仮説では、この H用語を取得する必要があります

別のオプションはerewrite -> negb_moveですこれは?xと?yのようなインスタンス化されていない変数を追加し、書き直しを試みます。 (evenb (S (S n'))) = negb ?yのような前提を証明する必要がありますし、うまくいけば、このサブゴールを解決する過程で、Coqは最初から何があったのかを見つけます（いくつかの制限がありますが、いくつかの問題が発生する可能性がありますCoqは、?yが何である必要があるかを考えずに目標を解決します）。（B

========== 
evenb (S n') = negb (evenb (S (S n'))) 

symmetry.

========== 
negb (evenb (S (S n'))) = evenb (S n') 

apply neg_move.

========== 
evenb (S (S n')) = negb (evenb (S n')) 

そして、それはあなたが望んでいたものです：

---

しかし、あなたの特定の問題のために、それは非常に簡単ですあなたが気にしているなら別のsymmetry.をしてください）。