triv

Summary

The triv tactic proves ⊢ true.

It also proves goals of the form x = x and more generally of the form x = y when x and y are definitionally equal, but traditionally people use refl to do that.

Examples

If your goal is

⊢ true

then it’s pretty triv, so try triv.

Details

Note that true here is the true proposition. If you know a proof in your head that the goal is true, that’s not good enough. If your goal is ⊢ P and you can tell that P is true (e.g. because you can deduce it from the hypotheses), triv won’t work; triv only works when the goal is actually definitionally equal to ⊢ true.

Further notes

The split tactic also proves a true goal, although you would have to learn a bit about inductive types to understand why. Also triv solves a true gol in 3 millisends on a modern computer, whereas split takes 4 milliseconds.