exprs of partials

Stream: lean4

[Arthur Paulino]

Hi all,

I'm calling Lean.Elab.IO.processCommands to get a Lean.Elab.Frontend.State so I can access commandState : Lean.Elab.Command.State to get the Lean.Environment.

Now, is there a way to get the original expressions for partial definitions before they're turned into trivial opaques with default values from their Inhabited instances?

[Arthur Paulino]

As a feature request, would it be too much to ask for the original partial implementation to be kept in the Lean.Environment with a distinct name?

[John Burnham]

One thing @Arthur Paulino and I just discovered which is interesting is that unsafe definitions do preserve their implementation values in the Lean.Environment you get after elaboration. So if you do something like

set_option pp.all true

unsafe def myPartialFnUnsafe (n : Nat) : Nat :=
  if n = 0 then 1 else myPartialFnUnsafe (n - 1) + n

partial def myPartialFn (n : Nat) : Nat :=
  if n = 0 then 1 else myPartialFn (n - 1) + n

#print myPartialFnUnsafe
#print myPartialFn

> info: ...: unsafe def myPartialFnUnsafe : Nat → Nat :=
fun (n : Nat) =>
  @ite.{1} Nat (@Eq.{1} Nat n (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
    (instDecidableEqNat n (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
    (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat)
      (myPartialFnUnsafe
        (@HSub.hSub.{0, 0, 0} Nat Nat Nat (@instHSub.{0} Nat instSubNat) n (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))))
      n)
info: ...: opaque myPartialFn : Nat → Nat

As far as we can tell, there isn't any auxiliary definition or other location in the environment that preserves the original body of the partial. This makes sene for typechecking, since there you only care about whether the type of the partial is inhabited, but for use cases that want to use an Environment for other tooling (in our case, hashing Lean constants so we can make zero-knowledge proofs from them) it would be nice to have partials create an auxiliary unsafe. I imagine this would be analogous to what you can do manually with the following boilerplate:

unsafe def myPartialFn._unsafe (n : Nat) : Nat :=
  if n = 0 then 1 else myPartialFnUnsafe (n - 1) + n
@[implemented_by myPartialFn._unsafe]
partial def myPartialFn (n : Nat) : Nat :=
  if n = 0 then 1 else myPartialFn (n - 1) + n

#eval do return Lean.Compiler.getImplementedBy? (<- get_env!) `myPartialFn
-- @Option.some.{0} Lean.Name (Lean.Name.mkStr2 "myPartialFn" "_unsafe")

(where get_env! is a metaprogram we have in our project that runs the elaborator on the current file to produce an environment.)

Would love to get feedback on whether this makes sense, or if there's somewhere this info is already preserved

[Henrik Böving]

import Lean

partial def f (x : Nat) : Nat := f x

open Lean Meta

#eval show MetaM _ from do
  let env ← getEnv
  return env.find? (Lean.Compiler.mkUnsafeRecName ``f) |>.map (·.value!)

[John Burnham]

Tysm! :pray: