How can we prove that if for all inputs, f and g returns the same output, then the two functions are equivalent?
lemma func_ext(f: int -> int, g: int -> int)
requires forall x :: f(x) == g(x)
ensures f == g
I would assume this is an axiom but it does not work. Is function extensionality not true in Dafny?
I don't think dafny supports function extensionality. I didn't find anything in official documentation but here is link to comment which confirms this https://github.com/dafny-lang/dafny/issues/2308#issuecomment-1169553777
We do not have functional extensionality in Dafny's theory. I asked @RustanLeino about it recently, and he thought it would be non-trivial to add. Part of the issue is that lambdas can read the heap, so pointwise equality without considering the heap is not enough.