Skip to content

Instantly share code, notes, and snippets.

Created August 3, 2018 12:39
What would you like to do?
Require Import Coq.Vectors.Vector.
Definition drop {A} {m n} : Vector.t A (m + n) -> Vector.t A n.
induction m.
- intros vec. exact vec.
- intros vec. inversion vec; subst.
apply IHm. apply X.
Definition to_matrix {A} {m n} : Vector.t A (m * n) -> Vector.t (Vector.t A n) m.
induction m; simpl; intros vec.
- apply nil.
- apply cons.
+ eapply take; [ | exact vec].
apply Nat.le_add_r.
+ apply IHm. eapply drop. exact vec.
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment