coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Andrew Appel <appel AT princeton.edu>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] (Computationally) Efficient Finite Maps
Date: Thu, 14 May 2020 12:46:38 -0400 (EDT)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=appel AT princeton.edu; spf=Pass smtp.mailfrom=appel AT cs.princeton.edu; spf=Pass smtp.helo=postmaster AT greenlight.cs.princeton.edu
Ironport-phdr: 9a23:MvtqbBVbfU4S8amEMlGSgQLxjBjV8LGtZVwlr6E/grcLSJyIuqrYbByHt8tkgFKBZ4jH8fUM07OQ7/m9Hz1eqsff+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi2oAnLssQbgIRuJ6IwxxDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjg0+3zVhMNtlqJWuByvqRxhzYDXYo6VOudwcazBctMbQmRBQt1cWDZdDoygdYYCFfYNMOReooLgp1UOtxy+BQy0Ce7zzD9Hm2X20rM00u88DQzGxBQgEMwKsH/Jq9j6Lr8SUfirw6nM1jjDd+lW2Tb76IfUbB8hvfaMXbRqfcXP1EYvChrIg1ONooPqIz2bzP4Cs3SH7+V+T+KvjXYqpQF+rDSxycohlIvEi4YJxl3F9Sh13ok4KNKkRUN7btCpHpVdui6ZOoZrQs0vXmJltTokxrAFt5C2YDQGxZcnyhPZdveJcJCI7wr+WOqPIjp0nm9pdK+hixqo7EStxOzxWtO23VpUtiZJj9vBum4X2xDN9sSLUOVx8lqh1DqVyQzf9/9ILVgpmabFKJMt2KM8mocNvUjZAyP7lkf7gLWZe0k5/OWj9v7pba/8ppCGMo95kgH+Pboqmsy4Gek4PRIOUHaF9uS60L3j/EL5QLVWjvEsjqbZq4rWJdwBpq64BQ9azpgs6wq4DzegytgXg2QILE9ddBKGiYjmJU3OLejlAfuhgFmgiipny+3YMrH7H5nAIHnOnK3jcLpj80JczRA8zdFb55JaELEBJ/fzV1fru9zAFh82LQi0zv37B9VmzI8eQXiPAq6fMKzOr1CI+uUvI++WaIALpTn9NuAp5+Tygn8hhV8dYa6p0IMLZ3C/B/RqOlmWYX7xgtgaCmoKpQo/TOnyiFKYSzJTZnCyX7g95j4hEo6mA53DFciRh+mK2z7+FZlLbCgSAVeVVHzsao+sWvEWaSvULNU3wRIeUr30Yoktzxyx/Cbi07djZr7d4jUVsbr7ztlz7ODPkhd0+DBpWZfOm1qRRn15yztbDwQ927py9BQkmwWzlJNgivkdLuR9ovZAUwM0L5nZlrwoAMu0QhjAeNyEVFGgBNiqHGNoF45j85o1e094Xu6aoFXbxSPzXu0Njb2ND5Eo9aSa0nTsdZ4kliT2kZI5hlxjefNhcG2rgqklplrcHYPElUGYmKa2M68HmjbX9WGIwHaJugdVXBMiCKg=

The MSets interface of the Coq standard library factors the program from the proof, and may solve the problem that's being discussed here.

It was intended as a replacement for FSets and FMaps.

There had been a plan to make MMaps also (finite maps instead of sets), but unfortunately I don't think that was ever done.

There are efficient implementations of MSets for AVL trees and Red-Black trees in the standard library.

[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