why3 + alt-ergo fail on unfolding a predicate
Hi, Here is a reduced example. I am not sure that this is the simplest one but though. Ingredients: a record type with an invariant stated with a predicate + a trivial lemma which restates the invariant without the predicate.
module System
use int.Int
use import array.Array as A
predicate eqlgth (i:int)(a b: array int) =
a[i]=b[i]
lemma toto: forall i:int, a b : array int.
eqlgth i a b <-> a[i] = b[i]
type cores =
{ cid : array int;
cload : array int }
invariant {
A.length cid = A.length cload &&
forall i:int. 0<=i<A.length cid -> eqlgth i cid cload
}
by { cid = A.make 0 0; cload = A.make 0 0 }
let lemma lll (i:int) (cs:cores)
requires { 0 <= i < A.length cs.cid }
ensures { cs.cid[i] = cs.cload[i] }
=
assert {true }
end
Strangely alt-ergo is not able to prove it (eprover does). Maybe it is a bug of alt-ergo but it may also come from an error on the generated goal, I could not figure that out.