instance of `nontrivial unit`?

Stream: new members

[Eric Rodriguez]

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:

import algebra.ring.basic
import tactic

open unit

def unit_comm_ring : comm_ring unit := { add := λ _ _, star,
  add_assoc := by {intros, refl},
  zero := star,
  zero_add := by {intros, apply ext},
  add_zero := by {intros, apply ext},
  neg := λ _, star,
  sub := λ _ _, star,
  sub_eq_add_neg := by {intros, apply ext},
  add_left_neg := by {intros, apply ext},
  add_comm := by {intros, apply ext},
  mul := λ _ _, star,
  mul_assoc := by {intros, apply ext},
  one := star,
  one_mul := by {intros, apply ext},
  mul_one := by {intros, apply ext},
  left_distrib := by {intros, apply ext},
  right_distrib := by {intros, apply ext},
  mul_comm := by {intros, apply ext} }

lemma this_isnt_ok [comm_ring unit] {r s : unit} : r * s = s * r :=
begin
  show_term {nontriviality}, -- There is now a `nontrivial R` hypothesis available.
  apply mul_comm,
end

theorem what : true :=
begin
  have := @this_isnt_ok unit_comm_ring star star,
  trivial
end


-- the suggestion from `show_term`:
/- Try this: refine (subsingleton_or_nontrivial unit).dcases_on
  (λ (_inst : subsingleton unit), (id (propext (eq_iff_true_of_subsingleton (r * s) (s * r)))).mpr trivial)
  (λ (_inst : nontrivial unit),
     _[subsingleton_or_nontrivial unit, subsingleton_or_nontrivial unit, subsingleton_or_nontrivial unit, _inst]) -/

[Patrick Massot]

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]

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

[Patrick Massot]

That's the whole point of this tactic.

[Patrick Massot]

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

[Eric Rodriguez]

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]

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 ...