implemented_by and wf recursion

Stream: lean4

[Jun Yoshida]

I got the following error:

def myfunUnsafe (x : Array α) (i : Fin x.size) : Array α :=
  sorry

/-
Error:
> invalid 'implemented_by' argument 'myfunUnsafe', 'myfunUnsafe' has type
>   {α : Type u_1} → (x : Array α) → Fin (Array.size x) → Array α
> but 'myfun._unary' has type
>   {α : Type u_1} → (x : Array α) ×' Fin (Array.size x) → Array α
-/
@[implemented_by myfunUnsafe]
def myfun (x : Array α) (i : Fin x.size) : Array α :=
  let next := 2*i.1 + 1
  if h : next < x.size then
      have : x.size - next < x.size - i.1 := sorry
      myfun (x.swap i ⟨next,h⟩) ⟨next, (x.size_swap _ _).symm ▸ h⟩
  else
    x
termination_by _ => x.size - i.1

The error message claims that the type of myfunUnsafe is not correct, but the next doesn't work, of course.

def myfunUnsafe' (x : (x : Array α) ×' Fin x.size) : Array α :=
  sorry

/-
Error:
> invalid 'implemented_by' argument 'myfunUnsafe'', 'myfunUnsafe'' has type
>   {α : Type u_1} → (x : Array α) ×' Fin (Array.size x) → Array α
> but 'myfun'' has type
>   {α : Type u_1} → (x : Array α) → Fin (Array.size x) → Array α
-/
@[implemented_by myfunUnsafe']
def myfun' (x : Array α) (i : Fin x.size) : Array α :=
  let next := 2*i.1 + 1
  if h : next < x.size then
      have : x.size - next < x.size - i.1 := sorry
      myfun' (x.swap i ⟨next,h⟩) ⟨next, (x.size_swap _ _).symm ▸ h⟩
  else
    x
termination_by _ => x.size - i.1

It seems to be a bug to me.
Are there any workaround?

[Mario Carneiro]

looks like a bug, the workaround is

def myfun' (x : Array α) (i : Fin x.size) : Array α :=
  let next := 2*i.1 + 1
  if h : next < x.size then
      have : x.size - next < x.size - i.1 := sorry
      myfun' (x.swap i ⟨next,h⟩) ⟨next, (x.size_swap _ _).symm ▸ h⟩
  else
    x
termination_by _ => x.size - i.1

@[implemented_by myfunUnsafe]
def myfun (x : Array α) (i : Fin x.size) : Array α := myfun' x i

[Jun Yoshida]

Thank you. Should I open an issue?

[Mario Carneiro]

my guess is that something is copying the implemented_by attribute to both the original function and the myfun._unary auxiliary function

[Jun Yoshida]

lean4#2899

[Jun Yoshida]

Mario Carneiro said:

my guess is that something is copying the implemented_by attribute to both the original function and the myfun._unary auxiliary function

I confirmed you are right. The myfun._unary, which is generated by Lean.Elab.WF.packDomain, inherits the attributes from the source declaration:

/- Defining an attribute that just stores names -/

import Lean.Meta

open Lean Meta

initialize myExtension :
    SimpleScopedEnvExtension Name (Array Name) ←
  registerSimpleScopedEnvExtension {
    addEntry := fun ns => ns.push
    initial := #[]
  }

@[inline] def getMyExtensionDecls {m : Type → Type} [Monad m] [MonadEnv m] : m (Array Name) := do
  return myExtension.getState (← getEnv)

syntax (name := myattr) "myattr" : attr

initialize registerBuiltinAttribute {
  name := `myattr
  descr := "Show all declarations that inherits an attribute 'myattr'."
  applicationTime := .afterTypeChecking
  add := fun declName _ _ => do
    MetaM.run' do myExtension.add declName
}

/-------------------/
/- In another file -/
/-------------------/

@[myattr]
def myfun (x : Array α) (i : Fin x.size) : Array α :=
  let next := 2*i.1+1
  if h : next < x.size then
    have : x.size - next < x.size - i.1 := sorry
    myfun (x.swap i ⟨next,h⟩) ⟨next,sorry⟩
  else
    x
termination_by _ => x.size - i.1

/-
`myattr` is attached not only to `myfun` but also to `myfun._unary`.
> #[`myfun._unary, `myfun]
-/
#eval getMyExtensionDecls (m:=Lean.CoreM)

[Jun Yoshida]

I am not sure if myfun._unary should have the same attributes as myfun. IMHO, it shouldn't have any special attribute, and the attribute inheritance should be done using another attribute for this purpose, if necessary.

[Joachim Breitner]

Most attributes that I can think of should only go on myfun: Everything that is external (doc related things, tactic registration etc.)
What attributes would have to be put on aux implementation definitions? Are there even any?

[Jun Yoshida]

Here is another terrible example with Mathlib:

import Mathlib.Tactic

/-
> (kernel) unknown constant 'myfunZero._unary.proof_1'
-/
@[to_additive]
def myfunOne (x : Array α) (i : Fin x.size) : Array α :=
  let next := 2*i.1 + 1
  if h : next < x.size then
      have : x.size - next < x.size - i.1 := sorry
      myfunOne (x.swap i ⟨next,h⟩) ⟨next, (x.size_swap _ _).symm ▸ h⟩
  else
    x
termination_by _ => x.size - i.1

[Jun Yoshida]

Joachim Breitner said:

Most attributes that I can think of should only go on myfun: Everything that is external (doc related things, tactic registration etc.)
What attributes would have to be put on aux implementation definitions? Are there even any?

How about specialize?

[Joachim Breitner]

For to_additive you’d want it on both, right?

[Jun Yoshida]

Ah, you are right. The "definition" to_additive sees is the generated one using myfunOne._unary, so it also needs myfunZero._unary. The problem in the above example is likely that to_additive doesn't take care of the termination proof. In this sense, it may be the bug of to_additive rather than of implemented_by.

[Floris van Doorn]

to_additive does no effort to additivize definitions with well-founded recursion correctly, so it doesn't surprise me that it doesn't work. The workaround it to write both versions (the additive version first) and then connect them using @[to_additive existing]. Note: in your MWE there is no multiplicative structure to additivize, right?

[Jun Yoshida]

@Floris van Doorn to_additive example is just an example and not a central problem here. And I still think it is a bug of to_additive; if it is not capable of dealing with well-founded recursion, it should produce an appropriate error, IMHO.

[Joachim Breitner]

Isn’t there a command-form of to_additive that you could apply to myFunOne._unary and then to myFunOne after both have been defined and it would just work? Or is there something fundamental about well-founded recursion that causes issues with to_additive?

[Jun Yoshida]

Joachim Breitner said:

Isn’t there a command-form of to_additive that you could apply to myFunOne._unary and then to myFunOne after both have been defined and it would just work? Or is there something fundamental about well-founded recursion that causes issues with to_additive?

Hmm, the idea actually works!

import Mathlib.Tactic

def myfunOne (x : Array α) (i : Fin x.size) : Array α :=
  let next := 2*i.1 + 1
  if h : next < x.size then
      have : x.size - next < x.size - i.1 := sorry
      myfunOne (x.swap i ⟨next,h⟩) ⟨next, (x.size_swap _ _).symm ▸ h⟩
  else
    x
termination_by _ => x.size - i.1

attribute [to_additive myfunZero._unary] myfunOne._unary
attribute [to_additive] myfunOne -- OK

[Jun Yoshida]

So, the problem on to_additive is maybe that it doesn't generate the name of the additive counterpart of myfunZero._unary correctly.

[Joachim Breitner]

It’s not complete, though. There are “unfold equations” attached to myFunOne that are not transferred:

import Mathlib.Tactic

def myfunOne (x : Array α) (i : Fin x.size) : Array α :=
  let next := 2*i.1 + 1
  if h : next < x.size then
      have : x.size - next < x.size - i.1 := sorry
      myfunOne (x.swap i ⟨next,h⟩) ⟨next, (x.size_swap _ _).symm ▸ h⟩
  else
    x
termination_by _ => x.size - i.1

attribute [to_additive myfunZero._unary] myfunOne._unary
attribute [to_additive] myfunOne -- OK

theorem ex1 : myfunOne #[true] (Fin.last 0) = #[true] := by
  unfold myfunOne
  -- no mention of myfunOne._unary
  rfl

theorem ex2 : myfunZero #[true] (Fin.last 0) = #[true] := by
  unfold myfunZero
  -- mentions of myfunZero._unary
  -- rfl still works, but more by accident
  rfl

I don’t know that corner of the system well; presumably to_additive could find them and translate them as well.

[Joachim Breitner]

These are generated lazily, it seems. So maybe to_additive needs to register a getter for such lemmas on the additive variant, and when called, call it on the original version, take the lemmas, transfer them, and return them. But at this point it may be simpler to just copy the recursive definition :-)

[Jun Yoshida]

The solution definitely depends on whether to_additive is attached to myfunOne._unary or not.

Generally, it really depends on an attribute if myfun._unary should inherit it from myfun:

• specialize nospecialize are examples which should be inherited; some functions in the core (e.g. Array.zipWithAux) assume this behavior.
• implemented_by is one that shouldn't be.

So, what would be the "fix" of the bug?