Equality between two propositions nat -> nat

Question

I am currently working in a project in coq where I need to work with lists of nat -> nat. So basically I will have a definition that takes a list (nat -> nat) and a proposition f : nat -> nat as parameters and the goal is to retrieve the index of f in the given list.

What I did is that I implemented a fixpoint going through the list and comparing each elements to f with equality =. But I found out that this was not correct and equality at such types are undecidable.

Does anyone know an alternative to solve this ? Or an easier way to retrieve the index of f in the list ?

Answer 1

I am not sure why you would call f : nat -> nat a proposition and not a function but in any case, unless you have more hypotheses on the contents of l, I don't think there is a solution to your problem.

As you point out, equality of functions is not decidable in general. You can only perform a finite amount of observations on them (like calling f 0 and examining the result). If you know your functions to be different enough then it might be enough to check whether they agree on a few (carefully chosen) specific values but otherwise I do not see a way out.

Perhaps is it that you oversimplified your problem/task at hand and the real problem you have does have a solution. At the moment, the problem is not related to Coq.

Answer 2

For the record, it seems unlikely that you really want/need this, provided that the general problem is undecidable (as Théo explained). However, for the sake of answering the question:

If you know for sure that your input list has exactly one occurrence of the function f you are looking for (where functions are identified by their pointwise equality), then all other functions of the list disagree with f at some point. In other words, for each of the other functions, there exists a k : nat such that g k ≠ f k.

Since nat is enumerable, that integer comparison is decidable, and that the list is finite, there is a terminating algorithm to solve this problem. In imperative pseudo-code:

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

If the list has several occurrences of f, then the algorithm never terminates (the occurrences remain candidates forever). If there is zero or one occurrence, the algorithm terminates but there is no way of deciding whether the remaining candidate is totally equal to f.

Hence the assumption stated above is necessary for termination and correction. That’s likely not easy to implement in Coq, especially since you have to convince Coq of the termination. Good luck if that’s really what you want. ;-)