Kalman Filter

Formalization of Kalman filter properties in Rocq using Mathematical Components (MathComp), Infotheo, Coq Efficient Algebra Library (CoqEAL), and proof techniques adapted from CoqQ (Coq-Quantum). The noise model and matrix expectation operator build on Infotheo finite distributions; positive definiteness and monotonicity lemmas adapt CoqQ Hermitian matrix algebra; executable seqmx programs are linked to the abstract specification through CoqEAL refinements.

Meta

• Author(s):
  • Ilya I. Nikitin
• License: GNU General Public License v3.0 or later
• Compatible Rocq/Coq versions: Rocq 9.0 - 9.1 (MathComp 2.5.0)
• Additional dependencies:
  • Dune 3.21 or later
  • Rocq-Elpi (HB plugin backend)
  • Hierarchy Builder 1.9.0 or later
  • MathComp 2.5.0 boot library
  • MathComp 2.5.0 order library
  • MathComp 2.5.0 fingroup library
  • MathComp 2.5.0 field library
  • MathComp 2.5.0 solvable library
  • MathComp finmap library
  • MathComp 2.5.0 algebra library
  • Elpi (required by Hierarchy Builder)
  • MathComp analysis classical library
  • MathComp analysis reals library
  • MathComp analysis 1.16.0 or later
  • MathComp zify micromega tactics for MathComp
  • Infotheo finite distributions and expectation
  • Bignums binary arithmetic for bigQ execution
  • CoqEAL refinements for seqmx extraction
• Rocq/Coq namespace: Kalman
• Related publication(s): none

Building and installation instructions

To build and install manually, you need to make sure that all the libraries this development depends on are installed. The easiest way to do that is still to rely on opam:

git clone https://github.com/F1uctus/kalman.v.git
cd kalman.v
opam repo add rocq-released https://rocq-prover.org/opam/released
opam install --deps-only .
dune build -p kalman
dune install

Building the kalman package runs the verified seqmx programs inside Rocq and promotes paper/data/*.json for Typst figures. These JSON files are generated at build time and are not tracked in VCS.