dsimpNF

Stream: mathlib4

[Kim Morrison]

@Johan Commelin et al, here is the output from the new simpNF linter on Mathlib.

[Kim Morrison]

(There are failures.)

[Kim Morrison]

I think maybe we should revert the Batteries change, make a new PR, and sort out the Mathlib failures by pointing a branch of Mathlib at the branch.

[Johan Commelin]

Ok, I guess that's a better path forward.

[Johan Commelin]

@Kim Morrison Here's a PR for the revert: batteries#841

[Damiano Testa]

I am trying out #13793 for the syntax linter deprecating "no since" deprecated.

To be honest, my main motivation is to practice self-correcting code, rather than the linter itself: I would like to add a step that automatically adds the since part, wherever the linter flags a warning.

[Johan Commelin]

Here is a batteries-free MWE of the first dsimpNF complaint:

section Equiv

variable {α β : Type}

/-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
structure Equiv (α β : Type) where
  protected toFun : α → β
  protected invFun : β → α

@[inherit_doc]
infixl:25 " ≃ " => Equiv

/-- Inverse of an equivalence `e : α ≃ β`. -/
@[symm]
protected def Equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩

end Equiv

variable {M N : Type} [Mul M] [Mul N]

section MulHom

/-- `M →ₙ* N` is the type of functions `M → N` that preserve multiplication. -/
structure MulHom (M N : Type) [Mul M] [Mul N] where
  protected toFun : M → N
  protected map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y

/-- `M →ₙ* N` denotes the type of multiplication-preserving maps from `M` to `N`. -/
infixr:25 " →ₙ* " => MulHom

end MulHom

/-- `MulEquiv α β` is the type of an equiv `α ≃ β` which preserves multiplication. -/
structure MulEquiv (M N : Type) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N

/-- Notation for a `MulEquiv`. -/
infixl:25 " ≃* " => MulEquiv

namespace MulEquiv

/-- The inverse of an isomorphism is an isomorphism. -/
def symm (e : M ≃* N) : N ≃* M :=
  ⟨e.toEquiv.symm, sorry⟩

namespace MulEquiv

