Matrix.v

Require Import Field_theory 
  Ring_theory List NArith 
  Ring Field Utf8 Lia 
  Coq.Arith.PeanoNat
  Vector Fin.
From mathcomp Require Import 
  all_ssreflect algebra.matrix
  algebra.ssralg.

Import ListNotations.

Set Implicit Arguments.


Section Mat.


  Variable (R : Type).

  Lemma vector_inv_0 (v : Vector.t R 0) :
    v = @Vector.nil R.
  Proof.
    refine (match v with
            | @Vector.nil _ => _
            end).
    reflexivity.
  Defined.

  Lemma vector_inv_S (n : nat) (v : Vector.t R (S n)) :
    {x & {v' | v = @Vector.cons _ x _ v'}}.
  Proof.
    refine (match v with
            | @Vector.cons _ x _ v' =>  _
            end).
    eauto.
  Defined.

  Lemma fin_inv_0 (i : Fin.t 0) : False.
  Proof. refine (match i with end). Defined.

  Lemma fin_inv_S (n : nat) (i : Fin.t (S n)) :
    (i = Fin.F1) + {i' | i = Fin.FS i'}.
  Proof.
    refine (match i with
            | Fin.F1 _ => _
            | Fin.FS _ _ => _
            end); eauto.
  Defined.


  Definition vector_to_finite_fun : 
    forall n, Vector.t R n -> (Fin.t n -> R).
  Proof.
    induction n.
    + intros v f.
      apply fin_inv_0 in f.
      refine (match f with end).
    + intros v f.
      destruct (vector_inv_S v) as (vhd & vtl & vp).
      destruct (fin_inv_S f) as [h | [t p]].
      exact vhd.
      exact (IHn vtl t).
  Defined.


  Definition finite_fun_to_vector : 
    forall n,  (Fin.t n -> R) -> Vector.t R n.
  Proof.
    induction n.
    + intros f.
      apply Vector.nil.
    + intros f.
      apply Vector.cons.
      apply f, Fin.F1.
      apply IHn;
      intro m.
      apply f, Fin.FS, m.
  Defined.


  Lemma finite_fun_to_vector_correctness 
    (m : nat) (f : Fin.t m -> R) (i : Fin.t m) :
    Vector.nth (finite_fun_to_vector f) i = f i.
  Proof.
    induction m.
    - inversion i.
    - pose proof fin_inv_S i as [-> | (i' & ->)].
      + reflexivity.
      + cbn. 
        now rewrite IHm.
  Defined.


  Lemma vector_to_finite_fun_correctness 
    (m : nat) (v : Vector.t R m) (i : Fin.t m) :
    Vector.nth v i = (vector_to_finite_fun v) i.
  Proof.
    induction m.
    - inversion i.
    - pose proof fin_inv_S i as [-> | (i' & ->)].
      destruct (vector_inv_S v) as (vhd & vtl & vp).
      rewrite vp.
      reflexivity.
      destruct (vector_inv_S v) as (vhd & vtl & vp).
      rewrite vp;
      simpl; 
      now rewrite IHm.
  Defined.

  Lemma vector_finite_back_forth : 
    forall (n : nat) (v : Vector.t R n),
    v = finite_fun_to_vector (vector_to_finite_fun v).
  Proof.
    induction n.
    + intros v.
      pose proof (vector_inv_0 v) as Hv.
      subst; 
      reflexivity.
    + intros v.
      destruct (vector_inv_S v) as (vhd & vtl & vp).
      subst; simpl; f_equal.
      apply IHn.
  Defined.
      


  
End Mat.

Section Reflection.

  (* These two are just need because it's 
    opaque in library *)
  Lemma introT : 
    forall (P : Prop) (b : bool), 
    reflect P b -> P -> b.
  Proof.
    intros ? ? Hr Hp.
    case b eqn:Ht.
    constructor.
    inversion Hr as [_ | Hrt].
    unfold not in Hrt.
    specialize (Hrt Hp).
    exfalso.
    exact Hrt.
  Defined.

  Lemma elimT :
    forall (P : Prop) (b : bool), 
    reflect P b -> b -> P.
  Proof.
    intros ? ? Hr H.
    case b eqn:Hb.
    inversion Hr as [Hrt | _].
    exact Hrt.
    refine (match H with end).
  Defined.

End Reflection.


Section Mx.

  Variable (R : Type).

  Definition Matrix n m := Vector.t (Vector.t R n) m.

  Definition finite_fun_to_matrix {n m}  
    (f : Fin.t n -> Fin.t m -> R) : Matrix n m :=
    @finite_fun_to_vector _ m (fun (x : Fin.t m) => 
      @finite_fun_to_vector _ n (fun (y : Fin.t n) => f y x)).

  Definition matrix_to_finite_fun {n m} 
    (mx : Matrix n m) : Fin.t n -> Fin.t m -> R :=
    fun (x : Fin.t n) (y : Fin.t m) => 
      @vector_to_finite_fun _ n 
        ((@vector_to_finite_fun _ m mx) y) x.

  Lemma matrix_to_finite_back_forth : 
    forall n m (mx : Matrix n m),
    mx = finite_fun_to_matrix (matrix_to_finite_fun mx).
  Proof.
    intros ? ?.
    revert n.
    induction m.
    + intros ? ?.
      unfold Matrix in mx.
      pose proof (vector_inv_0 mx) as Hn.
      subst; reflexivity.
    + intros ? ?.
      unfold Matrix in mx. 
      destruct (vector_inv_S mx) as (vhd & vtl & vp).
      subst.
      unfold finite_fun_to_matrix, 
      matrix_to_finite_fun.
      simpl; f_equal.
      apply vector_finite_back_forth.
      apply IHm.
  Defined.



  Definition finite_to_ord {n} (f : Fin.t n) : 'I_n.
    destruct (to_nat f) as [m Hm].
    apply (Matrix.introT ltP) in Hm.
    apply (Ordinal Hm).
  Defined.

  Definition ord_to_finite {n} (x : 'I_n) : Fin.t n.
    have Hx: x < n by [].
    apply (Matrix.elimT ltP) in Hx.
    apply (of_nat_lt Hx).
  Defined.



  Definition Matrix_to_matrix {n m} 
    (mx : Matrix n m) : 'M[R]_(n, m) :=
    \matrix_(i < n, j < m) 
      (matrix_to_finite_fun 
        mx 
        (ord_to_finite i) 
        (ord_to_finite j)).

  Definition matrix_to_Matrix {n m} 
    (mx : 'M[R]_(n, m)) : Matrix n m :=
    finite_fun_to_matrix (fun (i : Fin.t n) 
      (j : Fin.t m) => 
      mx (finite_to_ord i) (finite_to_ord j)).


  Lemma matrix_to_Matrix_correctness : 
    forall n m (i : Fin.t n) (j : Fin.t m)
    (mx : 'M[R]_(n, m)),
    mx (finite_to_ord i) (finite_to_ord j) = 
    Vector.nth (Vector.nth (matrix_to_Matrix mx) j) i.
  Proof.
    intros *.
    unfold matrix_to_Matrix,
    finite_fun_to_matrix.
    rewrite finite_fun_to_vector_correctness.
    rewrite finite_fun_to_vector_correctness.
    reflexivity.
  Defined.
    
  Lemma matrix_back_and_forth_same : 
    forall (n m : nat) (mx : Matrix n m),
    mx = matrix_to_Matrix (Matrix_to_matrix mx).
  Proof.
    unfold matrix_to_Matrix,
    Matrix_to_matrix,
    matrix_to_Matrix,
    matrix_to_finite_fun,
    finite_fun_to_matrix,
    matrix_of_fun.
    unfold locked_with.
    destruct matrix_key.
  
    intros ? ?.
    revert n.
    induction m.
    + intros ? ?.
      unfold Matrix in mx.
      pose proof (vector_inv_0 mx) as Hn.
      subst; reflexivity.
    + intros ? ?. 
      unfold Matrix in mx. 
      destruct (vector_inv_S mx) as (vhd & vtl & vp).
      subst.
      simpl.
      f_equal.