Zulip Chat Archive

Stream: new members

Topic: instance of `nontrivial unit`?


view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 02 2021 at 13:40):

That's the whole point of this tactic.

view this post on Zulip Patrick Massot (Apr 02 2021 at 13:40):

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

view this post on Zulip 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

view this post on Zulip 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