Thomas.v

From mathcomp Require Import 
all_ssreflect algebra.matrix
algebra.ssralg.
Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import 
eqtype fingroup fintype ssrnat seq finalg ssralg.   
From mathcomp Require Import 
bigop gproduct finset div.




From mathcomp Require Import 
all_ssreflect.
Require Import ssreflect ssrfun ssrbool.

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 F n m := Vector.t (Vector.t R n) m.

  (* Thomas: I see you have renamed/deleted it to F
     but it won't compile because all the functions
     uses Matrix. Feel to change it again.
     I brought it because I needed to compile the
     code base*)
  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 (Fin.to_nat f) as [m Hm].
    apply (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 (elimT ltP) in Hx.
    apply (Fin.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 finite_to_ord_correctness n (i : Fin.t n) :
    ord_to_finite (finite_to_ord i) = i.
  Proof.
    induction n.
    + inversion i.
    + pose proof fin_inv_S i as [-> | (i' & ->)].
      ++ cbn; reflexivity.
      ++  specialize (IHn i').
          unfold 
          finite_to_ord,
          ord_to_finite 
          in * |- *.
          cbn in * |- *.          
          destruct (Fin.to_nat i') as [a Ha].
          cbn.
          f_equal.
          cbn in *.
          rewrite Fin.of_nat_ext.
          rewrite Fin.of_nat_ext in IHn.
          exact IHn.
  Qed.


  Lemma ord_to_finite_correctness n (i : 'I_n) :
    finite_to_ord (ord_to_finite i) = i.
  Proof.
    unfold finite_to_ord, 
      ord_to_finite.
    rewrite Fin.to_nat_of_nat.
    destruct i; cbn.
    f_equal.
    apply bool_irrelevance.
  Qed.