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.