两个命题之间的相等nat -> nat

Question

我目前在coq的一个项目中工作，在那里我需要处理nat -> nat的列表。因此，基本上我将有一个以list (nat -> nat)和命题f : nat -> nat作为参数的定义，目标是检索给定列表中的f的索引。

我所做的是实现了一个固定点，遍历列表，并使用相等的=将每个元素与f进行比较。但我发现这是不正确的，这种类型的等价性是无法决定的。

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

Answer 1

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

正如您所指出的，函数的相等性在一般情况下是不可判定的。您只能对它们执行有限数量的观察(如调用f 0并检查结果)。如果您知道您的函数足够不同，那么检查它们是否在一些(精心选择的)特定值上是否一致就足够了，但除此之外，我看不到解决办法。

也许是因为你把手头的问题/任务过于简单化了，而你真正遇到的问题确实有解决方案。目前，这个问题与Coq无关。

Answer 2

根据记录，如果一般的问题是无法确定的(正如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终止。如果这真的是你想要的，祝你好运。;-)