MathComp matrices over a nonring

Most MathComp matrix operations, such as matrix multiplication, are parameterized over a Ring or Field structure. When you do the dot-products in a matrix multiply, it doesn't matter what order you add up the element products, because addition in a Ring is associative-commutative. But our functional models of matrix algorithms are in floating point, which is not a Ring or Field because (for example) addition is not associative. MathComp handles this by having some matrix operations (such as transpose tr_mx and the very definition of a @matrix _ _ _ (notated as 'M[_]_(_,_)) be parameterized only over a Type when they don't need a Ring structure; it is only the operators whose natural mathematics need additional properties, that require a Ring or Field. That means we can use natural MathComp operations such as blocking and transpose on floating-point matrices 'M[ftype t]_(m,n) but we cannot use MathComp's matrix multiply mulmx. Instead, if we multiply floating-point matrices, we must define it ourselves in a way that specifies exactly what order of operations is done, or (if a relation instead of a function) what order(s) are permitted. The definition update_mx is an example of an operation that naturally does not require a Ring structure. The definition subtract_loop, below, is an example of the other kind; we can't use MathComp's dot-product to define it, so we write a definition that explicitly specifies the order of additions.

Functional model of Cholesky decomposition (jik algorithm)

The next three definitions, up to cholesky_jik_spec, are adapted from similar definitions in coq-libvalidsdp by P. Roux et al.

When we have run the "Cholesky jik algorithm" only up to iteration (i,j), the matrix is only initialized above row i, and in row i up to column j, so we need this subrelation in our loop invariant.

Functional models of forward substitution and back substitution