2012-01-16 15 views
9

コンテキスト:私は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を解決するために何かを放棄しないでください)。

+0

「変数* y *のインスタンスを見つけることができません」というフレーズは、Coqが* neg_move *型の変数* y *を代入する値を見つけることができないことを意味します。条件の前件を含む* neg_move *のパラメータを明示的にインスタンス化することでこの問題を解決できます(インスタンス化されていない場合はサブゴールとして生成されます)。しかし、条件文は一般に*適用されることを意図しています*。実際、* neg_move *はあなたの帰納仮説に適用してより有用な仮説を得ることができます。 – danportin

答えて

9

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の用語でなければなりません。 xyのパラメータがneg_moveの2つのワイルドカードをそれぞれHからsome_xsome_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.をしてください)。

関連する問題