Record types with invariants are not extensional
The following program successfully verifies:
module Test
use int.Int
type pair = {x: int; y: int}
type t
goal test :
forall a:pair, b:pair.
a.x = b.x /\ a.y = b.y -> a = b
end
but adding an invariant causes it to fail (with Unknown):
module Test
use int.Int
type pair = {x: int; y: int} invariant { true }
type t
goal test :
forall a:pair, b:pair.
a.x = b.x /\ a.y = b.y -> a = b
end
When not using the invariant Why3 seems to convert the record to an ADT:
theory Test
(* use why3.BuiltIn.BuiltIn *)
(* use why3.Bool.Bool *)
(* use why3.Unit.Unit *)
(* use int.Int *)
type pair =
| Pair'mk (x:int) (y:int)
type t
goal test : forall a:pair, b:pair. a.x = b.x /\ a.y = b.y -> a = b
end
but after adding the invariant it seems to create an opaque type instead:
theory Test
(* use why3.BuiltIn.BuiltIn *)
(* use why3.Bool.Bool *)
(* use why3.Unit.Unit *)
(* use int.Int *)
goal pair'vc : true
type pair
function x pair : int
function y pair : int
axiom pair'invariant : forall self:pair. true
type t
goal test : forall a:pair, b:pair. a.x = b.x /\ a.y = b.y -> a = b
end