Compact data structures in Coq

A tentative formalization of compact data structures following [1]

[1] Gonzalo Navarro, Compact Data Structures---A Practical Approach, Cambridge University Press, 2016

Files

• tree_traversal.v
• rank_select.v
• jacobson_rank_complexity.v
• pred_succ.v
• louds.v
• insert_delete.v
• set_clear.v
• dynamic_redblack.v
• dynamic_dependent_program.v
• dynamic_dependent_tactic.v

Requirements

• Coq 8.12.1
• MathComp 1.11.0 or 1.12.0

Compilation

1. git clone [email protected]:affeldt-aist/succinct.git
2. cd succinct

If the Requirements (see above) are already met, do:

3. coq_makefile -f _CoqProject -o Makefile
4. make

Or, if opam is installed, do:

3. opam install .

opam takes care of the dependencies.

License

MIT

External Axioms

We do not explicitly introduce any additional axioms. However, dynamic_dependent_program.v and (to a lesser extent) dynamic_dependent_tactic.v uses the Program framework and thus implicitly depends on Coq.Logic.JMEq.JMEq_eq, which is in turn equivalent to Streicher's Axiom K (i.e., dependent pattern matching).

Accompanying material

• Most recent paper (arXiv version), presented at the 10th International Conference on Interactive Theorem Proving (ITP 2019)
• ITP 2019 slides
• TPP 2018 slides for LOUDS and dynamic bit vectors
• JSSST 2018 draft paper
• Earlier papers:
  • "Formal Verification of the rank Algorithm for Succinct Data Structures", in 18th International Conference on Formal Engineering Methods (ICFEM 2016)
  • "Safe Low-level Code Generation in Coq Using Monomorphization and Monadification", in Journal of Information Processing, vol. 26 (2018)