val matrix_seq (#c #m #n: _) (gen: matrix_generator c m n)
    : (t:
      SB.seq c
        { (SB.length t = (m * n)) /\
          (forall (i: under m) (j: under n). SB.index t (get_ij m n i j) == gen i j) /\
          (forall (ij: under (m * n)). SB.index t ij == gen (get_i m n ij) (get_j m n ij)) })
let matrix_seq #c #m #n (gen: matrix_generator c m n) : (t:SB.seq c{ (SB.length t = (m*n)) /\
  (forall (i: under m) (j: under n). SB.index t (get_ij m n i j) == gen i j) /\ 
  (forall(ij: under (m*n)). SB.index t ij == gen (get_i m n ij) (get_j m n ij))
}) = init gen
val matrix_seq (#c #m #n: _) (gen: matrix_generator c m n)
    : (t:
      SB.seq c
        { (SB.length t = (m * n)) /\
          (forall (i: under m) (j: under n). SB.index t (get_ij m n i j) == gen i j) /\
          (forall (ij: under (m * n)). SB.index t ij == gen (get_i m n ij) (get_j m n ij)) })
let matrix_seq #c #m #n (gen: matrix_generator c m n)
    : (t:
      SB.seq c
        { (SB.length t = (m * n)) /\
          (forall (i: under m) (j: under n). SB.index t (get_ij m n i j) == gen i j) /\
          (forall (ij: under (m * n)). SB.index t ij == gen (get_i m n ij) (get_j m n ij)) }) =
init gen
FStar.Matrix.fst.checked
prims.fst.checked FStar.Seq.Properties.fsti.checked FStar.Seq.Permutation.fsti.checked FStar.Seq.Equiv.fsti.checked FStar.Seq.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.IntegerIntervals.fst.checked FStar.Classical.fsti.checked FStar.Algebra.CommMonoid.Fold.fsti.checked FStar.Algebra.CommMonoid.Equiv.fst.checked
FStar.Matrix.fst
Prims.pos FStar.Matrix.matrix_generator FStar.Matrix.init FStar.Seq.Base.seq Prims.l_and Prims.b2t Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.Mul.op_Star Prims.l_Forall FStar.IntegerIntervals.under Prims.eq2 FStar.Seq.Base.index FStar.Matrix.get_ij FStar.Matrix.get_i FStar.Matrix.get_j
(*
   Copyright 2022 Microsoft Research
   
   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at
   
       http://www.apache.org/licenses/LICENSE-2.0
       
   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.

   Author: A. Rozanov
*)

(*
   In this module we provide basic definitions to work with matrices via
   seqs, and define transpose transform together with theorems that assert
   matrix fold equality of original and transposed matrices.
*)


module FStar.Matrix

module CE = FStar.Algebra.CommMonoid.Equiv
module CF = FStar.Algebra.CommMonoid.Fold
module SP = FStar.Seq.Permutation
module SB = FStar.Seq.Base
module SProp = FStar.Seq.Properties
module ML = FStar.Math.Lemmas

open FStar.IntegerIntervals   
open FStar.Mul
open FStar.Seq.Equiv

(* 
   A little glossary that might help reading this file
   We don't list common terms like associativity and reflexivity.

   lhs, rhs               left hand side, right hand side
   liat                   subsequence of all elements except the last (tail read backwards)
   snoc                   construction of sequence from a pair (liat, last) (cons read backwards)
   un_snoc                decomposition of sequence into a pair (liat, last)
   foldm                  sum or product of all elements in a sequence using given CommMonoid
   foldm_snoc             recursively defined sum/product of a sequence, starting from the last element
   congruence             respect of equivalence ( = ) by a binary operation ( * ), a=b ==> a*x = b*x
   unit                   identity element (xu=x, ux=x) (not to be confused with invertible elements)
*)

type matrix c m n = z:SB.seq c { SB.length z = m*n }
 
let seq_of_matrix #c #m #n mx = mx

let ijth #c #m #n mx i j = SB.index mx (get_ij m n i j)

let ijth_lemma #c #m #n mx i j 
 : Lemma (ijth mx i j == SB.index (seq_of_matrix mx) (get_ij m n i j)) = ()

let matrix_of_seq #c m n s = s

let foldm #c #eq #m #n cm mx = SP.foldm_snoc cm mx
 
let matrix_fold_equals_fold_of_seq #c #eq #m #n cm mx
  : Lemma (ensures foldm cm mx `eq.eq` SP.foldm_snoc cm (seq_of_matrix mx)) [SMTPat(foldm cm mx)]
  = eq.reflexivity (foldm cm mx)

let matrix_fold_internal #c #eq #m #n (cm:CE.cm c eq) (mx: matrix c m n)
  : Lemma (ensures foldm cm mx == SP.foldm_snoc cm mx) = ()
     
(* A flattened matrix (seq) constructed from generator function
   Notice how the domains of both indices are strictly controlled. *)
let init #c (#m #n: pos) (generator: matrix_generator c m n)
  : matrix_of generator =  
  let mn = m * n in
  let generator_ij ij = generator (get_i m n ij) (get_j m n ij) in
  let flat_indices = indices_seq mn in  
  let result = SProp.map_seq generator_ij flat_indices in
  SProp.map_seq_len generator_ij flat_indices;
  assert (SB.length result == SB.length flat_indices);
  let aux (i: under m) (j: under n) 
    : Lemma (SB.index (SProp.map_seq generator_ij flat_indices) (get_ij m n i j) == generator i j) 
    = consistency_of_i_j m n i j;
      consistency_of_ij m n (get_ij m n i j);
      assert (generator_ij (get_ij m n i j) == generator i j);
      SProp.map_seq_index generator_ij flat_indices (get_ij m n i j) in
  let aux1 (ij: under mn) 
    : Lemma (SB.index (SProp.map_seq generator_ij flat_indices) ij == generator_ij ij) 
    = SProp.map_seq_index generator_ij flat_indices ij in 
  FStar.Classical.forall_intro aux1;
  FStar.Classical.forall_intro_2 aux;
  result
  
private let matrix_seq #c #m #n (gen: matrix_generator c m n) : (t:SB.seq c{ (SB.length t = (m*n)) /\
  (forall (i: under m) (j: under n). SB.index t (get_ij m n i j) == gen i j) /\
val matrix_seq (#c #m #n: _) (gen: matrix_generator c m n)
    : (t:
      SB.seq c
        { (SB.length t = (m * n)) /\
          (forall (i: under m) (j: under n). SB.index t (get_ij m n i j) == gen i j) /\
          (forall (ij: under (m * n)). SB.index t ij == gen (get_i m n ij) (get_j m n ij)) })
gen: FStar.Matrix.matrix_generator c m n
  -> t:
    FStar.Seq.Base.seq c
      { FStar.Seq.Base.length t = m * n /\
        (forall (i: FStar.IntegerIntervals.under m) (j: FStar.IntegerIntervals.under n).
            FStar.Seq.Base.index t (FStar.Matrix.get_ij m n i j) == gen i j) /\
        (forall (ij: FStar.IntegerIntervals.under (m * n)).
            FStar.Seq.Base.index t ij == gen (FStar.Matrix.get_i m n ij) (FStar.Matrix.get_j m n ij)
        ) }