Không thể tìm thấy một phiên bản cho biến

Question

Bối cảnh: Tôi đang thực hiện các bài tập trong 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. 

Trước khi dòng cuối cùng, subgoal của tôi là thế này:

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

Và tôi muốn biến nó thành này:

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

Khi tôi cố gắng bước qua rewrite -> neg_move, tuy nhiên, nó tạo ra lỗi này:

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

Tôi chắc chắn điều này thực sự đơn giản, nhưng tôi đang làm gì sai? (Xin vui lòng không cung cấp bất cứ điều gì để giải quyết evenb_n__oddb_Sn, trừ khi tôi đang làm nó hoàn toàn sai).

Answer 1

Như danportin đã đề cập, Coq đang cho bạn biết rằng nó không biết cách khởi tạo y. Thật vậy, khi bạn làm rewrite -> neg_move, bạn yêu cầu nó thay thế một số negb x bằng một số y. Bây giờ, những gì y là Coq nghĩa vụ phải sử dụng ở đây? Nó không thể hình dung ra được.

Một lựa chọn là để nhanh chóng y một cách rõ ràng khi viết lại:

rewrite -> neg_move with (y:=some_term)

này sẽ thực hiện việc viết lại và yêu cầu bạn chứng minh các cơ sở, ở đây nó sẽ thêm một subgoal dạng x = negb some_term.

lựa chọn khác là chuyên neg_move khi viết lại:

rewrite -> (neg_move _ _ H)

Đây H phải là một thuật ngữ kiểu some_x = negb some_y. Tôi đặt hai ký tự đại diện cho các thông số x và y của neg_move vì Coq có thể suy ra chúng từ H tương ứng là some_x và some_y. Coq sau đó sẽ cố gắng viết lại một sự xuất hiện của negb some_x trong mục tiêu của bạn với some_y. Nhưng trước tiên bạn cần phải nhận được hạn H này trong giả thuyết của bạn, mà có thể có một số gánh nặng thêm ...

(Lưu ý rằng tùy chọn đầu tiên tôi đưa bạn sẽ có tương đương với rewrite -> (neg_move _ some_term))

lựa chọn khác là erewrite -> negb_move , sẽ thêm các biến không được xác nhận sẽ trông giống như ?x và ?y và cố gắng viết lại. Sau đó bạn sẽ phải chứng minh tiền đề, trông giống như (evenb (S (S n'))) = negb ?y, và hy vọng trong quá trình giải quyết subgoal này, Coq sẽ tìm ra những gì ?y nên có được từ đầu (có một số hạn chế mặc dù, và một số vấn đề có thể phát sinh là Coq giải quyết mục tiêu mà không tìm ra những gì ?y phải).

---

Tuy nhiên, đối với vấn đề cụ thể của bạn, nó là khá dễ dàng hơn:

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

Và đó là những gì bạn muốn (b ackwards, hãy làm symmetry. nếu bạn quan tâm).