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):
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: May 11 2021 at 22:14 UTC