overriding decidable instances

Stream: general

[Scott Morrison]

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

[Scott Morrison]

The implementation of nodup_decidable is too slow. :-)

[Simon Hudon]

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]

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]

decidable_prime has two implementations

[Mario Carneiro]

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]

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