Verify if a matrix is reduced in ProLog

For the ones that I might have reached with my recent questions on my matrix operations project, I can actually confirm that everything is working perfectly...except one certain operation. I'm talking of course on a function to check if a matrix is reduced to the Row Echelon Form, and as a newbie in functional/logic programming, it is really the most difficult task that I have yet faced.

So, to this function I need to check:

If the left-to-right diagonal has no zeros;
If the inferior matrix triangle is full of zeros.

This time I'm actually asking for total help as I don't even know how to start creating this mess, really hoping for a generous soul to execute this ambitious function and to please explain her way of thinking and procede.

Solution

Having not heard of Row Echelon Form before, I found https://stattrek.com/matrix-algebra/echelon-form.aspx which tells me that there can be zeros in the left-to-right diagonal as long as each row "starts" later than the one before it. So I'm thinking:

Count how many leading zeros there are in a row.
- Manual recursion grind, if the start of the list is a zero then increment a counter, and recurse down the remaining elements. If the start is not a zero, stop counting.
Building on that, the matrix is in Row Echelon Form if the number of leading zeros in this row is greater than in the previous row. I'm calling that a ratchet, as it can only increase.
- Or if the row is all zeros.
- and if this ratchet/all zeros holds for remaining rows.

% the number of leading zeros in a list [0,0,1,2,3] -> 2
row_leadZeroCount([],             LZC, LZC).
row_leadZeroCount([N|Ns], ZerosToHere, LZC) :-
    (N=0 -> (ZerosSeen is 1+ZerosToHere,
            row_leadZeroCount(Ns, ZerosSeen, LZC))
    ;       LZC = ZerosToHere).  % stop counting at the first non-zero.


% Nested lists are in Row Echelon Form if 
% the leading zeros in this row are more than the previous row
% or we're at a state of all remaining rows being only zeros.
matrix_ref_([], _, _).
matrix_ref_([Row|Rows], RowLen, Ratchet) :-
    row_leadZeroCount(Row, 0, RowZeros),
    (RowZeros < RowLen -> RowZeros > Ratchet
    ; RowZeros = RowLen),
    matrix_ref_(Rows, RowLen, RowZeros).


% wrapper to get row length, to see when a row is all zeros,
% and start the row length Ratchet going.
matrix_ref([Row|Rows]) :-
    length(Row, RowLen),
    matrix_ref_([Row|Rows], RowLen, -1).

e.g.

?- _Mx = [[1,2,3,4],    
          [0,0,1,3],
          [0,0,0,1],    %Example from linked web page
          [0,0,0,0]],
matrix_ref(_Mx).
true

NB. You say "reduced to the Row Echelon Form"; I'm ignoring the "Reduced Row Echelon Form" from that link, assuming that's not what you're asking for.