我在理解 Coq 中强规范和弱规范之间的区别时遇到了一些麻烦。例如，如果我想使用强规范方式编写复制函数（给定一个数字 n 和一个值 x，它会创建一个长度为 n 的列表，其中所有元素都等于 x），我将如何做到这一点? 显然我必须编写函数的归纳“版本”，但如何编写？
Haskell 中的定义：
myReplicate :: Int -> a -> [a]
myReplicate 0 _ = []
myReplicate n x | n > 0 = x:myReplicate (n-1) x
| otherwise = []
弱规范的定义：
用弱规范定义这些函数，然后添加伴随引理。例如，我们定义一个函数 f : A->B 并证明形式为 ? x:A, Rx ( fx )，其中 R 是对函数的预期输入/输出行为进行编码的关系。
强规范的定义：
给出函数的强规范：该函数的类型直接声明输入是类型 A 的值 x，输出是类型 B 的值 v 和 v 满足Rxv的证明的组合。这种规范通常依赖于依赖类型。
编辑：我收到老师的回复，显然我必须做类似的事情，但对于复制案例：
“例如，如果我们想从其规范中提取一个计算列表长度的函数，我们可以定义一个关系 RelLength，该关系建立预期输入和输出之间的关系，然后证明它。像这样：
Inductive RelLength (A:Type) : nat …