Zulip Chat Archive

Stream: general

Topic: overriding decidable instances


view this post on Zulip Scott Morrison (Sep 22 2018 at 06:02):

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

view this post on Zulip Scott Morrison (Sep 22 2018 at 06:03):

The implementation of nodup_decidable is too slow. :-)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 22 2018 at 06:11):

decidable_prime has two implementations

view this post on Zulip 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

view this post on Zulip 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: May 11 2021 at 22:14 UTC