## Stream: new members

### Topic: instance of nontrivial unit?

#### Eric Rodriguez (Apr 02 2021 at 13:33):

I'm very confused by docs#tactic.interactive.nontriviality. One of the examples it gives is:

example {R : Type} [comm_ring R] {r s : R} : r * s = s * r :=
begin
nontriviality, -- There is now a nontrivial R hypothesis available.
apply mul_comm,
end


But we can easily give unit a comm_ring structure (see below), so why are we allowed to have this assumption? If I change the goal to anything else (e.g. nontrivial R) and then use nontriviality R, it complains that it can't discount subsingleton R (which is very sensible!), and if I try show_term it gives me a term that I cannot get to work. Meanwhile, if I change it just to [comm_ring unit] {r s : unit}, we have a term in the proof state of nontrivial unit, which seems like a contradiction; but I don't know where. What is going on?!

All code below the fold:

#### Patrick Massot (Apr 02 2021 at 13:38):

The tactic is doing its job in:

example {R : Type} [comm_ring R] {r s : R} : r * s = s * r :=
begin
nontriviality, -- There is now a nontrivial R hypothesis available.
apply mul_comm,
end


It does a case disjunction: either the ring is trivial and then r*s and s*r are the same because the ring has only one element, or it is not trivial and you get to finish the proof using this nontriviality extra assumption.

#### Eric Rodriguez (Apr 02 2021 at 13:39):

riight so the tactic also solves the goal itself in the case of subsingleton R! that makes a lot of sense, thanks

#### Patrick Massot (Apr 02 2021 at 13:40):

That's the whole point of this tactic.

#### Patrick Massot (Apr 02 2021 at 13:40):

I'm exaggerating a bit, it also tries to infer nontrivility from context

#### Eric Rodriguez (Apr 02 2021 at 13:41):

I only understood it as inferring nontriviality from context; the previous example was that 0 < a and so that instantly gives you nontrivial R. This is a lot cleverer

#### Bryan Gin-ge Chen (Apr 02 2021 at 13:43):

The last paragraph in the docstring before the examples describes the behavior here:

Otherwise, it will perform a case split on subsingleton α ∨ nontrivial α, and attempt to discharge the subsingleton goal using ...

Last updated: May 11 2021 at 12:15 UTC