Yêu cầu, nhập, yêu cầu nhập

Question

Trong Coq, sự khác nhau giữa ... là gì?

• Yêu cầu X.
• nhập X.
• Yêu cầu nhập khẩu X.

tôi đã cơ bản thuộc lòng một số mô hình chung. Tôi thường thấy mã bằng cách sử dụng Yêu cầu nhập X. Sau đó, có Import ListNotation. Và tôi chỉ nhận thấy nó cũng có thể viết chỉ yêu cầu X. sự khác biệt là gì? Một số ví dụ thực tế sẽ được đánh giá cao.

Answer 1

Require tải thư viện trong khi Import đưa định nghĩa của nó vào phạm vi. Require Import thực hiện cả hai. Nếu bạn chỉ có thư viện được tải, bạn sẽ cần phải tham khảo tên đầy đủ. Coq cho phép các mô-đun cấp cao nhất tương ứng với các tệp để xác định các mô-đun; này đã được nhập khẩu riêng biệt để mang lại tất cả các định nghĩa của họ vào phạm vi, và họ không thể Require d - đó là những gì đang xảy ra với ListNotations:

(* List is not loaded by default *) 
Fail Check List.map. 

(* the full name is technically Coq.Lists.List *) 
Require List. 

(* note that lists are actually defined in Coq.Init.Datatypes which is 
imported by default, so [list] is unqualified and the [x::xs] notation is 
already defined *) 
Print List.map. 
(* 
List.map = 
fun (A B : Type) (f : A -> B) => 
fix map (l : list A) : list B := 
    match l with 
    | nil => nil 
    | (a :: t)%list => (f a :: map t)%list 
    end 
    : forall A B : Type, (A -> B) -> list A -> list B 
*) 

(* bring everything in List into scope *) 
Import List. 
(* this includes the ListNotations submodule *) 
Import ListNotations. 

(* note that now list notations are available, and the list notation scope is 
open (from importing List) *) 
Print List.map. 
(* 
map = 
fun (A B : Type) (f : A -> B) => 
fix map (l : list A) : list B := 
    match l with 
    | [] => [] 
    | a :: t => f a :: map t 
    end 
    : forall A B : Type, (A -> B) -> list A -> list B 
*) 

Lưu ý có một số quirks với cách Coq xử lý mô-đun, đặc biệt so với các ngôn ngữ khác:

• Coq không yêu cầu đường dẫn đầy đủ đến mô-đun, chỉ hậu tố rõ ràng. Thật vậy, tôi hiếm khi nhìn thấy đường dẫn nhập đầy đủ, ngay cả với các mô-đun thư viện chuẩn.
• Không thể sử dụng ký hiệu trừ khi nhập mô-đun và không giống như hầu hết các đối tượng không có cách nào để tham chiếu đến ký hiệu, đủ điều kiện hoặc cách khác.
• Nhập mô-đun có thể có tác dụng phụ, ví dụ như thay đổi phạm vi diễn giải chú thích hoặc tùy chọn cài đặt nếu bạn sử dụng Global Set trong mô-đun đang được nhập.
• Nhập khẩu khá hạn chế (đặc biệt là so với Haskell) - không có cách nào để đổi tên mô-đun tại thời điểm nhập hoặc nhập một cách có chọn lọc một số định nghĩa.