coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] (Computationally) Efficient Finite Maps

From: Gregory Malecha <gmalecha AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] (Computationally) Efficient Finite Maps
Date: Wed, 13 May 2020 17:37:51 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f53.google.com
Ironport-phdr: 9a23:88v+9BQdGleTgcxv+Gpm40BaZNpsv+yvbD5Q0YIujvd0So/mwa6zZRGN2/xhgRfzUJnB7Loc0qyK6v2mCDBLuMvQ+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi2oAnLssQbjoRuJrsxxxbNv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/XrJgcJskq1UvBOhpwR+w4HKZoGVKOF+db7Zcd8DWGZNQtpdWylHD4y7coUPEvEBPf5GoIbhu1sAoxy+BQy2C+PuzD9Dm3v60KI+3ugkFwzNwQ4uEM8UsHnMo9r7NKkcX+OowqfW0TrOdOlZ1Svn5YXSbhwtvfOBULRtesTR00kvEAbFg02Rp4z/ITyV2eMNs3Kb7uF9UuygkWonpB9trTiv3Mgnl47Eho0Qyl/e8SV23po6Jd2iR0Ngbt6kFYFftyCeN4dsXswiRGRotT88x7YbtpG1YDIEx447xx7DdfOHaY6I7wr9WOuVJTp1hXJoda6/iRi870Ss1/PxWMew3VtIsCdIjMfAu3QN2hHT98SKSedw8luh1DuRygzf9OFKLEA1mKfYLZMq37A+lp0WsUvZHy/2nl37jKCXdkU4+uio9v/obq/npp+bMYJ/lwLwMrw2l8ChHeg1NhICUmub9OimybHv4070TK9Kg/A4lKTSrYrUKt4BpqGjBg9YyoYj5Ai7DzehyNkYmGMILFNBeB6egYnpPkzCLOn2Dfq/jVmgijhrx/fBPr3uBpXCMGLPn6vmfbZ480JcyQwzws5D559MFL0NPPb+VlXyudHYFBM1LhK4zuX9BNh92I4SQWePDbWYMKPWv1+I/OUvI+yUaY8avTbyMfwl6ODygn85g1AQZqap3Z4NZ3C5GvRqOVmWYX3pgtsZC2cFohI+TPD2iF2FSTNce3GyX7sl6j4nDIKmEJzMS5u2gL2B2Se7BodZanpHClCKC3fodp+LV+0CaCKIcYddlWkvUqHpYIs831n6vwjjjrFjM+D8+ysCtJul2sIjtMPJkhRn2iZ5AMOHwimoRmV5lWMBD2s52al7rEd9w3+M1KF5h7pTEtkFtKABaRszKZOJl78yMNv1QA+UO4rQEQf0cpCdGTg0C+kJ7ZoLakd5Fc+li0majSWvCr4R0beMAc5tq/+O7z3KP894jk3++uwhgl0hGJYdMGSngutg8lGWCdOS1UqekKmueOIX2yufrD7fn1rLh1lRVUtLaYuARWoWPxKEotHw50eERLirW+wq

Hello --

I am wondering what people suggest as an efficient representation of finite maps. Normally I use positive maps but for this purpose I have a *very* sparse key space so it actually makes sense to store pairs of the key and the element. The standard library has an implementation of AVL trees, but the proof term that is store with data is prohibitively expensive. Are there other implementations of finite maps that the community can recommend?

Thanks.

gregory malecha

gmalecha.github.io

[Coq-Club] (Computationally) Efficient Finite Maps, Gregory Malecha, 05/13/2020
- Re: [Coq-Club] (Computationally) Efficient Finite Maps, Frédéric Besson, 05/14/2020
- Re: [Coq-Club] (Computationally) Efficient Finite Maps, Alex Shkotin, 05/14/2020
- Re: [Coq-Club] (Computationally) Efficient Finite Maps, Xavier Leroy, 05/14/2020
  - Re: [Coq-Club] (Computationally) Efficient Finite Maps, Pierre-Marie Pédrot, 05/14/2020
    - Re: [Coq-Club] (Computationally) Efficient Finite Maps, Andrew Appel, 05/14/2020
      - Re: [Coq-Club] (Computationally) Efficient Finite Maps, Gregory Malecha, 05/14/2020
      - Re: [Coq-Club] (Computationally) Efficient Finite Maps, Hugo Herbelin, 05/14/2020
        
        Re: [Coq-Club] (Computationally) Efficient Finite Maps, Pierre Courtieu, 05/14/2020