Skip to content

IMTs in Coq: Model of IMTs and single fixed-pos implementation

Germán Delbianco requested to merge germanD@experiments into master

Implements #2 (closed) and #3 (closed).
See #1 (closed) for more details

This new MR splits the development of the model of IMTs, their canonical API, and the single commitment, optimizing position-correcting implementation (#3 (closed)).

IMT Model:

  • Internal model of IMTs using binary trees
  • Implemental_spec and related properties and lemmas.
  • Rename: Incremental -> Left leaning
  • Canonical API over trees (insert, get, iter_insert)
  • External model for IMTs (Sigma Type)
  • External API over IMTs (add, iter_add, get) and properties
  • Rename Library from IMT experiments to IMT.

IMT Implementations

  • Single insert, fixed-position implementation #3 (closed)
  • Improve doc

Reviewers: @ZaynahDargaye @clarus1 @paracetamolo

Edited by Germán Delbianco

Merge request reports