theorem symm_mk' (f f') (h) :
    (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm =
      {(⟨⟨f, f'⟩, h⟩ : M ≃* N).symm with
        toFun := f'
        invFun := f } :=
  rfl

theorem works_as_expected (f f') (h) :
    (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm =
      {(⟨⟨f, f'⟩, h⟩ : M ≃* N).symm with
        toFun := f'
        invFun := f } := by
  simp? only [symm_mk'] -- succeeds

/--
error: tactic 'simp' failed, nested error:
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
-/
#guard_msgs in
theorem fails_as_unexpected (f f') (h) :
    (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm =
      {(⟨⟨f, f'⟩, h⟩ : M ≃* N).symm with
        toFun := f'
        invFun := f } := by
  dsimp only [symm_mk'] -- fails, but `symm_mk'` is a rfl lemma

end MulEquiv

[Notification Bot]

7 messages were moved here from #mathlib4 > Technical Debt Counters by Johan Commelin.

[Johan Commelin]

I haven't looked into the others. But it seems to me that this is maybe just a bad lemma to begin with?

[Johan Commelin]

@Eric Wieser do you have an idea whether symm_mk' is desirable or not?

[Eric Wieser]

My guess here is that dsimp is recursing into the proof fields

[Eric Wieser]

At first glance the lemma looks suspicious because the LHS contains the RHS, but in fact this loop only happens within the proofs which should be ok.

[Johan Commelin]

But do we want to have lemmas like this in our default simp-set? From that angle it still looks very suspicious to me.

[Eric Wieser]

This works fine:

def symm_mk'.aux (f f') (h) := (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm.map_mul'

theorem symm_mk' (f f') (h) :
    (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm =
      { toFun := f'
        invFun := f
        map_mul' := symm_mk'.aux f f' h } :=
  rfl

[Eric Wieser]

So I claim that either this is a dsimp bug; or that there should be some way to generate symm_mk'.aux automatically to protect its contents from dsimp

[Johan Commelin]

Updated version of the MWE, displaying the two versions: the MWE coming from mathlib, and Eric's workaround.

section Equiv

variable {α β : Type}

/-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
structure Equiv (α β : Type) where
  protected toFun : α → β
  protected invFun : β → α

@[inherit_doc]
infixl:25 " ≃ " => Equiv

/-- Inverse of an equivalence `e : α ≃ β`. -/
@[symm]
protected def Equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩

end Equiv

variable {M N : Type} [Mul M] [Mul N]

section MulHom

/-- `M →ₙ* N` is the type of functions `M → N` that preserve multiplication. -/
structure MulHom (M N : Type) [Mul M] [Mul N] where
  protected toFun : M → N
  protected map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y

/-- `M →ₙ* N` denotes the type of multiplication-preserving maps from `M` to `N`. -/
infixr:25 " →ₙ* " => MulHom

end MulHom

/-- `MulEquiv α β` is the type of an equiv `α ≃ β` which preserves multiplication. -/
structure MulEquiv (M N : Type) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N

/-- Notation for a `MulEquiv`. -/
infixl:25 " ≃* " => MulEquiv

namespace MulEquiv

/-- The inverse of an isomorphism is an isomorphism. -/
def symm (e : M ≃* N) : N ≃* M :=
  ⟨e.toEquiv.symm, sorry⟩

namespace MulEquiv

namespace case1 -- MWE from mathlib

-- lemma similar to something in mathlib
theorem symm_mk (f f') (h) :
    (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm =
      {(⟨⟨f, f'⟩, h⟩ : M ≃* N).symm with
        toFun := f'
        invFun := f } :=
  rfl

attribute [local simp] symm_mk -- leads to breakage
-- attribute [simp] symm_mk' -- works

theorem works_as_expected (f f') (h) :
    (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm =
      {(⟨⟨f, f'⟩, h⟩ : M ≃* N).symm with
        toFun := f'
        invFun := f } := by
  simp -- succeeds

/--
error: tactic 'simp' failed, nested error:
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
-/
#guard_msgs in
theorem fails_as_unexpected (f f') (h) :
    (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm =
      {(⟨⟨f, f'⟩, h⟩ : M ≃* N).symm with
        toFun := f'
        invFun := f } := by
  dsimp -- fails, but `symm_mk'` is a rfl lemma

end case1

namespace case2 -- workaround by Eric Wieser

-- aux lemma for `symm_mk'`
theorem symm_mk'.aux (f f') (h : ∀ x y, f (x * y) = f x * f y) (x y : N) :
    (⟨f, f'⟩ : M ≃ N).symm.toFun (x * y) =
      (⟨f', f⟩ : N ≃ M).toFun x * (⟨f', f⟩ : N ≃ M).toFun y :=
  (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm.map_mul' _ _

-- variant of `symm_mk` above, but this one does not cause problems
theorem symm_mk' (f f') (h) :
    (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm =
      { toFun := f'
        invFun := f
        map_mul' := symm_mk'.aux f f' h } :=
  rfl

attribute [local simp] symm_mk' -- works

theorem works_as_expected (f f') (h) :
    (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm =
      {(⟨⟨f, f'⟩, h⟩ : M ≃* N).symm with
        toFun := f'
        invFun := f } := by
  simp -- succeeds

theorem does_not_fail (f f') (h) :
    (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm =
      {(⟨⟨f, f'⟩, h⟩ : M ≃* N).symm with
        toFun := f'
        invFun := f } := by
  dsimp

end case2

end MulEquiv

[Eric Wieser]

Is there some elaborator foo% x which means "create an auxiliary declaration with value x, and reference it here"?

[Johan Commelin]

Johan Commelin said:

But do we want to have lemmas like this in our default simp-set? From that angle it still looks very suspicious to me.

Nevertheless :this:

[Eric Wieser]

I think the lemma is very reasonable to have in the dsimp set

[Eric Wieser]

⟨⟨f, f'⟩, h⟩ : M ≃* N).symm is clearly less simple than ⟨⟨f', f⟩, h2⟩ : M ≃* N)

[Eric Wieser]

The fact that h2 is a mess should be irrelevant, it's a proof term

[Johan Commelin]

But I think you should compare

 { toFun := f, invFun := f', map_mul' := h }.symm
-- vs
let __src := { toFun := f, invFun := f', map_mul' := h }.symm;
  { toFun := f', invFun := f, map_mul' := ⋯ }

Maybe that let expression shouldn't appear in the RHS of a dsimp lemma.

[Johan Commelin]

In Lean 3 there was a tactic dsimp_result, which might have been handy here.

[Matthew Ballard]

What happens if you manually expand the RHS and change __src to src?

[Johan Commelin]

Like so?

theorem symm_mk (f f') (h) :
    (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm =
      let src := (⟨⟨f, f'⟩, h⟩ : M ≃* N).symm;
  { toFun := f', invFun := f, map_mul' := src.map_mul' } :=
  rfl

Same problem...

[Eric Wieser]

The let is a distraction here, the problem persists if you inline the src

[Johan Commelin]

#13804 fixes some of these lemmas: dsimp visits proof subterms for a good reason

[Matthew Ballard]

To keep things well typed?

[Johan Commelin]

To get rid of artificial dependencies

[Johan Commelin]

Here is another mystery

variable {R M : Type}

class Zero (α : Type) where
  zero : α

instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

/-- Typeclass for the `⊥` (`\bot`) notation -/
class Bot (α : Type) where
  /-- The bot (`⊥`, `\bot`) element -/
  bot : α

/-- The bot (`⊥`, `\bot`) element -/
notation "⊥" => Bot.bot

/-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
class SMul (M α : Type) where
  smul : M → α → α

infixr:73 " • " => SMul.smul

structure Submodule (R : Type) (M : Type) [Zero M] [SMul R M] where
  carrier : M → Prop
  zero_mem : carrier (0 : M)

variable [Zero M] [SMul R M]

instance : Bot (Submodule R M) where
  bot := ⟨(· = 0), rfl⟩

instance : Zero (Submodule R M) where
  zero := ⊥

@[simp]
theorem zero_eq_bot : (0 : Submodule R M) = ⊥ :=
  rfl

theorem ohai : (0 : Submodule R M) = ⊥ := by simp -- works

/-- error: dsimp made no progress -/
#guard_msgs in
theorem oops : (0 : Submodule R M) = ⊥ := by dsimp -- fails

[Johan Commelin]

Simpler:

class Zero (α : Type) where
  zero : α

instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

/-- Typeclass for the `⊥` (`\bot`) notation -/
class Bot (α : Type) where
  /-- The bot (`⊥`, `\bot`) element -/
  bot : α

/-- The bot (`⊥`, `\bot`) element -/
notation "⊥" => Bot.bot

variable {α : Type} [Zero α]

structure copy (α : Type) where
  val : α

instance : Bot (copy α) where
  bot := ⟨0⟩

instance : Zero (copy α) where
  zero := ⊥

@[simp]
theorem zero_eq_bot : (0 : copy α) = ⊥ :=
  rfl

theorem ohai : (0 : copy α) = ⊥ := by simp -- works

/-- error: dsimp made no progress -/
#guard_msgs in
theorem oops : (0 : copy α) = ⊥ := by dsimp -- fails

[Eric Wieser]

OfNat is to blame here, everything works with Zero.zero

[Eric Wieser]

Specifically, the builtin OfNat is special-cased internally, and that breaks things

[Eric Wieser]

It works fine if you roll your own:

class Zero (α : Type) where
  zero : α


/-- Typeclass for the `⊥` (`\bot`) notation -/
class Bot (α : Type) where
  /-- The bot (`⊥`, `\bot`) element -/
  bot : α

/-- The bot (`⊥`, `\bot`) element -/
notation "⊥" => Bot.bot

variable {α : Type} [Zero α]

structure copy (α : Type) where
  val : α

instance : Bot (copy α) where
  bot := ⟨Zero.zero⟩

instance : Zero (copy α) where
  zero := ⊥

class MyOfNat (α) (n : Nat) where
  ofNat : α

instance (priority := 300) Zero.toMyOfNat0 {α} [Zero α] : MyOfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

@[simp]
theorem zero_eq_bot : (MyOfNat.ofNat (nat_lit 0) : copy α) = ⊥ :=
  rfl

@[simp]
theorem zero_eq_bot' : (OfNat.ofNat (nat_lit 0) : copy α) = ⊥ :=
  rfl

theorem ohai : (MyOfNat.ofNat (nat_lit 0) : copy α) = ⊥ := by dsimp -- works

theorem oops : (OfNat.ofNat (nat_lit 0) : copy α) = ⊥ := by dsimp -- fails

[Eric Wieser]

possibly lean4#2867?

[Johan Commelin]

Could well be! So I think we should tag this one as nolint simpNF and add a comment pointing to that issue.

[Johan Commelin]

Another PR fixes two of the dsimpNF problems flagged by the (temporarily reverted) linter fix.

chore(Topology/Spectral/Hom): fix problem with dsimp lemma, fix porting note #13818

After this one, I think we are ready to re-revert the linter fix in batteries.

[Johan Commelin]

@Kim Morrison @Mario Carneiro I think we are ready to refix the linter.

Reapply "chore(Tactic/Lint/Simp): make simpNF linter dsimp-aware (batteries#839)" (batteries#841) batteries#844

[Mario Carneiro]

I think this PR needs a mathlib companion PR to ensure the issue is not repeated

[Kim Morrison]

If you could just add a link to a Mathlib PR using this Batteries PR, we can check CI looks good.

[Johan Commelin]

testing new dsimpNF linter #13855

just passed CI

[Johan Commelin]

I have also added a link to this testing PR as requested.

[Kim Morrison]

I've merged batteries#841, and will merge #13855 as soon as it passes. Thanks!

[Johan Commelin]

chore: remove many nolint simpNF #13889

tries to remove a bunch of nolint simpNFs. Is there an easy way to automate this? So far, I've just removed all of them, and then manually restored a whole bunch of them...

[Yaël Dillies]

Sounds like a job for Damiano auto-correction Testa

[Michael Rothgang]

... though this one is one level harder, as the simpNF linter is global on all of mathlib (if I understood correctly...)

[Eric Wieser]

I think a sensible direction would be to make nolint simpNF an error if the lemma does not trigger the linter in the first place

[Eric Wieser]

Of course, this doesn't help for cases where we nolint some_linter to prevent the linter crashing

[Damiano Testa]

Funny that you mention this, but I've been just writing a prototype "unnecessary syntax" linter that flags syntax uses that do not cause errors when removed. I can try it with no_lint simpNF when I'm back at a computer, if you want.

[Damiano Testa]

#13970 is a preliminary version of the "unnecessary nolint simpNF"-linter. This is a linter that flags when a flag to not lint for simpNF is in fact not necessary. :upside_down:

[Damiano Testa]

I look forward to a linter that flags when this linter is unnecessary.

[Damiano Testa]

If anyone wants to take a look at the nolints flagged by the linter, feel free to do so! I would like to make the linter self-correcting, but this one is a little challenging, since nolint takes a space-separated list of linters and nolint itself is in a comma-separated list of attributes, so either I rely on the pretty-printed syntax, or removing by hand the right stuff is going to be tricky.

[Damiano Testa]

Oh, if you do look at the nolints flagged by the linter and find some mistakes, please let me know!

As a by-product of this experiment, the linter essentially implements a syntax-version of the environment simpNFlinter. Thus, if there is interest in making the syntax simpNF linter available, then getting it to align with the environment linter would be good! Of course, the syntax linter has the advantage that it gives live warnings. However, the environment linter also flags auto-generated declarations and post-hoc attributes, which is trickier with the syntax linter.

[Damiano Testa]

#13982 removes 86 unused nolint simpNFs.

[Damiano Testa]

As a consequence of the removal, I also have essentially implemented a syntax version of the simpNF linter. It does the "local" checking, so misses some global lints, but flags issues "live".

Is there interest in polishing it and PRing it?

[Damiano Testa]

For reference, the linter flagged the 86 nolints in the PR, together with 22 extra ones that the global linter flags, but the local one does not.

[Damiano Testa]

I also wonder whether these "polishing up code" linters should self-correct and should only be run every once in a while by CI.

[Damiano Testa]

Kim, you delegated the removal of nolint simpNF, but you also PRed some adaptations where you add some nolints back: can I check somehow that the nolints that I would be removing would not have to be added back with the bump?

[Damiano Testa]

Specifically, some of the ones in Mathlib/Data/NNRat/Defs.lean may fit the general pattern of the ones you had to re-nolint.

[Kim Morrison]

Can you just run your machinery on nightly-testing?

[Damiano Testa]

Oh, sure: I'll look for the nightly-testing branch.

[Damiano Testa]

Ok, I am not sure that I will have much more time soon, but this is an initial observation, that may be helpful in case you know what else has changed!

The Expr-tree of the lhs of docs#Pi.one_apply

theorem one_apply [∀ i, One <| f i] : (1 : ∀ i, f i) i = 1 :=

goes from being

-- on master
inspect: '1'

'OfNat.ofNat' -- app
|-'[anonymous]' -- app
|   |-'_uniq.421' -- fvar
|-'1' -- lit
|-'One.toOfNat1' -- app
|   |-'[anonymous]' -- app
|   |   |-'_uniq.421' -- fvar
|   |-'[anonymous]' -- app
|   |   |-'_uniq.421' -- fvar

to being

-- on nightly-testing
inspect: '1 i'

'OfNat.ofNat' -- app
|-('i') -- forallE
|   |-'_uniq.415' -- fvar
|   |-'[anonymous]' -- app
|   |   |-'0' -- bvar
|-'1' -- lit
|-'One.toOfNat1' -- app
|   |-('i') -- forallE
|   |   |-'_uniq.415' -- fvar
|   |   |-'[anonymous]' -- app
|   |   |   |-'0' -- bvar
|   |-'Pi.instOne' -- app
|   |   |-'_uniq.415' -- fvar
|   |   |-'_uniq.416' -- fvar
|   |   |-'_uniq.418' -- fvar
|-'_uniq.417' -- fvar

[Eric Wieser]

Surely that first one is a typo, and it shoudn't say inspect: '1'?

[Damiano Testa]

Actually, both should be correct: the LHS even pretty prints differently

[Eric Wieser]

So on master the LHS of (1 : ∀ i, f i) i = 1 is 1? Are you reducing somehow?

[Damiano Testa]

No, that is just what you see with the cursor right after :=

[Damiano Testa]

("no" was to reducing, yes, on master that is how the LHS looks like, just 1)

[Damiano Testa]

You are making me doubt, but I checked a few times. I'm on mobile now, though, but feel like I should be checking again! :smile:

[Damiano Testa]

I am now at a computer and I no longer see the lhs as 1, but instead as 1 i. I am not sure what was happening when I was looked at this earlier.