Hello,
I have a function that creates a matrix filled with zeros and then
assigns 1 to elements on the diagonal. I want to prove that the part
of the matrix above the diagonal is unchanged.
module MatrixTest
use ref.Ref
use int.Int
use matrix.Matrix
let matrixTest (n : int)
requires { 0 < n }
Dear Evgeny,
With the following change to your program, both invariants are proved
instantly by Alt-Ergo. The reason why the invariants are true is that
the contents of the matrix above the diagonal are unchanged. My change
makes this explicit. In general, as a user I prefer doing this kind of
Le 21/05/2019 à 09:48, Raphael Rieu-Helft a écrit :
Dear Evgeny,
With the following change to your program, both invariants are proved
instantly by Alt-Ergo. The reason why the invariants are true is that
the contents of the matrix above the diagonal are unchanged. My change
makes this explic
