refactor(init/data/string/*): implement decidable equality for strings without using tactics

[JLimperg]

The decidable equality instance for strings
(string.has_decidable_equality) was previously defined via the
mk_dec_eq_instance tactic. However, we'd like to be able to use this
instance in init.meta.*, which creates import cycles. This commit
therefore reimplements the instance without using tactics.

[JLimperg]

This change is fully backwards-compatible unless someone imports init.data.string.instances directly (and why would you?). Should I still write a changes entry?

[gebner]

LGTM. The only important thing is that the decidability instance still has exactly the same name and type, because it is override in the VM.

If somebody imports init.data.string.instances, they're on their own.