Avoid circular instances

Stream: general

[Riccardo Brasca]

The instance docs#invariant_basis_number_of_nontrivial_of_comm_ring says that any nontrivial commutative ring satisfies the invariant_basis_number (what this means is irrelevant for my question), and docs#nontrivial_of_invariant_basis_number says that rings with this property are nontrivial. Is there a way of making the latter an instance and avoid circularity?

I am asking this linear_algebra.dimension because is full of [nontrivial R] [invariant_basis_number R], and technically the first assumption is implied by the second. Of course if this is not possible we can just refactor linear_algebra.dimension to use some letI in proofs.

[Anne Baanen]

I think there is no easy way in Lean 3: otherwise you'd get for a trivial comm_ring R a loop invariant_basis_number → nontrivial → .... Perhaps Lean 4's tabled typeclass resolution can help.

For now, the tactic#nontriviality might help to reduce the amount of copy-pasting letI := nontrivial_of_etc.

[Anne Baanen]

You might have to help the tactic by adding an appropriate lemma along the lines of:

@[nontriviality]
lemma not_subsingleton_of_invariant_basis_number {R : Type*} [invariant_basis_number R] :
  subsingleton R ↔ false := sorry

[Anne Baanen]

See also my thread on a loop ufm ↔ wf_dvd_monoid from a couple of days ago, which has the same characteristics.