feat(tactic/core): derive handler for simple instances

[robertylewis]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/deriving.20instances

This is a simple derive handler for adding instances that can be found just by unfolding a new definition.

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[cipher1024]

This is a good idea but the name is wrong. It is very much inline with Haskell's DeriveNewtype extension, that is deriving instances for type synonyms. Whether it is algebraic or not should not matter.

[robertylewis]

I changed the PR title and doc string to remove the word "algebraic."

[cipher1024]

Good :) Why do you make the definition of the instance an abbreviation?

[robertylewis]

Oh, no good reason. I don't know what the default values for reducibility_hints.regular are, do you?

[cipher1024]

I would use mk_definition in init/meta/declaration.lean as an exemplar. It uses 1 and tt.

[robertylewis]

Changed to use mk_definition directly.