Programming with Dependent Types in Coq: a Study of Square Matrices

Associated paper: Programming with Dependent Types in Coq: a Study of Square Matrices.
The Coq proof system allows users to write (functional) programs and to reason about them in a formal way. We study how to program using dependently typed data structures in such a setting. Using dependently typed data structures enables programmers to have more precise specifications for their programs before starting proving any significant properties (e.g. total correctness) about these programs.
We particularly focus on an operational description of square matrices and their operations. Matrices are represented using dependent types. A matrix is a vector of rows, which are themselves vectors indexed by natural numbers. We also take advantage of Coq modules system to have matrices parametrised by a carrier set. Finally, this operational description of square matrices can be extracted into a mainstream functional programming language like Ocaml.
Relevant links

Global Index

(283 entries)

Axiom Index

(67 entries)

Lemma Index

(106 entries)

Constructor Index

(2 entries)

Inductive Index

(1 entry)

Definition Index

(89 entries)

Module Index

(12 entries)

Library Index

(6 entries)

Global Index

A

A [definition, in squarematrices]
A [definition, in operators]
A [definition, in matrices]
A [definition, in carrier]
A [axiom, in carrier]
A [axiom, in matrices]
A [definition, in matrices]
A [definition, in squarematrices]
A [definition, in operators]
A [axiom, in operators]
A [axiom, in squarematrices]
access_sym [lemma, in matrices]
addmatrix [definition, in squarematrices]
addmatrix [axiom, in squarematrices]
addmatrix [definition, in matrices]
addmatrix [axiom, in matrices]
addmatrix_assoc [axiom, in matrices]
addmatrix_assoc [lemma, in squarematrices]
addmatrix_assoc [lemma, in matrices]
addmatrix_assoc [axiom, in squarematrices]
addmatrix_oppmatrix [lemma, in squarematrices]
addmatrix_oppmatrix [lemma, in matrices]
addmatrix_oppmatrix [axiom, in matrices]
addmatrix_oppmatrix [axiom, in squarematrices]
addmatrix_sym [axiom, in squarematrices]
addmatrix_sym [lemma, in squarematrices]
addmatrix_sym [lemma, in matrices]
addmatrix_sym [axiom, in matrices]
addmatrix_zero_l [lemma, in squarematrices]
addmatrix_zero_l [lemma, in matrices]
addmatrix_zero_l [axiom, in squarematrices]
addmatrix_zero_l [axiom, in matrices]
addvect [axiom, in operators]
addvect [definition, in operators]
addvect_assoc [lemma, in operators]
addvect_assoc [axiom, in operators]
addvect_oppvect [lemma, in operators]
addvect_oppvect [axiom, in operators]
addvect_reg [lemma, in operators]
addvect_reg [axiom, in operators]
addvect_sym [axiom, in operators]
addvect_sym [lemma, in operators]
addvect_zero_l [axiom, in operators]
addvect_zero_l [lemma, in operators]
Aeq [definition, in operators]
Aeq [definition, in operators]
Aeq [definition, in carrier]
Aeq [definition, in squarematrices]
Aeq [axiom, in matrices]
Aeq [axiom, in squarematrices]
Aeq [axiom, in carrier]
Aeq [definition, in squarematrices]
Aeq [axiom, in operators]
Aeq [definition, in matrices]
Aeq [definition, in matrices]
Amult [definition, in carrier]
Amult [definition, in squarematrices]
Amult [definition, in matrices]
Amult [definition, in matrices]
Amult [definition, in operators]
Amult [definition, in squarematrices]
Amult [definition, in operators]
Amult_scalprod [lemma, in matrices]
Aopp [definition, in operators]
Aopp [definition, in squarematrices]
Aopp [axiom, in operators]
Aopp [definition, in matrices]
Aopp [axiom, in squarematrices]
Aopp [definition, in carrier]
Aopp [axiom, in carrier]
Aopp [definition, in squarematrices]
Aopp [axiom, in matrices]
Aopp [definition, in matrices]
Aopp [definition, in operators]
Aplus [definition, in matrices]
Aplus [definition, in squarematrices]
Aplus [definition, in squarematrices]
Aplus [definition, in matrices]
Aplus [definition, in carrier]
Aplus [definition, in operators]
Aplus [definition, in operators]
Aplus_Aplus [lemma, in matrices]
A0 [definition, in matrices]
A0 [definition, in operators]
A0 [definition, in squarematrices]
A0 [definition, in carrier]
A0 [definition, in operators]
A0 [definition, in squarematrices]
A0 [definition, in matrices]
A1 [definition, in operators]
A1 [definition, in squarematrices]
A1 [definition, in matrices]
A1 [definition, in carrier]
A1 [definition, in operators]
A1 [definition, in squarematrices]
A1 [definition, in matrices]
A_ring [axiom, in matrices]
A_ring [definition, in operators]
A_ring [axiom, in squarematrices]
A_ring [definition, in carrier]
A_ring [axiom, in operators]
A_ring [definition, in operators]
A_ring [definition, in squarematrices]
A_ring [axiom, in carrier]
A_ring [definition, in matrices]
A_ring [definition, in squarematrices]
A_ring [definition, in matrices]

