Locating defeq abuse

Stream: mathlib4

[Daniel Weber]

I want to detect all places across mathlib where a certain type (ENat) is defeq-abused, which for this purpose we can define as "a defeq check which would've failed had ENat been @[irreducible]". However, I don't want this to block later uses which depend it, so I want the check to succeed, just log it somewhere.
What would be a good way to do this?

[Kevin Buzzard]

Just make it irreducible in a PR and then fix CI by writing unseal PNat in in front of every declaration that fails?

[Daniel Weber]

That'll likely take many iterations, could that be automated somehow?

[Damiano Testa]

As you might imagine, I would suggest a linter: you make the linter re-elaborate every declaration prefixing it with attribute [irreducible] ENat (untested, I'm not sure this would work), and report failures using a try ... catch for instance.

[Damiano Testa]

This is slightly tricky, since re-elaborating will have to happen changing the name of the declaration and I don't have a "good" solution to this, just approximate hacks.

[Daniel Weber]

Do you happen to have an example linter re-elaborating all declarations I could adapt?

[Damiano Testa]

Not at a computer now, but an easy way is to re-elaborate the syntax inside a withScope adding an extra namespace. Not all build failures will be what you want, but most of them should!

[Daniel Weber]

I have no idea how to write a linter - which mathlib linter would be best as a model for this?

[Damiano Testa]

I'll be unable to help for a few hours, but will try once I'm back. Otherwise, ping me again tomorrow and I'll do it then! :smile:

[Damiano Testa]

#17715 does something similar for certain declarations (theorems and lemmas), but also does a bunch of other things, so you can ignore quite a bit of that linter.

[Damiano Testa]

#19177 is a prototype, but I have done very few checks to make sure that it does, at least usually, the right checks!

[Daniel Weber]

Thanks!

[Daniel Weber]

Hmm, making ENat an @[irreducible] isn't strong enough in some cases, for example here

import Mathlib

attribute [local irreducible] ENat

lemma test (k : ℕ) : (k : ℕ∞) < ((k + 1 : ℕ) : ℕ∞) := WithTop.coe_lt_coe.2 (Nat.lt_succ_self _)

Is there a way to simulate it being opaque?

[Daniel Weber]

That should be possible by directly modifying the Environment, right? Replacing the defnInfo with a opaqueInfo. How badly should I expect things to break, doing that?

[Daniel Weber]

Hmm, even that doesn't help -- the problematic thing which gets unfolded here is one of ENat's instances, not ENat itself

[Damiano Testa]

I think that modifying the environment will be much harder.

[Daniel Weber]

I tried doing that, it doesn't even help

[Daniel Weber]

Daniel Weber said:

Hmm, even that doesn't help -- the problematic thing which gets unfolded here is one of ENat's instances, not ENat itself

Making ENat opaque means that the expression obtained by unfolding something using it will be type incorrect, but the equality test can just ignore that

[Daniel Weber]

I see there's recordUnfold, is there a way to see it specifically?

[Daniel Weber]

(deleted)

[Daniel Weber]

Using set_option diagnostics true works, I'll check if I can incorporate it to the linter

[Daniel Weber]

I'm trying to use docs#Lean.withOptions to do the elabCommand with the appropriate options, but I'm getting a failed to synthesize MonadWithOptions CommandElabM error message. What is the correct way to do this?

[Jannis Limperg]

You can probably just add this instance locally. Many sensible instances are not declared because core hasn't needed them yet.

[Jannis Limperg]

You can also elabCommand $ <- `(command| set_option diagnostics true), now that I think about it.

[Daniel Weber]

I think I found how I can do this, it can just be modified in withScope

[Damiano Testa]

Btw, I do not know if you were already planning to do this, but feel free to push directly to the PR! I tried to put a single entry-point for the declaration to inspect, so that, if this turns out to be useful, a similar diagnostic could be run on other declaration. Other than that, I don't think that I had any other specific design constraints.

[Daniel Weber]

I made #19372. I can merge it to the PR, I think

[Damiano Testa]

It's ok, whatever is more convenient!

[Daniel Weber]

In https://github.com/leanprover-community/mathlib4/blob/bcfe9ac8ef66da2223bd327a912e8a9b2634e434/Mathlib/Tactic/Linter/FindDefEqAbuse.lean#L85-L90 I'm trying to figure out if the definition is data or a proof, but it's misfiring on docs#multiplicity, thinking it's a proof. What could be the cause of that? Is there a better approach to take? I don't think it can be figured out just from the syntax, as I want it to work for instance which can be both a Prop and a Type _

[Jannis Limperg]

There's a function for this: docs#Lean.Meta.isProof

[Daniel Weber]

I think it can't find the name in the environment in the linter, but I'm not sure why

[Daniel Weber]

I'm having trouble understanding what's going on here:

import Mathlib

set_option diagnostics true
set_option diagnostics.threshold 1

theorem test {N : ℕ∞} {n : ℕ} (hn : ↑(n + 1) ≤ N) : ↑n < N :=
  (Nat.cast_lt.mpr n.lt_add_one).trans_le hn

why is ENat unfolded 114 times? I assume it happens during typeclass inference, but I don't see what could cause it to be unfolded - I thought typeclass inference only unfolds instances and abbrevs?