-
This is a formal matrix library in Coq, and integrated with multiple different implementations.
-
Our goal is to provide a unified framework for different implementations of formalized matrix libraries, so as to decouple the differences between underlying technologies and upper-level applications.
-
There are several design ideas in this:
- we mainly use equivalence relations on setoid instead of Leibniz equal.
- organize an operation and its related properties with typeclasses instead of unorganized scattered assumptions, to simplify the proof and improve the readibility.
- organize the mathematical hierarchy of element or matrix with module type.
- mainly use functor to maintain the polymorphism of the design, the concrete theory could be batch exported.
-
What we have done?
- First, developped several useful extensions for Coq Standard Library, such as: NatExt.v ZExt.v QExt.v QcExt.v RExt.v SetoidListExt.v SetoidListListExt.v HierarchySetoid.v
- Second, seperately reimplement formal matrix library of several known matrix model.
- Third, design mathematical hierarchy of matrix element and matrix interface.
- Forth, package different implementations according the matrix interface.
- Fifth, create conversion between different models, and proof lots of them are homomorphism/isomomorphism.
-
What we got?
- An available formal matrix library with unified interface under several different low-level implementations.
- A fundamental technical comparison of these different models, about maturity, simplicity, technical difficulty etc.
-
History of this project?
- It is a submodule of project VFCS
- A stage version is published in SETTA 2022, and located in coq-matrix.
-
How to contact us?
- We are a team focusing on formal engineering mathematics study, and located in Nanjing University of Aeronautics and Astronautics, in China.
- Author: ZhengPu Shi (zhengpushi@nuaa.edu.cn)
| Models | DepList | DepPair | DepRec | NatFun | FinFun | SafeNatFun |
|---|---|---|---|---|---|---|
| Maturity | * | * | ** | ** | *** | ** |
| Conciseness of the definitions | * | * | * | *** | *** | *** |
| Conciseness of the proofs | * | * | ** | *** | *** | *** |
| Conciseness of the extracted OCaml code | * | * | *** | ** | ** | ** |
| Simplicity of the syntax or skill | ** | ** | *** | ** | * | * |
-
Dependent projects
- CoqExt: Extension of Coq Standard Libray.
-
Related projects
- VFCS: Verified flight control system.
- DepRec: Matrix by NUAA
- DepList: Coq.Vectors.Vector
- DepPair: Matrix in Coquelicot
- NatFun: Verified Quantum Computing, Software Foundations Inspired, Volume Q.
- FinFun: Mathematical Component
- [SafeNatFun]: by myself, look at the source code.
-
Basic usage
From CoqMatrix Require Import MatrixNat. (* use "MatrixZ, MatrixQ, MatrixQc, MatrixR" as you need *) (** Then, all functions, theorems, notations are available *) Example dl := [[1;2;3];[4;5;6]]. Example m1 : mat 2 3 := @l2m 2 3 dl. Compute (m2l m1). (* = [[1; 2; 3]; [4; 5; 6]] : list (list A) *) Compute (mnth m1 0 1). (* = 2 : A *) Compute (m2l (m1\T)). (* = [[1; 4]; [2; 5]; [3; 6]] : list (list A) *) Goal mmap S m1 == l2m [[2;3;4];[5;6;7]]. Proof. (** Proof with tactic "lma" (linear matrix arithmetic), availabe for all models *) lma. Qed. (** Check that if A is nat really *) Print A. (* A = nat : Type *) (** You can mixed use all models *) Import MatrixAllNat. (* all models *) Compute @DL.l2m 2 3 dl. Compute @DP.l2m 2 3 dl. Compute @DR.l2m 2 3 dl. Compute @NF.l2m 2 3 dl.
-
Support Q type (rational number) and Qc type (canonical rational number), hence the low-level equality is Setoid Equality instead of Leibniz Equality.
Import MatrixQ. (* automatic maintain the Scope and Notations. for exmaple, here, Q_scope is opened. *) Example m1 : mat 2 3 := l2m [[6/4;10/4;7/2];[4;5;6]]. Example m2 : mat 2 3 := l2m [[1.5;2.5;3.5];[4;5;6]]. Example eq1: m1 == m2. Proof. lma. Qed. (** Proof by ltac or by using properties *) Goal m1 * (mat1 _) == m2. Proof. lma. Qed. Goal m1 * (mat1 _) == m2. Proof. rewrite mmul_1_r. apply eq1. Qed.
-
Conversion between models, and all these conversion functions are bijective.
(* opem matrix theory on Z with default model *) Import MatrixZ. (* open matrix theory on Z with all models (optional) *) Import MatrixAllZ. (** convert from one model to other models *) Example m : NF.mat 2 2 := NF.mk_mat_2_2 1 2 3 4. Compute nf2dl m. (* = [[1; 2]; [3; 4]]%vector : DL.mat 2 2 *) Compute nf2dp m. (* = (1, (2, tt), (3, (4, tt), tt)) : DP.mat 2 2 *) Compute nf2dr m. (* = {| mdata := [[1;2];[3;4]]; .. |} : DR.mat 2 2 *) (** prove that {SF -> DL -> DP -> DR -> NF -> DL -> SF} return back *) Goal forall r c (m0 : SF.mat r c), let m1 : DL.mat r c := sf2dl m0 in let m2 : DP.mat r c := dl2dp m1 in let m3 : DR.mat r c := dp2dr m2 in let m4 : NF.mat r c := dr2nf m3 in let m5 : DL.mat r c := nf2dl m4 in let m6 : SF.mat r c := dl2sf m5 in m6 == m0. Proof. intros. unfold m6,m5,m4,m3,m2,m1,dl2dp,dp2dr,dr2nf,nf2dl,dl2sf,sf2dl. rewrite DR.m2l_l2m_id; auto with mat. rewrite NF.m2l_l2m_id; auto with mat. rewrite DP.m2l_l2m_id; auto with mat. rewrite DL.m2l_l2m_id; auto with mat. rewrite DL.m2l_l2m_id; auto with mat. rewrite SF.l2m_m2l_id; auto with mat. reflexivity. Qed.