[Merged by Bors] - feat(tactic/dec_trivial): make dec_trivial easier to use

[jcommelin]

---

This PR is motivated by the fin 3 "issues" in #3872

[robertylewis]

Module doc please! Alternatively, I know we're generally moving away from the monolithic tactic.interactive, but since the copyright and module doc boilerplate will be longer than the content of this file, you could just stick the important bit in there.

[robertylewis]

Unfortunately this kind of reversion can also change a trivial goal into a non-trivial goal, e.g.:

import tactic.dec_trivial

example (n : ℕ) : (0 : fin (n+1)) + 0 = 0 :=
dec_trivial -- good 
-- by dec_trivial -- bad

So by dec_trivial isn't a drop-in replacement for dec_trivial. Maybe the behavior should be

• by dec_trivial is the same as term mode, e.g. tactic.exact_dec_trivial
• by dec_trivial! is what you've implemented
  ?

[robertylewis]

I'm happy, but let's see if anyone else has opinions about the ! syntax.

[fpvandoorn]

It's a bit weird that dec_trivial! is not strictly stronger than dec_trivial, but I think it's fine like this.
LGTM.

[robertylewis]

The alternative, which Johan suggested, is implementing tactic.interactive.dec_trivial := exact_dec_trivial <|> revert_dec_trivial. But this has bad behavior when the proposition is decidable, expensive to decide, false, and irrelevantly depends on a variable, e.g. something like

example (b : bool) : function.const _ 10000 b = 10001

[jcommelin]

@digama0 🏓

[digama0]

Works for me. I like the currently implemented behavior, where ! makes it revert first (and is not the default), and don't mind that it doesn't subsume the other version, after all the user can pick whichever one works and I like it when lean doesn't have to guess when the wrong guess is possibly costly.

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests