10

コンテキスト: 私はSoftware Foundationsの演習に取り組んでいます。

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')))

そして、私はそれを次のように変換したいと思います:

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

ただし、ステップスルーしようとするとrewrite -> neg_move、次のエラーが発生します。

エラー: 変数 y のインスタンスが見つかりません。

これは本当に簡単だと思いますが、何が間違っているのでしょうか? evenb_n__oddb_Sn（私が完全に間違っている場合を除き、解決のために何も与えないでください）。

4

1 に答える 1

10

danportin が述べたように、Coq は をインスタンス化する方法を知らないと言っていますy。実際、そうするときは、一部を arewrite -> neg_moveに置き換えるように要求します。では、ここで Coq は何を使用すればよいのでしょうか。それを理解することはできません。negb xyy

1 つのオプションは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パラメータに 2 つのワイルドカードを入れました。これは、Coq がそれぞれ とであるとneg_move推測できるためです。Coq は、ゴール内の の出現を で書き換えようとします。しかし、最初にこの用語を仮説に組み込む必要があります。これは、追加の負担になる可能性があります...Hsome_xsome_ynegb some_xsome_yH

(最初に指定したオプションは と同等であることに注意してくださいrewrite -> (neg_move _ some_term))

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

ただし、特定の問題については、非常に簡単です。

==========
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.気にするなら別のことをしてください）。

于 2012-01-16T09:16:50.380 に答える