Getting the pre-equation compiler Expression

Stream: lean4

[Lev Stambler]

Hello, I am trying to write an attribute macro which uses getConstInfo to get a def function. I want to get the function without any compilation via BrecOn. Is this possible?

For example, I have

def counting : Nat → Bool := fun n => match n with
  | 0 => false
  | n + 1 => counting n

getConstInfo though gives the Expression for

def counting : Nat → Bool :=
fun n =>
  Nat.brecOn n fun n f =>
    (match (motive := (n : Nat) → Nat.below n → Bool) n with
      | 0 => fun x => false
      | succ n => fun x => x.fst.fst)
      f

[Mario Carneiro]

No, this expression is not stored so unless you intercept it during creation it isn't available. There are basically four options:

1. Use the definition (brecOn ugliness)
2. Use the equations (you can ask for these to be generated)
3. Use the _sunfold smart unfolding theorem (from which 2 is generated IIRC)
4. Use the compiled code or IR (not an Expr, but reflects the original recursive structure better)

[Max Nowak 🐉]

Lean also doesn’t have native match

[Lev Stambler]

Mario Carneiro said:

No, this expression is not stored so unless you intercept it during creation it isn't available. There are basically four options:

1. Use the definition (brecOn ugliness)
2. Use the equations (you can ask for these to be generated)
3. Use the _sunfold smart unfolding theorem (from which 2 is generated IIRC)
4. Use the compiled code or IR (not an Expr, but reflects the original recursive structure better)

Thank you for the response! What do you mean by getting the equations and how could I do so?

[James Gallicchio]

this might be relevant? https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Equational.20Lemmas
which references this api: https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Eqns.html#Lean.Meta.getEqnsFor?

[Lev Stambler]

James Gallicchio said:

this might be relevant? https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Equational.20Lemmas
which references this api: https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Eqns.html#Lean.Meta.getEqnsFor?

This is fantastic thank you

[Lev Stambler]

Okay. getEqnsFor looks almost like what I would want but would love to just get the expressions in the match (not the associated theorems for termination) .

[James Gallicchio]

do you have an example? I'm not really familiar with what the function returns right now...

[Lev Stambler]

James Gallicchio said:

do you have an example? I'm not really familiar with what the function returns right now...

So, overall, I would like some simple way to modify my written function to add small statements after every sub-expression in a recursive function (i.e. counting runtime). I think it'd be doable if for a recursive function, I can get an expression associated with a case.

So, for

def counting3 : Nat → Bool
  | 0 => false
  | n + 1 => counting3 n

I'd get some expression representing 0 => false and n + 1 => counting3 n. Right now, getEqnsFor returns

private theorem counting3._eq_1 : counting3 0 = false :=
Eq.refl (counting3 0)

and

private theorem counting3._eq_2 : ∀ (n_1 : Nat), counting3 (succ n_1) = counting3 n_1 :=
fun n_1 => Eq.refl (counting3 (succ n_1))

which basically encapsulated the functionallity.

I may also start looking into the compiled code/ IR but have no clue where to start there (I do not have much experience with IR or compilers). @Mario Carneiro do you know of any reading material which I could check out for this? I found this export_format readme, but am unsure if this is what you were referring to.

[Mario Carneiro]

Why not do it before the definition is compiled? Then you can do whatever you want

[Mario Carneiro]

i.e. an attribute on the definition, or using a new keyword instead of def

[Mario Carneiro]

When processing a declaration you are given very explicitly all the cases and can do lowering as you see fit

[Lev Stambler]

Mario Carneiro said:

Why not do it before the definition is compiled? Then you can do whatever you want

How could I go about doing this? My end goal is to make it an attribute on the definition but am finding it very challenging to debug when writing directly within the attribute and am thus prototyping outside of the attribute macro.

Alternatively, how would I use a new keyword instead of def?