csimp on recursors

Stream: lean4

[Eric Wieser]

What is the error message telling me here?

/-- A computable version of `List.rec` -/
def List.recC {α : Type _} {motive : List α → Sort _} (nil : motive [])
  (cons : (head : α) → (tail : List α) → motive tail → motive (head :: tail)) :
    (l : List α) → motive l
| [] => nil
| (x :: xs) => cons x xs (List.recC nil cons xs)

@[csimp]
lemma List.recC_eq_rec : @List.recC = @List.rec := by
  ext α motive nil cons l
  induction l with
  | nil => rfl
  | cons x xs ih => rw [List.recC, ih]

invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.

Is @List.recC = @List.rec not of the form @f = @g?

[Henrik Böving]

I would suspect that while it is of the correct form what you are trying to do doesn't make sense for the compiler due to computable vs noncomputable stuff. I guess that it throws an error that just somehow ends up manifesting like this.

[Eric Wieser]

I thought the whole point of csimp was to turn noncomputable stuff (List.rec) into computable stuff (List.recC)

[Sebastian Ullrich]

The only other condition I can see in the code is that the level names of f and g must be exactly equal

[Henrik Böving]

The point of csimp is originally to have an inefficient nice for formalization version of a function and a pefornant version + a proof of equivalence for the compiler. I dont know about interactions with computability

[Eric Wieser]

Sebastian Ullrich said:

The only other condition I can see in the code is that the level names of f and g must be exactly equal

That fixes it, thanks!

[Eric Wieser]

Relatedly; is that csimp stated in the right direction?

[Eric Wieser]

Does the compiler version go on the LHS or RHS?

[Eric Wieser]

Answered my own question, thanks all:

def List.recC.{u_1, u} {α : Type u} {motive : List α → Sort u_1} (nil : motive [])
  (cons : (head : α) → (tail : List α) → motive tail → motive (head :: tail)) :
    (l : List α) → motive l
| [] => nil
| (x :: xs) => cons x xs (List.recC nil cons xs)

@[csimp]
lemma List.recC_eq_rec : @List.rec = @List.recC := by
  ext α motive nil cons l
  induction l with
  | nil => rfl
  | cons x xs ih =>
    rw [List.recC, ←ih]

-- works!
#eval (List.rec 0 (fun x xs ih => 0) ([] : List Nat) : Nat)

[Eric Wieser]

I guess the follow-up question is whether mathlib should add a recC for all of its inductive types (c.f. mathlib4#1720), or if having compiler support for .rec is on a near enough horizon that we don't need to

[Henrik Böving]

Leo said it is not of interest in the near future unless someone steps up and does it.

[Eric Wieser]

It looks like mathlib gets a long way by supporting just Nat.rec and List.rec via csimp, so probably it's not that big a deal

[Kevin Buzzard]

Is it meaningful to ask how much of mathlib is "noncomputable"? Much of the parts I deal with are a long way from being computable (and this is not a problem) but I no longer have a real oveview of the full library.

[Eric Wieser]

You could count def vs computable def to get a good estimate; or get the exact answer by looking at doc-gen's data dump

[Reid Barton]

computable is not relevant for 99% of mathlib anyways; only the parts used from tactics.

[Eric Wieser]

Lists + naturals are precisely the types that are likely to appear in tactics though, hence why I think those are worth having compiler support for

[Mario Carneiro]

BTW, I took a look at the code for this and I don't think it would be that hard to add support for compiling .rec functions like everything else, so I'm not that interested in investing in too many workarounds to preserve computability when the whole thing can be fixed in one go. It's just not a priority right now

[Parth Shastri]

I have actually already written code to autogenerate implementations for recursors. The code is a bit messy, but I would be happy to add it to mathlib