what is `elab_as_elim`

Stream: general

[Asei Inoue]

what is [elab_as_elim] attribute? what does this attribute? what is the difference when I add this attribute to something...?

[Kevin Buzzard]

It changes the way the declaration is elaborated. I don't know the technical details but presumably the idea is that with the tag, Lean is more prepared to have a good guess at the type of the motive which the user means, even though this typically means solving a higher-order unification problem.

[Asei Inoue]

is there an example ?

[Kevin Buzzard]

Sure, search mathlib for the attribute, then remove it from something and see what breaks.

[Aaron Liu]

@[elab_as_elim] registers the declaration as an eliminator. Eliminators have special support for filling in the motives automatically with syntactic replacement instead of using second-order unification. By default, .rec, .recOn, .casesOn, .brecOn are all eliminators.

[Kevin Buzzard]

Things we want to use as recursors (i.e. stuff we want to use to do induction) is what is being tagged.

[Asei Inoue]

Thank you!

[Kyle Miller]

In general, @[elab_as_elim] is for declarations whose return type is of the form p x1 x2 ... xn, and during elaboration you want p to be solved for using the expected type. The expressions x1 through xn can be arbitrary expressions. To solve for p, xn through x1 are replaced by variables in that order; the result is the body for p. (This process can fail, and you may get a "motive not type correct" error. That's when the expression for p is ill-typed.) The elaborator will throw an error if there is no expected type.

There are a couple of other different rules for how these are elaborated. It eagerly elaborates all arguments that appear in x1 through xn. These are like "major premises", using eliminator terminology. The remaining arguments are "minor premises", and and elaboration for those is deferred until after p is computed.

@[elab_as_elim] at this point is only loosely related to eliminators, but every eliminator uses this elaboration procedure.

This attribute shouldn't be confused with @[induction_eliminator] or @[cases_eliminator], which are for configuring which induction or cases principle should be used for the induction and cases tactics.

[Asei Inoue]

I've been searching for a code example that shows what changes before and after adding the elab_as_elim attribute, and today I finally found one.

universe u

/-- A pseudo-recursion function modeled after the standard recursor `Nat.rec` -/
def Nat.rec' {motive : Nat → Sort u}
    (zero : motive 0) (succ : ∀ n, motive n → motive (n + 1))
    (t : Nat) : motive t := Nat.rec zero succ t

set_option pp.mvars false in

-- If no attribute is given, we get an error message like this
/--
error: Function expected at
  Nat.rec' ?_ (fun x b => b + 1) ?_
but this term has type
  ?_ ?_

Note: Expected a function because this term is being applied to the argument
  a
-/
#guard_msgs in
def add (a b : Nat) := Nat.rec' _ (zero := b) (succ := fun _ b => b + 1) a

-- Add an attribute
attribute [elab_as_elim] Nat.rec'

-- The error message changes to “failed to elaborate eliminator.”
-- It is now recognized as an eliminator!
/-- error: failed to elaborate eliminator, expected type is not available -/
#guard_msgs in
def add (a b : Nat) := Nat.rec' _ (zero := b) (succ := fun _ b => b + 1) a

[Asei Inoue]

The documentation comment for [elab_as_elim] includes an intriguing code example, but unfortunately, the details are omitted and it can't be run as-is. If anyone is able to fill in the missing pieces of that example, I'd love to hear from them.

[Kyle Miller]

You can also take tests/lean/run/elabAsElim.lean in Lean 4 and try deleting @[elab_as_elim] and see failures.

[Kyle Miller]

With the example in the docstring for elab_as_elim, you can replace ... with sorry.

(@Joseph Rotella In the "complex substitution" example, I wonder if it's worth explaining that if @[elab_as_elim] weren't there then even though it looks like it works, you get a bad motive. I wonder if the docstring should include the details from my comment above on 3/14 about how the arguments to the motive can b earbitrary expressions? By the way, there's a typo with evenOddRec vs evenOddRecOn.)

[Joseph Rotella]

@Kyle Miller I've tried to (relatively concisely) incorporate these changes in lean4#9359—feel free to adjust. (Relatedly, at some point, it's probably worth turning the "motive not type correct" explainer text into a proper error explanation, but I figured that'd best be left to a separate PR.)

[Kyle Miller]

Thanks Joseph (and thanks for adding the docstring in the first place!)

[Joseph Rotella]

No worries—though I believe it was Robin Arnez who added the docstring!

[Kyle Miller]

Oh, oops, sorry for pinging you :-)