1

我目前在 coq 的一个项目中工作，我需要使用nat -> nat. 所以基本上我会有一个定义，它接受一个list (nat -> nat)和一个命题f : nat -> nat作为参数，目标是检索f给定列表中的索引。

我所做的是我实现了一个通过列表并将每个元素f与相等性进行比较的固定点=。但是我发现这是不正确的，并且此类类型的相等性是无法确定的。

有谁知道解决这个问题的替代方法？或者更简单的方法来检索f列表中的索引？

4

2 回答 2

1

我不知道为什么你会调用f : nat -> nat一个命题而不是一个函数，但无论如何，除非你对 的内容有更多的假设，否则l我认为你的问题没有解决方案。

正如您所指出的，功能的平等通常是不可判定的。您只能对它们执行有限数量的观察（例如调用f 0和检查结果）。如果您知道您的功能足够不同，那么检查它们是否同意一些（精心选择的）特定值可能就足够了，否则我看不到出路。

也许是您过度简化了手头的问题/任务，而您遇到的真正问题确实有解决方案。目前，该问题与 Coq 无关。

于 2021-11-23T15:47:44.660 回答
0

作为记录，如果一般问题无法确定（正如 Théo 解释的那样），您似乎不太可能真的想要/需要这个。但是，为了回答这个问题：

如果您确定您的输入列表中恰好出现了一次您要查找的函数（其中函数由它们的逐点相等标识），那么列表中的所有其他函数在某些时候f都不同意。f换句话说，对于其他每个函数，都存在一个k : nat这样的g k ≠ f k。

由于nat是可枚举的，整数比较是可判定的，并且列表是有限的，所以有一个终止算法来解决这个问题。在命令式伪代码中：

input: a function f : nat → nat
input: a list of functions [ g[0] ; g[1] ; … ; g[n−1] ] : list (nat → nat)
start:
  candidates := { 0 ; 1 ; … ; n−1 } (set of cardinal n)
  k := 0
  while true do:
    if card candidates < 2 then:
      return the only candidate
    for all i in candidates do:
      if f k ≠ g[i] k then:
        candidates := candidates \ { i }
    k := k+1
end

如果列表中有多次出现f，则算法永远不会终止（这些出现永远是候选者）。如果出现 0 次或 1 次，则算法终止，但无法确定剩余候选者是否完全等于f。

因此，上述假设对于终止和纠正是必要的。这在 Coq 中可能不容易实现，尤其是因为您必须说服 Coq 终止。祝你好运，如果这真的是你想要的。;-)

于 2021-11-23T19:40:27.860 回答