checking a proof uses all its assumptions

Stream: Is there code for X?

[Edwin Agnew]

Is there code for a tactic which proves that some proof does or doesn’t use all of its assumptions?

For example, imagine someone writes a proof for a group that happens to not use the inverse assumption. Is there a way to automatically detect this so that a flag could be raised that the inverse assumption wasn’t used and therefore that proof is equally valid for a monoid?

In terms of what it means to use an assumption, it seems that tactics like by and show from are sufficient. Not sure what’s necessary because there’s probably edge cases like pmi

[Yakov Pechersky]

The linter does check if there are unused arguments

[Edwin Agnew]

And is there a way to access this linter or does it already raise a warning? I’m new to lean sorry

[Yakov Pechersky]

Try adding the #lint command below a lemma

[Yakov Pechersky]

import tactic

lemma foo (n : ℕ) : 2 = 1 + 1 := rfl
#lint
/-
/- The `unused_arguments` linter reports: -/
/- UNUSED ARGUMENTS. -/
#check @foo /- argument 1: (n : ℕ) -/
-/

[Edwin Agnew]

wow thats perfect! thanks :)

[Eric Wieser]

That doesn't really address your original question though

[Eric Wieser]

It won't detect that you wrote [group G] but only needed [monoid G], as the argument is still "used", just not all of it

[Yakov Pechersky]

Alex has a complex linter/tactic that does this search

[Eric Wieser]

@Alex J. Best's paper about that should be linked on the community website somewhere

[Eric Wieser]

There's probably a talk on YouTube too

[Stuart Presnell]

@Alex J. Best: "Automatically Generalizing Theorems Using Typeclasses" at Formal Mathematics for Mathematicians 2021.

[Stuart Presnell]

For example, Alex's linter detects that a comm_ring has been used in a lemma when it would be sufficient to use a comm_semiring.

[Eric Rodriguez]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/An.20example.20of.20why.20formalization.20is.20useful/near/278293462 has a list of these generalisations applied to mathlib (a while ago). maybe it'd be nice to rerun it on current mathlib!

[Riccardo Brasca]

I can do it, but it took a few days last time, so we need to wait.

[Alex J. Best]

I can also run it again sometime and post the output if people want, I keep hoping to improve it first/or at least fix the obvious bugs, but never seem to find the time

[Riccardo Brasca]

I am running it. The last version at https://github.com/alexjbest/lean-generalisation seems working

[Alex J. Best]

How many cores? I think it still recommends euclidean domain as better than comm_ring sometimes

[Alex J. Best]

So while most of the output is ok still there are still somethings not to be trusted :smile:

[Riccardo Brasca]

There are 16 cores in the computer I am using, and it is using all of them at the moment. If I remember correctly, last time at some point it switched to use only one core, after it produced the rubbish output at the beginning

[Riccardo Brasca]

The result is here

[Riccardo Brasca]

https://github.com/leanprover-community/flt-regular/blob/master/res

[Riccardo Brasca]

(it's in the flt project just because it was in a computer I can access using my phone and this was the easiest way to make it public)

[Riccardo Brasca]

Feel free to create a gist or whatever

[Yaël Dillies]

ordered_comm_semiring ↝ linear_ordered_semifield :thinking:

[Filippo A. E. Nuccio]

What is a linear_ordered_semifield?

[Yaël Dillies]

docs#linear_ordered_semifield. It's a linearly ordered field, but without negation. Typically, nnreal

[Filippo A. E. Nuccio]

and does it exist in nature? :palm_tree:

[Eric Rodriguez]

Yaël Dillies said:

ordered_comm_semiring ↝ linear_ordered_semifield :thinking:

the linter loves euclidean_domain

[Filippo A. E. Nuccio]

And the advantage out of ordered_comm_semiring is that you can divide easily?

[Yaël Dillies]

The linter is completely wrong here. linear_ordered_semifield implies ordered_comm_semiring, so it makes no sense to "weaken" the latter to the former.

[Eric Rodriguez]

gist: https://gist.github.com/ericrbg/b89109c674b3e04a8f708afa13357911

[Eric Rodriguez]

the original version is here, I've force-pushed flt-regular to keep the history clean

[Eric Rodriguez]

#16012, #16013, #16014 for some of these (I think #16014 will actually be very helpful!)

[Yaël Dillies]

Wow! I didn't think division monoids would actually help further than basic files!

[Alex J. Best]

The linear ordered field thing is probably the same as the Euclidean domain issue mentioned above. But I still haven't had time to look into it.

[Eric Rodriguez]

I wonder if these are broken classes because linear ordered semifield is the class that causes the olean bug

[Alex J. Best]

That seems unlikely to me but who knows, it could be relevant somehow. My best guess is that there something wrong with the type class graph it constructs, maybe some instance with many arguments that isn't interpreted properly