模块错误类型Coq不同

Question

我很难弄清楚如何编写此代码。

例如，我有一个签名A，一个仿函数C需要a: A作为参数，以能够使用C，我定义了一个模块B实现签名A

Require Import String. 
Module Type A. 
    Parameter toto : string -> nat. 
End A. 

Module C (Import a : A). 
... 
End C. 

Module B <: A. 
     Definition toto (s: string) := foo s. 
End B. (* COQ error *) 

和支持我有类型foo: string -> string list-> nat.

然后在End B.，我有一个错误的Coq说：signature components for label toto do not match: types differ.

或者另一种方式：

Module B. 
Definition too (s : string) := foo s. 
End B. 

Module Export D := C B. 

我会得到同样的错误在D

我理解这个问题，因为我没有提供的toto的定义string list说法。

所以我的问题是我不知道如何在这种情况下提供参数string list。

在我的真实代码中，我使用的是Section和Record而不是Module。

Record A : Type := mkA { too : string -> nat}. 

然后我打开一个Section

Section B. 
Variable l: string list. 
Definition too (s: string) := foo s l. 
Definition A := mkA too. 
End B. 

能否请你帮我写或理解，我怎样才能正确地写仿函数B模块？有没有办法可以在模块中定义/声明变量string list？在Coq中定义后，我会将其解压到OCaml。

Answer 1

那么你总是可以做到这一点：

Require Import String. 

Parameter foo: string -> list string -> nat. 

Module Type A. 

    Parameter toto : string -> nat. 

End A. 

Module B <: A. 

    Variable (* or Parameter, or Axiom *) ls : list string. 

    Definition toto (s: string) := foo s ls. 

End B. 

但让我认识到，只有让LS公理......另一种解决方案是推迟LS的提供：

ModuleType HasListString. 

    Parameter ls : list string. 

End HasListString. 

Module B(LS: HasListString) : A. 

    Definition toto (s: string) := foo s LS.ls. 

End B. 

这可能不是你需要的。没有上下文，很难给你提供更好的建议。