two errors

Stream: mathlib4

[Heather Macbeth]

I ported Logic.Function.Iterate, modulo two errors. I will make MWEs of the errors if needed, but thought I would toss the output here wholesale in case they are particular gotchas that someone will immediately recognize. One is:

fail to show termination for
  Function.RightInverse.iterate
with errors
structural recursion cannot be used

well-founded recursion cannot be used, 'Function.RightInverse.iterate' does not take any (non-fixed) arguments

and the other is

code generator does not support recursor 'Nat.rec' yet, consider using 'match ... with' and/or structural recursion

[Gabriel Ebner]

The second one should be self-explanatory, just avoid *.rec.

[Gabriel Ebner]

(This might be solved at some point in the future, but don't hold your breath.)

[Gabriel Ebner]

The RightInverse.iterate is a change in how name resolution works in recursive calls:

def RightInverse.iterate (h : RightInverse) : Nat :=
  h.iterate -- refers to `RightInverse.iterate`

while in Lean3 this referred to left_inverse.iterate

[Heather Macbeth]

In response to an error

code generator does not support recursor 'Nat.rec' yet, consider using
'match ... with' and/or structural recursion

Gabriel suggested
Gabriel Ebner said:

just avoid *.rec.

I think I can avoid using *.rec in the proof, but the name of the lemma itself is Iterate.rec. (See the mathport version). So should the lemma itself be deleted?

[Mario Carneiro]

Another option if the compiler gives you trouble is to mark the lemma as noncomputable

[Mario Carneiro]

The fact that the lemma is named *.rec doesn't matter that much. The issue is only that built-in recursors are not code-genned properly

[Heather Macbeth]

Mario Carneiro said:

Another option if the compiler gives you trouble is to mark the lemma as noncomputable

Thanks, this works!

[Mario Carneiro]

If you can make it computable, by writing it as a recursive function instead, that is preferable since it will keep downstream things computable

[Heather Macbeth]

I don't know how to do that (my intuition for computability is poor), but anyone should feel free to push to the branch: it's mathlib4#585 and the declaration is Iterate.rec.

[Yuyang Zhao]

How about implementing .rec manually for some important types before built-in recursors are supported?

[Yuyang Zhao]

Also to_additive does not seem to support match ... with. It complains code generator does not support recursor '*.brecOn' ....

[Yuyang Zhao]

Yuyang Zhao said:

How about implementing .rec manually for some important types before built-in recursors are supported?

Like this

namespace List

def rec' {C : List α → Sort _} (nil : C [])
    (cons : (head : α) → (tail : List α) → C tail → C (head :: tail)) (l : List α) : C l :=
  match l with
  | [] => nil
  | hd::tl => cons hd tl (rec' nil cons tl)

end List

[Eric Wieser]

Gabriel Ebner said:

(This might be solved at some point in the future, but don't hold your breath.)

Would it be easier to implement this in core than it is to change every use of rec to a match in the port?

[Floris van Doorn]

Yuyang Zhao said:

Also to_additive does not seem to support match ... with. It complains code generator does not support recursor '*.brecOn' ....

Oh, that is a bug, and I'm not sure how easy it is to fix. As a workaround, explicitly write down the addivite definition as well (and then additivize the multiplicative one) (and include a porting note, mentioning the tracking issue I created: mathlib4#1428).

[Rémi Bottinelli]

I'm having trouble understanding the code generator does not support recursor … problem:

• The way I thought I understood things, is that the recursor is what any inductive construction compiles down to, eventually: pattern matching uses brec or well-founded recursion, which in turn is defined in terms of a recursor, which is just the induction principle of the type.
• I also thought I understood that if you want to compile some code to something that you can run, it makes sense (for performance and probably simplicity of the generated assembler/bytecode) to instead drop the recursor and have "unchecked" recursive calls, which you know will behave well because the type is right.

So, since lean4 is also meant to be used as a programming language and be efficient at it, I would guess the compiler checks that the code is correct by way of my first bullet, and makes it compute by way of the second, but "it should be trivial" to also translate calls of rec to dumb "unchecked" recursive calls, no?

[Jannis Limperg]

Conceptually it's trivial, yes. The devs have indicated that they won't do it in the near future because they don't need it, but they would take a PR (though there seems to be a PR freeze atm, so this is probably not a good time).

[Eric Wieser]

Note that you can manually implement compiler support for the missing recursors; we do this for docs4#List.recC and docs4#Nat.recC

[Rémi Bottinelli]

is csimp some kind of a compiler hint?

[Rémi Bottinelli]

Actually, I'm still a bit confused:

• How does the lean kernel/elaborator ensure that a definition by pattern matching is well-defined? Is the kernel still .rec all the way down?
• As far as I understand, defining stuff without explicitly using .rec can sometimes lead to bad defeqs. How does it work around this?
  Ah, I guess having nice defeqs is solely a typechecking problem, which you don't care when compiling?

[Eric Wieser]

Do you have a specific rec in mind?

[Eric Wieser]

Yes, csimp says "use this lemma to exchange a computation-unfriendly function with nice defeqs with this efficient / computable one"

[Rémi Bottinelli]

Eric Wieser said:

Do you have a specific rec in mind?

Relative to my "claim" that not using rec can lead to bad defeqs? Well, I experienced a few such instances.

[Eric Wieser]

No, I mean a case where the Lean3 code used rec, and during porting you were coerced into using something else?

[Eric Wieser]

Jannis Limperg said:

Conceptually it's trivial, yes. The devs have indicated that they won't do it in the near future because they don't need it, but they would take a PR (though there seems to be a PR freeze atm, so this is probably not a good time).

Note that lean4#2049 tracks the missing compiler support for rec

[Rémi Bottinelli]

ah, yes, that's a problem I had with PathCategory (see thread).

[Rémi Bottinelli]

I just added noncomputable

[Eric Wieser]

You could instead define Quiver.Path.recC