需要,导入,需要导入

Question

在Coq,......之间的区别是什么？

• 需要X.
• 导入X.
• 需要导入X.

我基本上记住了一些常见的模式.我通常使用Require Import X来查看代码.然后是Import ListNotation.我只是注意到它也可以只写需要X.有什么区别？一些实际的例子将不胜感激.

Answer 1

Require加载库,同时Import将其定义放入范围.Require Import做到了.如果您只加载了库,则需要引用完全限定的名称.Coq允许与文件对应的顶级模块定义模块; 这些必须单独导入,以将所有定义纳入范围,并且它们不能成为Required - 这是正在发生的事情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相比) - 在导入时无法重命名模块,或者有选择地导入某些定义.