adding definitions

Stream: lean4

[Patrick Massot]

What is the simplest way in CommandElabM to create a new definition using a object that we already have? For instance assume my tactic state is

arr : Array Nat
⊢ CommandElabM PUnit

What is the simplest way to add to the current environment a definition with name foo, type Array Nat and value arr? I know I can write

  let typ : Expr := mkApp (mkConst ``Array) (mkConst ``Nat)
  let val : Expr := sorry
  let decl : Declaration := Declaration.defnDecl {name := `foo, levelParams := [], type := typ, value := val, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe}
  addAndCompile decl

but it seems very complicated and I don't really know how to construct the val expression. I could also try to create some Syntax and use elabCommand but it seems even more tortuous.

[Arthur Paulino]

I could be wrong, but I think you need to build the value expression

[Arthur Paulino]

(I'm not sure if you don't want a solution that involves building the value expression of if you just don't know how to)

[Arthur Paulino]

To build the value expression, you can use mkNatLit to build a List Expr from arr, mkListLit to build an expression that represents the List Nat and mkApp to build the expression that represents the Array Nat

[Patrick Massot]

Thanks Arthur. I was really hoping for a much simpler way. Basically I'd like a (monadic) function creating an Expr from a local declaration in my "programming state" (I don't really know how to call what the info view is showing while I'm programming in do notation).

[Patrick Massot]

But maybe those difficulties show that I'm following a completely wrong path.

[Gabriel Ebner]

elabCommand (← `(def foo : Array Nat := $(quote arr)))

Note that this will add a definition with the (inaccessible) declaration name (← `(foo)).getId.

[Gabriel Ebner]

If you want to go with addAndCompile directly, you can do:

addAndCompile <| .defnDecl {
  name := `foo
  levelParams := []
  type := toTypeExpr (Array Nat)
  value := toExpr arr
  hints := .regular (getMaxHeight (← getEnv) (toExpr arr) + 1)
  safety := .safe
}

[Patrick Massot]

Thanks Gabriel!

[Patrick Massot]

Gabriel Ebner said:

Note that this will add a definition with the (inaccessible) declaration name (← `(foo)).getId.

Unless I disable hygiene, right?

[Gabriel Ebner]

I would never suggest to disable hygiene. If you want a non-hygienic name for the definition I'd do:

elabCommand (← def $(mkIdent `foo):ident : Array Nat := $(quote arr))

[Patrick Massot]

Sorry about the heretic suggestion and thanks for telling me how to redeem myself.

[Arthur Paulino]

Oh, toExpr and toTypeExpr for the rescue! I didn't know those

[James Gallicchio]

Definitely would be worth including somewhere in the metaprogramming book, I had the exact question as Patrick earlier this week and resorted to manually reconstructing the syntax

[Arthur Paulino]

Good call. Added as an issue

[Patrick Massot]

I'm back to Lean and none of Gabriel's solutions works in my real use case :sad: There is no miracle, quote, toExpr and toTypeExpr all require instances.

[Gabriel Ebner]

Then you should post your real use case. :smile:

[Patrick Massot]

And no luck with hoping for deriving miracles.

[Patrick Massot]

In the real case Nat is replaced with a home-made structure.

[Patrick Massot]

However the fields of that structure are either Name or String so I guess defining the missing instances shouldn't be too hard

[Patrick Massot]

I managed to create the Quote instance!

[Patrick Massot]

I don't know how the deriving magic works but it looks like what I did is easy to automate to get a Quote instance for a structure where all fields have Quote instances.

[Patrick Massot]

I have a dual question. Inside a TermElabM computation I want to get access to an object that have been declared previously. Am I meant to use docs4#Lean.Environment.find? and then docs4#ConstantInfo.value! and then docs4#Lean.Meta.evalExpr or is there a more direct route?

[Patrick Massot]

The Zulip linkfier doesn't like declaration names ending in punctuation marks :sad:

[Mario Carneiro]

If you just want the expr then ((<- getEnv).find? name).get!.value! will do the trick

[Patrick Massot]

I know, but I want the object, that's why I'm asking whether I should use evalExpr. It sounds a bit expensive to to this while Lean already did that work at declaration time.

[Mario Carneiro]

evalConst is a bit easier than evalExpr for this case

[Mario Carneiro]

(<- getEnv).evalConst A (<- getOptions) name

[Sebastian Ullrich]

A definition, even with zero parameters, is not immediately evaluated to an object at declaration time

[Patrick Massot]

Does it mean it's evaluated every time we use it?

[Sebastian Ullrich]

In compiled code, it is evaluated once. In interpreted code, it is currently evaluated once per interpreter invocation (i.e. if your interpreted tactic calls evalConst multiple times on the same declaration, it should only be evaluated once I think).

[Patrick Massot]

It feels a but weird that I need to add unsafe everywhere because I want to access declared objects (both evalExpr and evalConst are unsafe).

[Mario Carneiro]

The operation is fundamentally unsafe, since nothing prevents you from passing the wrong type to evalExpr

[Mario Carneiro]

You can use Mathlib.Util.TermUnsafe to make it a bit more ergonomic to call unsafe functions

[Reid Barton]

Now known as Std.Util.TermUnsafe.