nontriviality

Stream: metaprogramming / tactics

[Riccardo Brasca]

If I use nontriviality here
https://github.com/leanprover-community/mathlib/blob/0c90c3ed1b520b34a37d12eddc6e74868e5ed97e/src/linear_algebra/basis.lean#L294
it produces automatically an instance nontrivial M (here M is a module over a semiring R). This in turn implies nontrivial R (that is what I need), via docs#module.subsingleton. Is it possible to have nontriviality to do this for me? Note that I know exactly nothing about tactic writing, so this can be nonsense/very easy.

[Anne Baanen]

I haven't used nontriviality a lot, but I believe from the docs at docs#tactic.interactive.nontriviality that nontriviality R will get you the nontrivial R instance.

[Anne Baanen]

I have to go to bed soon, but I can take a closer look at it tomorrow if no one else wants to be first :)

[Riccardo Brasca]

Thanks!nontriviality R says Could not prove goal assuming subsingleton R. But note that my question has nothing to do with this specific goal, nontriviality is able to produce nontrivial M, and this always implies nontrivial R.

[Kevin Buzzard]

import algebra.module.basic

variables (R : Type) [ring R] (M : Type) [add_comm_group M] [module R M]

@[nontriviality] instance ring.nontrivial_of_nontrivial_module [hM : nontrivial M] : nontrivial R :=
classical.by_contradiction (λ hR,
  not_subsingleton M (@semimodule.subsingleton R M _ (not_nontrivial_iff_subsingleton.1 hR) _ _))

example [nontrivial M] : R ≠ R := by nontriviality R; sorry -- _inst : nontrivial R appears

[Eric Wieser]

Does that work without instance?

[Riccardo Brasca]

I am playing with this, and it doesn't seem to work without instance.

[Riccardo Brasca]

But adding this instance creates random problems elsewhere

[Kevin Buzzard]

What are the nature of the problems? One can give a constructive proof, it's just longer.

[Eric Wieser]

It's a dangerous instance just like docs#module.subsingleton

[Eric Wieser]

(but we should definitely add it as a lemma if we don't already have docs#module.nontrivial)

[Riccardo Brasca]

The first problem I get is in algebra/module/ordered, in the proof of ordered_module.mk'': no real errors, but there are unsolved goals.
Essentially the final goal is 0 < 1, but exact zero_lt_one says
maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

[Riccardo Brasca]

This seems to me a bad sign

[Anne Baanen]

Would it work to say a local attribute [instance] module.nontrivial only in the file you need it?

[Riccardo Brasca]

For my proof it is even simpler, nontriviality creates nontrivial M, and so I can use Kevin's lemma with a letI by hand.

[Eric Wieser]

I think the solution here is to teach docs#tactic.nontriviality_by_assumption about module.nontrivial

[Eric Wieser]

Right now it does:

apply_instance <|> `[solve_by_elim [nontrivial_of_ne, nontrivial_of_lt]]

If you could add module.nontrivial to that list I expect it would work; although obviously you'd need a mechanism to register the lemma from elsewhere