Impossible to prove simple lemma about polymorphic maps with CVC4 and Z3
Why3 code:
use map.Map
axiom a: not (forall x : int -> 'a, u : 'a. (set x 1 u)@1 = u)
goal g: false
The problem seems to be that, for some reason, the encoding of the lambda appearing in the definition of set does not generate a defining axiom.
Then, when maps go through the machinery of encoding of polymorphism, we cannot leverage the native support of arrays from provers, so they don't have any information about the "set" function.