IMTs in Coq: Model of IMTs and single fixed-pos implementation
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