C

Carrier [module, in carrier]
carrier [library]

D

decompose [lemma, in vects]
decompose_dep [lemma, in vects]

E

eq_add_S_tr [definition, in matrices]
eq_add_S_tr [definition, in operators]
eq_add_S_tr [definition, in squarematrices]
eq_vect [definition, in vects]
eq_vect_vcons [lemma, in vects]
extract [library]

G

getcolumn [definition, in matrices]
getcolumn_addvect [lemma, in matrices]
getcolumn_In [lemma, in matrices]
getline [definition, in matrices]
getline_lemma [lemma, in matrices]

H

head [definition, in vects]
head_addvect [lemma, in operators]
head_lemma_1 [lemma, in vects]
head_multscal [lemma, in operators]

I

I [definition, in squarematrices]
I [axiom, in matrices]
I [axiom, in squarematrices]
I [definition, in matrices]
induc1 [lemma, in vects]
induc2 [lemma, in vects]
induc3 [lemma, in vects]
I' [definition, in matrices]
I'_mat [lemma, in matrices]
I'_mat' [lemma, in matrices]
I'_simpl [lemma, in matrices]
I_mat [lemma, in squarematrices]
I_mat [lemma, in matrices]
I_mat [axiom, in matrices]
I_mat [axiom, in squarematrices]

L

last [definition, in vects]
last_n [lemma, in vects]
last_n' [lemma, in vects]
last_o1 [lemma, in vects]
last_o2 [lemma, in vects]
last_o3 [lemma, in vects]
last_o4 [lemma, in vects]
last_S [lemma, in vects]
last_vcons [lemma, in vects]
last_vcons' [lemma, in vects]
le_Sn_le_n_pred [lemma, in vects]
le_S_lt_O [lemma, in vects]
Lmatrix [axiom, in matrices]
Lmatrix [definition, in matrices]
lt_decompose [lemma, in operators]
lt_le_pred [lemma, in vects]

M

map [definition, in vects]
map_prodmat_getcolumn [lemma, in matrices]
map_2 [lemma, in vects]
map_2' [lemma, in vects]
Matrices [module, in matrices]
matrices [library]
matrixZ [module, in matrices]
mat_I [lemma, in matrices]
mat_I [axiom, in matrices]
mat_I [axiom, in squarematrices]
mat_I [lemma, in squarematrices]
mat_I_last [lemma, in matrices]
mat_I_last_aux [lemma, in matrices]
mkrowI [axiom, in operators]
mkrowI [definition, in operators]
mkrowI_mkvect [lemma, in operators]
mkrowI_nth [lemma, in operators]
mkrowI_nth [axiom, in operators]
mkrowI_prodvectmat [lemma, in matrices]
mkvect [definition, in operators]
mkvect [axiom, in operators]
mkvectA0_prodvectmat [lemma, in matrices]
mkvectA0_prodvectmatrix [lemma, in matrices]
mkzero [definition, in matrices]
multscal [axiom, in operators]
multscal [definition, in operators]
MyMatrices [module, in squarematrices]
MyVectors [module, in matrices]

N

nth [definition, in vects]
nth_addvect [axiom, in operators]
nth_addvect [lemma, in operators]
nth_lemma [lemma, in vects]
nth_lemma' [lemma, in vects]
nth_mkvect [lemma, in matrices]
nth_multscal [axiom, in operators]
nth_multscal [lemma, in operators]

O

o [definition, in matrices]
o [axiom, in matrices]
o [axiom, in squarematrices]
o [definition, in squarematrices]
operators [library]
oppmatrix [definition, in squarematrices]
oppmatrix [definition, in matrices]
oppmatrix [axiom, in squarematrices]
oppmatrix [axiom, in matrices]
oppvect [definition, in operators]
oppvect [axiom, in operators]
o1 [lemma, in matrices]
o1 [lemma, in operators]
o1' [lemma, in matrices]
o2 [lemma, in operators]
o2 [lemma, in matrices]
o2' [lemma, in matrices]
o3 [lemma, in matrices]
o3' [lemma, in matrices]
o4 [lemma, in matrices]

P

R

ring_thm2 [lemma, in operators]

S

T

tail [definition, in vects]
tail_addvect [lemma, in operators]
tail_multscal [lemma, in operators]
TMatrices [module, in matrices]
TSquareMatrices [module, in squarematrices]
TVectors [module, in operators]
two_step_ind [lemma, in vects]

U

uniq [lemma, in vects]

V

vcons [constructor, in vects]
vcons_lemma [lemma, in vects]
vect [inductive, in vects]
Vectors [module, in operators]
vects [library]
vnil [constructor, in vects]