Ssreflect Users Discussion List

[Georges Gonthier <>]

   This is probably the simplest way, but by no means the only one. You could 
also establish other properties that characterise the rank; the mxalgebra 
library provides many of these for the ssr rank function, so by proving 
my_rank = /rank you'll get them all. Conversely these properties show that 
any "rank" function characterized by, say, a Smith normal form, must coincide 
with the ssr rank function.
   Note that as the ssr rank is computed by Gaussian elimination in a field, 
you will have to start with an independent characterization if your 
definition is more general (say, over  a PID domain). Also note that in full 
generality the several "rank" variations do not always coincide. 

  Georges

-----Original Message-----
From: Vincent Siles [] 
Sent: 21 June 2011 13:31
To: 
Subject: defining an executable version of rank

I have defined a function to effectively compute the rank of matrix and want 
to prove it correct in ssr. Is the only way to prove is to prove that is 
something like

forall n m (A : 'M[R]_(n,m)), \rank A = my_rank n m A

?

Cheers,
Vincent