Zulip Chat Archive

Stream: general

Topic: overriding decidable instances


Scott Morrison (Sep 22 2018 at 06:02):

Can someone point me to an example of overriding a decidable instance with a faster algorithm?

Scott Morrison (Sep 22 2018 at 06:03):

The implementation of nodup_decidable is too slow. :-)

Simon Hudon (Sep 22 2018 at 06:09):

You create your own instance and you give it higher priority than nodup_decidable. Is this for lists? Be sure that the culprit nodup_decidable and not the fact that comparing objects (e.g. nat) is slow

Simon Hudon (Sep 22 2018 at 06:10):

One more consideration: is this for a proof or for a program? If it's for a proof, you can write a tactic that does the comparison faster.

Mario Carneiro (Sep 22 2018 at 06:11):

decidable_prime has two implementations

Mario Carneiro (Sep 22 2018 at 06:17):

For checking nodup of big things like those lists of numbers, it helps if you've put them in order. list.chain is linear time

Mario Carneiro (Sep 22 2018 at 06:29):

Oh, wait this doesn't work for cycles, since the order matters. You can still improve on the n^2 performance of the default implementation by utilizing the order. If you sort the list then you can check for duplicates in linear time


Last updated: Dec 20 2023 at 11:08 UTC