Coq：haskell 的 Replicate 函数的强规范

Question

我在理解 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 -> list A -> Prop :=
| len_nil : RelLength  0 nil
| len_cons : forall l x n, RelLength n l -> RelLength (S n) (x::l) .


Theorem len_corr : forall (A:Type) (l:list A),  {n | RelLength n l}.
Proof.
 …
Qed.

Recursive Extraction len_corr.

用于证明的函数必须直接使用列表“recursor”（这就是修复点不会出现的原因——它隐藏在 list_rect 中）。

所以你不需要写函数本身，只需要写关系，因为函数将由证明来定义。”

知道了这一点，我如何将其应用于复制功能案例？