FinMatrix.CoqExt.Basic
- Basic libraries
- Reserved Notations
- Eliminate Warning.
- Customized tactics
- Global coercions
- Extension for option type
- Extension for sig type
- Usually used scopes
FinMatrix.CoqExt.BoolExt
FinMatrix.CoqExt.StrExt
FinMatrix.CoqExt.TupleExt
FinMatrix.CoqExt.ListExt
- list
- Properties of cons
- Properties of hd and tl
- Properties of nth
- nthFull : nth element with index-in-the-bound
- Properties of fold_left
- Properties of fold_right
- Print a list
- Set element of a list
- Swap two elements
- Properties of length
- List to elements
- Customized list induction
- list repeat properties
- Zero list
- Properties of map
- map two lists to a list
- map2 on dlist
- map2 properties with same base type
- concatenation of list
- Convert between list and natural-number-index-function
- Addition, Opposition and Subtraction of list
- constant multiplication of list
- product of two lists
- Generate special list for MatrixUnit
- Convert list to fixed-length list
- Find non-zero element from a list
- Sub list
- dlist (list of list)
- width of a dlist (dlist A)
- nnth : that is nth of nth of dlist
- dlist to elements
- Properties of dlist
- Print a dlist
- a dlist with same element nil
- map2 for dlist
- Convert between dlist and function
- Convert between row and col. eg, 1;2;3 <-> [1];[2];[3]
- head column of a dlist
- tail columns of a dlist
- construct a dlist with a list and a dlist by column
- nth column of a dlist
- Append two objects of dlist type to one object of dlist
- Zero dlist
- transpose a dlist
- dlist unit, like a identity matrix
- map of dlist with f : A -> B
- Extra properties of dmap
- map of dlist with f : A -> A
- map2 of dlist
- dmap2 with same base type
- Square Zero dlist
- dmap2 is considered as dladd
- dmap2 is considered as dlsub
- list dot dlist, and dlist dot dlist
- Properties of dlcmul
- Set element with a constant value
- Set element with a generation function
- Set row with a constant value
- Set row with a generation function
- Row Transform
- dlist remove one row and/or one column
- Setoid equal of list
- Special search algorithm
FinMatrix.CoqExt.Hierarchy
- Small utilities
- <TEMPLATE structures>
- A relation is equivalence relation
- A relation is decidable
- Respect: an operation respect a relation (also known as "well-defined")
- Injective
- Surjective
- Bijective
- Homomorphic
- Homomorphism
- Isomorphism
- Subset
- Associative
- Commutative
- Identity Left/Right
- Inverse Left/Right
- Distributive
- Involution Law
- Total order relations
- Semigroup 半群
- Abelian semigroup 交换半群
- Monoid 幺半群、独异点
- Abelian monoid
- Group
- Abelian Group
- SemiRing
- Ring
- ARing
- Abelian-ring with total order
- Field
- Field with total order
- Convert to R type
- Metric space
FinMatrix.CoqExt.NatExt
- Mathematical Structure
- More properties for nat
- Loop shift
- Extension for nat from (Verified Quantum Computing).
- Useful bdestruct tactic with the help of reflection
- Lost or deprecated lemmas and new lemmas
- Properties for div and mod
FinMatrix.CoqExt.PositiveExt
FinMatrix.CoqExt.ZExt
- Mathematical Structure
- Conversion between Z and other types
- Properties for Zeqb and Zeq
- Other properties
FinMatrix.CoqExt.QExt
FinMatrix.CoqExt.QcExt
FinMatrix.CoqExt.RExt
- Config the usage of Coq-Standard-Library Reals: Hints, Opaque, auto
- Decidable procedure for comparison of R
- Reqb,Rleb,Rltb: Boolean comparison of R
- Suplymentary properties about "real number R"
- Automatic solving equalites or inequalities on real numbers
- atan
- Conversion between R and other types
- Approximate of two real numbers
- Mathematical Structure
- Additional properties
FinMatrix.CoqExt.RealFunction
FinMatrix.CoqExt.Ratan2
FinMatrix.CoqExt.Complex
FinMatrix.CoqExt.LinearSpace
FinMatrix.CoqExt.MyExtrOCamlR
FinMatrix.Matrix.Fin
- _fin type and basic operations
- Cast between fin terms
- Cast between two fin type with actual equal range
- fin m to fin n
- Fin n i + Fin n k -> Fin n (i+k)
- Fin n i + Fin n k -> Fin n (i-k)
- Fin n i -> Fin n (S i)
- Fin n i -> Fin n (pred i)
- Fin n i -> Fin n (loop-shift-left i with k)
- Fin n i -> Fin n (loop-shift-right i with k)
- Fin n i -> Fin n (n - i)
- Fin n i -> Fin (S n) i
- Fin (S n) i -> Fin n i
- Fin n i -> Fin (m + n) i
- Fin (m + n) i -> Fin n i
- Fin m i -> Fin (m + n) i
- Fin (m + n) i -> Fin m i
- Fin n i -> Fin (m + n) (m + i)
- Fin (m + n) (m + i) -> Fin n i
- Fin m i -> Fin (m + n) (i + n)
- Fin (m + n) (i + n) -> Fin m i
- Fin (S n) (S i) -> Fin n i
- Fin n i -> Fin (S n) (S i)
- Sequence of fin
FinMatrix.Matrix.Sequence
FinMatrix.Matrix.Vector
- vec type and basic operations
- Make a vector
- Get head, tail, slice of a vector
- Update a vector
- Predicate of vectors
- Folding of a vector
- Algebraic operations
- Geometric operations
FinMatrix.Matrix.Matrix
- Matrix type and basic operations
- Row vector and column vector
- Make a matrix
- Update a matrix
- Algebraic operations
- Elementary Row Transform
- Test examples
FinMatrix.Matrix.MatrixDet
FinMatrix.Matrix.MatrixGauss
FinMatrix.Matrix.MatrixInvBase
FinMatrix.Matrix.MatrixInvAM
- Matrix Inversion by Adjoint Matrix (Typeclass version)
- Matrix Inversion by Adjoint Matrix (module version)
- More theory of matrix inversion by Adjoint Matrix
- Test
FinMatrix.Matrix.MatrixInvGE
- Inverse matrix based on Gauss elimination (Typeclass version)
- Inverse matrix based on Gauss elimination (module version)
- More theory of matrix inversion by Gauss Elimination
- Test
FinMatrix.Matrix.MatrixInv
FinMatrix.Matrix.MatrixOrth
FinMatrix.Matrix.ElementType
- ElementType
- OrderedElementType
- Element with abelian-monoid structure
- Element with abelian-ring structure
- Element with abelian-ring structure and ordered relation
- Element with field structure
- Element with field structure and ordered relation
- Element with field structure and ordered relation and normed
FinMatrix.Matrix.MatrixModule
- Basic matrix theory
- Definition of the vector type
- Equalities of the vector
- Convert between vector and function
- Convert between vector and list
- Make concrete vector
- Mapping of vector
- Constant vector and zero vector
- Set element of a vector
- Swap two element of a vector
- Insert element to a vector
- Remove one element
- Get head or tail element
- Get head or tail elements
- Remove exact one element at head or tail
- Remove some elements at head or tail
- Construct vector with one element at the head or tail position
- Construct vector with two vectors
- A proposition which all elements of the vector hold
- A proposition which at least one element of the vector holds
- An element belongs to the vector
- An vector belongs to another vector
- Two vectors are equivalent (i.e., contain each other)
- Folding of a vector
- Automation for vector equality proofs
- Definition of the matrix type
- Equalities of the matrix
- Convert between cvec and vec
- Convert between rvec and vec
- Convert between matrix and function
- Convert between matrix and list
- Convert between `list of vectors` and mat
- Make concrete matrix
- Get row and column of a matrix
- Construct matrix with two matrices
- Get head or tail column
- Remove exact one column at head or tail
- Construct matrix from vector and matrix
- Mapping of matrix
- matrix set row / column
- Matrix transposition
- Diagonal Matrix
- Zero matrix
- Automation for matrix equality proofs
- Monoid matrix theory
- Ring matrix theory
- 自然基的基向量
- natural basis, 自然基（最常见的一种标准正交基)
- Vector opposition
- Vector subtraction
- Vector scalar multiplication
- Vector dot product
- Properties of vsum
- Unit vector
- Orthogonal vectors
- Identity matrix
- Matrix trace
- Monoid structure over {madd,mat0,meq}
- Matrix opposition
- Matrix subtraction
- Abelian group structure over {madd,mat0,mopp}
- Scalar multiplication of matrix
- Matrix multiplication
- Matrix multiply vector (treat vector as column vector)
- Vector multiply matrix (treat vector as row vector)
- Mixed properties about mmul, mmulv, mvmul
- Skew-symmetric matrix
- Hardmard product
- Determinant of a matrix over a ring
- Determinant on matrix of 1-,2-, or 3-dim
- Adjoint matrix (Adjugate matrix, adj(A), A* )
- Invertible matrix
- Ordered ring matrix theory
- Field matrix theory
- Properties about veye
- Properties about vcmul
- Projection component of a vector onto another
- Perpendicular component of a vector respect to another
- un-sorted properties about vector
- Properties about zero or non-zero matrices
- Determinant of a matrix over a field
- Cramer rule
- Invertible matrix
- Matrix inversion by GE (Gauss Elimination)
- Matrix Inversion by AM
- Matrix Inversion (default method, JUST IS Notaiton of AM)
- Orthonormal vectors 标准正交的向量组
- Orthogonal matrix
- O(n): General Orthogonal Group, General Linear Group
- SO(n): Special Orthogonal Group, Rotation Group
- Ordered field matrix theory
- Normed ordered field matrix theory
FinMatrix.Matrix.MatrixNat
FinMatrix.Matrix.MatrixZ
FinMatrix.Matrix.MatrixQ
FinMatrix.Matrix.MatrixQc
FinMatrix.Matrix.MatrixR
- Matrix theory come from common implementations
- Matrix theory applied to this type
- Extension for R
- 去掉 a2r 以及 Aabs 的一些引理
- Vector normalization (only valid in R type)
- Angle between two vectors
- The cross product of 2D vectors
- 2D vector theory
- Standard base of 2-D vectors
- 2D vector angle from one to another
- Properties about parallel, orthogonal of 3D vectors
- The cross product (vector product) of two 3-dim vectors
- Skew-symmetric matrix of 3-dimensions
- 3D vector theory
- Standard base for Euclidean space (3-D vectors)
- Direction cosine of 3-D vectors
- The triple scalar product (or called Mixed products) of 3-D vectors
- Standard base for 4-D vectors
- matrix norm
- matrix F norm
- Orthogonal matrix
- SO2 and SO3
- Modules for notations to avoid name pollution
- Usage demo