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

• compact_data_structures.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

Compilation

1. coq_makefile -f _CoqProject -o Makefile
2. make

Requirements

• Coq 8.9.1
• MathComp 1.9.0

Accompanying material

• Most recent draft paper (arXiv version)
• TPP 2018 slides for LOUDS and dynamic bit vectors
• JSSST 2018 draft paper