Function extensionality in Dafny

Question

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?

Answer 1

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.

Answer 2

There is no extensionality for functions. One big reason for that is that "==" is not translated with a type yet.

So for example take:

var f: int -> int = (x: int) => x;
var g: int -> int = (x: int) => if x >= 0 then x else -x;

var fp: nat -> int = f;
var gp: nat -> int = g;
assert forall x: nat :: fp(x) == gp(x);
assert fp == gp; // Suppose we had extensionality
assert f == g;   // Because fp == f and gp == g
assert -1 == f(-1) == g(-1) == 1;
assert false;

This would go away if only we could have equality according to a type, though.