to_additive for generated lemmas

Stream: mathlib4

[Lukas Miaskiwskyi]

In porting Data.Finset.Pointwise (!4#1911), an innocuous to_additiveattribute on the following theorem is throwing an error:

theorem coe_npow (s : Finset α) (n : ℕ) : ↑(s ^ n) = (s: Set α) ^ n  := by
  change ↑(npowRec n s) = (s: Set α) ^ n
  induction' n with n ih
  · rw [npowRec, pow_zero, coe_one]
  · rw [npowRec, pow_succ, coe_mul, ih]

The error is

application type mismatch
  @npowRec._eq_1 (Finset α) Finset.zero
argument has type
  Zero (Finset α)
but function has type
  ∀ [inst : One (Finset α)] [inst_1 : Mul (Finset α)] (x : Finset α), npowRec 0 x = 1

set_option trace.to_additive true indeed reveals that to_additive generates a translation of the theorem that contains npowRec._eq_1, despite npowRec itself being marked with the to_additive attribute. I imagine ideally we'd like to_additive to also be inherited by the generated lemmas, right? Is this a bug? Could try to work out an #mwe if necessary.

[Floris van Doorn]

I'll investigate.

[Floris van Doorn]

This went deeper than I thought.
This has to do with the fact that Lean doesn't generate equation lemmas for definitions eagerly anymore. Instead, it generates them when used (at most once per file, I think). However, I just realized that even if we do generate the equation lemmas eagerly, Lean doesn't use them, and just generates a new one anyway.

[Floris van Doorn]

Example:

-- Test1.lean
import Lean

def foo := 1
open Lean Elab Meta Command

#eval liftCoreM <| MetaM.run' <| do
  let nm := `foo
  let d ← getEqnsFor? nm true
  logInfo m!"{d}" -- some ([_private.Mathlib.Test1.0.foo._eq_1])

-- Test2.lean
import Mathlib.Test1

open Lean Elab Meta Command

#eval liftCoreM <| MetaM.run' <| do
  let nm := `foo
  let d ← getEqnsFor? nm true
  logInfo m!"{d}" -- some ([_private.Mathlib.Test2.0.foo._eq_1])

[Floris van Doorn]

And rw uses getEqnsFor? to generate the equation lemmas. I'm confused that simp doesn't have the same behavior: I thought that simp uses the original equation lemma. Let me figure out if that is true. If so, maybe rw can use the same behavior as simp...

[Floris van Doorn]

Or maybe it's possible to add all eagerly generated equation lemmas (i.e. in the same file as the original declaration) to the environment extension eqnsExt, so that they can be found again (that should also save of generating a bunch of equation lemmas many times).

[Floris van Doorn]

@Lukas Miaskiwskyi this is going to be a nontrivial to_additive fix, or a core change. If you want to work-around this in the meantime: don't use rw on a definition. Instead, use something like simp [npowRec] or rw [npowRec_zero] (if that exists)

[Lukas Miaskiwskyi]

Very interesting as far as I understand it, thank you for looking into it! That workaround sounds doable.

[Floris van Doorn]

Apparently the difference is that rw uses getEqnsFor? declName (nonRec := true) when rewriting with a definition, and simp uses getEqnsFor? with nonRec set to false. For non-recursive definitions this does nothing, and simp instead uses a separate list of declarations that should be unfolded, and unfolds them using unfoldDefinition?

[Floris van Doorn]

So I guess we need to_additive to generate the equation lemmas for the additive declarations on the fly (like rw does for the multiplicative declaration).

[Floris van Doorn]

@Mario Carneiro if you have time: do you know if there is a reason for this distinction in the behaviors of rw and simp?

[Jannis Limperg]

These lazily generated equation lemmas also cause issues for Aesop. I'm not sure how much sense this makes, but maybe equation lemmas could be added to the environment as 'lazy constants' with a specific name and type, but without a proof, and then the proof is computed once the constant is actually used?

[Jannis Limperg]

Of course this would require substantial core changes, so probably not a near-term solution.

[Jakob von Raumer]

Is the laziness just for better performance here?

[Mario Carneiro]

The laziness is to avoid generating lots of useless and unused theorems in a programming project like lean core

[Mario Carneiro]

I think the most sensible way to control equation generation is with a set_option, so that we can enable it in proofy parts and disable it in meta parts

[Floris van Doorn]

It would still require a change in getEqnsFor?, because currently it will keep generating equation lemmas for foo in every file, even if you generated an equation lemma for foo when you defined it.

[Floris van Doorn]

@Lukas Miaskiwskyi the original problem can be solved in a similar way as we solve the lemmas that simp generated, so I pushed a fix in !4#1948