Elaboration Strategies

Stream: lean4

[François G. Dorais]

Closed issue #201 suggests that special elaboration strategies like Lean 3's elab_as_eliminator are no longer useful in Lean 4. What has changed?

[François G. Dorais]

I've been working on porting some low-level Lean 3 code which makes strong use of term mode and custom recursors. Here is a trick to work around the absence of elab_as_eliminator in case someone else is struggling with similar issues.

It looks like *.recOn and friends are always elaborated just like any other terms but in Lean 4 we can specify individual optional arguments by name. The motive in *.recOn and friends seems to always be called motive (rather than a nondescript name like C in Lean 3), so *.recOn (motive := fun _ => _) ... often works to simulate what elab_as_eliminator would do. Sometimes fun _ => _ is not enough and a bit more of the motive needs to be specified but it's generally a good starting point.

In tactic mode, it appears that the induction and cases tactics have gained some additional powers that may make elaboration strategies obsolete but I haven't explored this yet.