無法找到變量的實例

上下文：我正在練習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，但是，它會產生此錯誤：

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

我確定這很簡單，但是我做錯了什麼？（請不要給任何東西解決evenb_n__oddb_Sn，除非我完全錯誤）。

來源

2012-01-16 Dan Burton

短語「無法找到變量* y *的實例」意味着Coq無法找到替換* neg_move *類型中的變量* y *的值。你可以通過明確地實例化* neg_move *的參數來解決這個問題，包括條件的前件（如果沒有實例化，它將作爲子目標生成）。但是，條件陳述一般意味着*應用*;事實上，* neg_move *可以應用於你的歸納假設，以獲得更有用的假設。 – danportin 2012-01-16 05:31:17

正如danportin提到的，Coq告訴你它不知道如何實例化y。事實上，當你做rewrite -> neg_move時，你會要求它用y替換negb x。現在，Coq應該在這裏使用什麼y？它無法弄清楚。

一種選擇是在改寫實例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設置了兩個通配符，因爲Coq能夠從H分別推斷它們分別爲some_x和some_y。然後Coq將嘗試用some_y重寫您的目標0123'的發生。但是，你首先需要在你的假設得到這個H來看，這可能是一些額外的負擔......

（請注意，我給了第一個選項，你應該相當於rewrite -> (neg_move _ some_term)）

另一種選擇是erewrite -> negb_move ，它會添加看起來像?x和?y的無實際變量，並嘗試進行重寫。然後你必須證明這個前提，它看起來像(evenb (S (S n'))) = negb ?y，並且希望在解決這個子目標的過程中，Coq會發現從一開始應該是什麼?y（雖然有一些限制，並且可能會出現一些問題， Coq解決了這個目標，但沒有弄清楚?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'))

這就是你想要的（B ackwards，如果你在意，另做symmetry.）。

來源

2012-01-16 09:16:50 Ptival

無法找到變量的實例

回答

相關問題