6
Trong coq, bằng cách nào đó nó có thể áp dụng một bổ đề hoặc giả thuyết cho một biểu hiện con của mục tiêu hiện tại? Ví dụ tôi muốn áp dụng thực tế là cộng là giao hoán để hoán đổi 3 và 4 trong ví dụ này.Làm thế nào để sử dụng viết lại trên một biểu hiện con của mục tiêu hiện tại
Require Import Coq.Arith.Plus.
Inductive foobar : nat -> Prop :=
| foob : forall n:nat, foobar n.
Goal foob (3 + 4) = foob (4 + 3).
Proof.
apply plus_comm. (* or maybe rewrite plus_comm *)
cho:
Error: Impossible to unify "?199 + ?200 = ?200 + ?199" with
"foob (3 + 4) = foob (4 + 3)".
Làm thế nào tôi có thể nói Coq nơi chính xác trong mục tiêu này để áp dụng plus_comm?
Nó hoạt động khi tôi làm như sau, đó là những gì tôi thực sự muốn chứng minh ở nơi đầu tiên. Mục tiêu foobar (3 + 4) = foobar (4 + 3). Bằng chứng. viết lại plus_comm. phản xạ. Qed. Tôi đoán viết lại không hoạt động trên các giá trị, chỉ trên các loại. –
'rewrite' hoạt động trên cả hai (thực tế là các loại trong Coq ;-). Vấn đề chính ở đây là 'foob (3 + 4)' có kiểu 'foobar (3 + 4)' và 'foob (4 + 3)' có kiểu 'foobar (4 + 3)'. Coq có thể kiểm tra rằng cả hai đều bằng nhau (do đó sự bình đẳng được đánh máy tốt), nhưng 'viết lại' sử dụng một dạng trung gian mà nó không phải là trường hợp, do đó thông báo lỗi khó hiểu bạn nhận được với' rewrite (plus_comm 3 4) '. – Virgile
Thông thường, bạn sẽ có thể sử dụng 'mẫu' (http://coq.inria.fr/refman/Reference-Manual011.html#pattern) cho các hành động cục bộ ở đâu đó trong thuật ngữ. Tuy nhiên, điều này không thành công cho cùng một lý do @Virgile được đề cập. Nếu điều đó có thể xảy ra, bạn cũng có thể chuyển sang loại bình đẳng 'hoàn chỉnh hơn' tạm thời (ví dụ: 'JMeq'), thực hiện công cụ ở đó và sau đó quay lại. (Tôi thích nghĩ về nó như là 'phức tạp số'-tương tự về bình đẳng.) – nobody