1.0.6

A updated version for Coq 8.18

ChangeLog:

1. fix: error or warning for Coq 8.18

1.0.4

1. a new module SafeNatFun, and additionally, determinant of generic matrix and inversion matrix by adjoint matrix.
2. preliminary calculus theory.
3. better notation for mnth function, with "m!i!j" instead of "m$i$j".
4. rename A0,A1 to Azero,Aone, to avoiding conflict of A1 in Reals library.
5. temporarily block the "FinFun" model because the math-comp library has been upgraded to 2.0, but our code is designed for math-comp 1.6.xx.
6. Coq version issue
   (1). If Coq version < 8.14.0, Uint63 does not exist
   (2). If Coq version <= 8.14.0, "sqrt_inv" does not exist, we need to use "inv_sqrt".
   (3). If Coq version >= 8.16.1, "sqrt_inv" is suggested, but the "inv_sqrt" is deprecated.
   (4). If Coq version >= 8.17.0, several proofs can be solved by "auto", but need more lines if Coq version is < 8.17.0
   Thus, we prepare a new version 1.0.4 for Coq [8.14.0~8.16.1], and another new version 1.0.5 for Coq.8.17.0

1.0.5 (same as 1.0.4, but for Coq 8.17.0)

This version is the same as 1.0.4, but with small changes for Coq 8.17.0

1.0.3

1. Add a new matrix model naming SF (SafeNatFun), which is a safe version of NF (NatFun). Meanwhile, added conversions between SF and DL/DP/DR/NF/SF, see MatrixAll.v
2. Add a unified tactic "lma" (means Linear Matrix Arithmetic) to solve matrix equations such as "A == B", and it is available in all models. This tactic also worked for vector equations.
3. Add several concrete modules, including MatrixNat, MatrixZ, MatrixQ, MatrixQc, MatrixR, VectorNat, VectorZ, VectorQ, VectorQc, VectorR. These modules are convenient for final developers. The demo usage can be found in each file, such as MatrixR, or can be quickly found in README.md
4. Add usage demo in README.md

So, we are happy to publish a new version v1.0.3.
Any suggestion or correction will be a great encouragement to us.

Full Changelog: 1.0.2...1.0.3

1.0.2

When I publish this project to opam repository, the CI of coqbot in github reports a strange error but I can't solve it,
So, I just skip this coq statement which is not critical.
This version is a simple fix for this issue, and published naming coq-matrix.1.0.1.

I logged the error message and corresponding Coq statement here, for further research later.

Error: Illegal application: 
The term "@fieldAinvProper" of type
 "forall (A : Type) (Aadd : A -> A -> A) (A0 : A) (Aopp : A -> A) (Amul : A -> A -> A) 
    (A1 : A) (Ainv : A -> A) (Aeq : A -> A -> Prop),
  Field Aadd A0 Aopp Amul A1 Ainv Aeq -> Proper (Aeq ==> Aeq) Ainv"
cannot be applied to the terms
 "A" : "Type"
 "Qcplus" : "Qc -> Qc -> Qc"
 "Q2Qc 0" : "Qc"
 "Qcopp" : "Qc -> Qc"
 "Qcmult" : "Qc -> Qc -> Qc"
 "1" : "Qc"
 "Ainv" : "Qc -> Qc"
 "Aeq" : "relation A"
 "Field_Qc" : "Field Qcplus (Q2Qc 0) Qcopp Qcmult 1 Qcinv eq"
The 1st term has type "Type@{A.u0}" which should be coercible to "Type@{Field.u0}".

, and the corresponding position at the CoqMatrix/ElementType.v at line 754

Add Field Field_thy_inst : Field_thy.

1.0.1

Now, this library is independent with CoqExt library, which is a library of myself.
Because I want to publish this project to Coq community.

Available version.

This is a available version of CoqMatrix, we call it 1.0.0.
Lots of ideas have been implemented here, including:

1. full support for setoid equivalence relation of element and matrix itself.
2. Organization of structures with Typeclasses, such as: Associativity, Community, Monoid, AMonoid, Group, AGroup, Ring, Field.
3. Organization of element type with Module, such as: BasicElementType, RingElementType, etc.
4. Organization of matrix theory with Module, such as: BasicMatrixTheory, RingMatrixTheory, etc.
5. Top four implementations (DepRec, DepList, DepPair, NatFun) are available and almost all the proofs have been finished, and last one implementation (FinFun) which is come from Math-Comp project haven't been developed too much.
   Finally, I hope this project will continue to be developed.