coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] (Computationally) Efficient Finite Maps

From: Alex Shkotin <alex.shkotin AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] (Computationally) Efficient Finite Maps
Date: Thu, 14 May 2020 14:04:21 +0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=alex.shkotin AT gmail.com; spf=Pass smtp.mailfrom=alex.shkotin AT gmail.com; spf=None smtp.helo=postmaster AT mail-qv1-f49.google.com
Ironport-phdr: 9a23:DOZsMhCInP+0aF/mqMNbUyQJP3N1i/DPJgcQr6AfoPdwSPT8osbcNUDSrc9gkEXOFd2Cra4d1qyH7eu7AyQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagYb5+NhG7oATeusQYn4dpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLvhykaKj4563nXhdJsg6JHrhyhoBl/zJTVYIGTKfFyeqzQcNcfSWdHQ81fVTFOApmkYoQAAeoOP+ZWoYf+qVUTsxWxGRKhC/nzxjJSnHL6wbE23uYnHArb3AIgBdUOsHHModjpMKcdT++0x7TVwzXDbPNW3iv96InOchs8pvyDR7ZwftTeyEU1DAPFjlaQqYv5PzOU0OQAqGeb7+96WuKuj24rsR1+oj+qxso1jITCm40axEze+ypj3IY1OcO3SFR9YdO8DZZeuC+XOYt4T84hQGxluCY0x7IJtJC0YSUExoorygLRZfGbb4SG4g7uWeWPLTp2gH9odrCyihes/UWuyuDyWM+520tEoCpCl9nDrHEN1xrL58iIS/t94keh2SuU2AzJ6+FEJkY5nrfYJZ452rM8iIYfvEDZEiL1mEj6lrGaelgg9+Sy5OnqZrPrrYKGOYBukAHxKKEul9S/AesmNggOWHCW+eGm273i+U31WaxKjuMrnqXAvpDXKsAWqrS2Aw9S1YYj5BK/ACm83NsEmnkHKUpJeBOBj4f3J1HDOO70Aeu7jli2kzpmx+rKMqP8DpjJNHTOn7Psca5460FGyQozyd5f54hTCrEEOP/8QEvxu8LXDxMjKAy0w+XnCNJh1oMfX2KCGaCZMKbIvl+J4uIjOfWDZIgQuDrlMfgq++bujWMlmV8aZaSmwZwXaGmhEvt6J0WZfGHjj8waEWYKuwo+VPblhEeDUT5VfXayXrgz6is1CIK8Xs//QdWmh6XE1yOmFLVXYHpHAxaCCyTGbYKBDt4IZTLaGc9ilSAFU/D1QossxVe1tAz917thBuXR8ywc85nk0Y4mtKXoiRgu+GksXIym2GaXQjQozzpVFQ9z57h2pAlG8nnG0aV8hKYFR9la5vcMSxljcJCAnqp1DNf9Xg+HddCMGg7/HoeWRAopR9d0+OcgJl5nEoz73B/G1iuuRbQSku7TXc1mwufnx3H0Yv1F5TPD3aglgUMhR5IWZ2Kjj697sQPUAtyQng==

Hi, Gregory & All!

Gregory, may I add my question by reformulating yours: I am wondering what people suggest as an efficient representation of finite algebraic systems.

Alex

чт, 14 мая 2020 г. в 00:39, Gregory Malecha <gmalecha AT gmail.com>:

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