✔ Counting operations used by a function · Coq users

Stream: Coq users

Topic: ✔ Counting operations used by a function

Malcolm Sharpe (Sep 09 2022 at 03:36):

Let's say I want to prove a bound on the number of a certain operation used by a function (such as proving a bound on the number of comparisons used by a sorting algorithm). What techniques/libraries should I be considering for doing that?

Paolo Giarrusso (Sep 09 2022 at 04:05):

Bounds about a specific algorithm are one kind of problem; bounds about a class of algorithms are a different problem. https://coq.discourse.group/t/trying-to-prove-sort-algorithm-correctness-for-specific-n-in-search-for-hints/1076/11?u=blaisorblade is relevant to the second.

Mukesh Tiwari (Sep 09 2022 at 09:29):

@Malcolm Sharpe Have a look at this thread [1].

[1] https://sympa.inria.fr/sympa/arc/coq-club/2022-07/msg00008.html

Malcolm Sharpe (Sep 09 2022 at 16:38):

Thanks for the links. My conclusions:

Monads are the tool of choice (if you're doing a shallow embedding).
There is a variety of public code available, though none of it actively maintained.

(This made me curious what's the most accessible library for monads in Coq, and that seems to be coq-ext-lib, which is in coq-platform.)

Notification Bot (Sep 09 2022 at 16:38):

Malcolm Sharpe has marked this topic as resolved.

John Wiegley (Sep 09 2022 at 16:54):

I’d like to offer that I’m working on a new sub-library for my category-theory library that aims to make Monads very easy to work with in Coq, while leveraging the power of the larger library when proving that some construction is, in fact, a lawful Monad.

Last updated: Oct 05 2023 at 02:01 UTC