Matrix.v

Require Import Coq.Vectors.Vector.

Definition drop {A} {m n} : Vector.t A (m + n) -> Vector.t A n.
Proof.
  induction m.
  - intros vec. exact vec.
  - intros vec. inversion vec; subst.
    apply IHm. apply X.
Defined.
                      
Definition to_matrix {A} {m n} : Vector.t A (m * n) -> Vector.t (Vector.t A n) m.
Proof.
  induction m; simpl; intros vec.
  - apply nil.
  - apply cons.
    + eapply take; [ | exact vec].
      apply Nat.le_add_r.
    + apply IHm. eapply drop. exact vec.
Defined.

Arguments cons {A} _ {n} _.
Arguments nil {A}.

Definition example : Vector.t nat (2 * 2) := (cons 1 (cons 2 (cons 3 (cons 4 nil)))).

Eval compute in to_matrix example.