import - 需要，导入，需要导入

Question

在 Coq 中，... 和有什么区别？

Require X.

Import X.

Require Import X.

我已经基本记住了一些常见的模式。我通常看到使用 Require Import X 的代码.然后是 Import ListNotation .我刚刚注意到也可以只写Require X .有什么不同？一些实际的例子将不胜感激。

Answer 1

Require加载一个库，而 Import将其定义纳入范围。 Require Import两者都做。如果您只加载了库，则需要引用完全限定的名称。 Coq 允许文件对应的顶层模块定义模块；这些必须单独导入才能将它们的所有定义纳入范围，并且它们不能是 Require d - 这就是 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
*)

请注意，Coq 处理模块的方式有一些怪癖，尤其是与其他语言相比:

Coq 不需要模块的完整路径，只需要一个明确的后缀。事实上，我很少看到完整的导入路径，即使是标准库模块也是如此。

除非通过导入模块，否则无法使用符号，并且与大多数对象不同，无法引用完全限定或其他方式的符号。

导入模块可能会产生副作用，例如，如果您使用 Global Set，则会更改符号解释范围或设置选项在要导入的模块中。

导入是相当有限的(尤其是与 Haskell 相比) - 无法在导入时重命名模块，或有选择地导入某些定义。