Add tactic to solve decidable goals

It is surprisingly hard to find out how to solve a goal exploiting the fact that it is decidable:

apply (bool_decide_unpack _); by compute

IMO it would be a good idea to make that into a tactic. As usual the hardest part is figuring out how to call it. Or alternatively we could make done also do this, at which point the name basically would not matter.