Defining my own code extraction from proofs

Stream: general

[Paweł Balawender]

Hey!

I'm looking for a way to define my own code extraction method from proofs in Lean. I would like to traverse the proof term manually, extract the nodes that interest me and output a C++ function that "corresponds" to the proof. I wasn't able to find relevant functionality in the section about Metaprogramming in the Lean Reference. I also wasn't able to find anything relevant (such as code extraction) in the source code of Lean. I also worry that Proof irrelevance might be a trouble (but not when operating on the meta-level perhaps?). Could you point me to how one would normally approach such a thing? I.e. getting your hands on the actual proof created by the user, and extracting computational content out of it?

The background: I'm currently formalizing the field of bounded arithmetic, and what's interesting about this field is that if you manage to prove a theorem (e.g. addition is associative, or for every x sqrt(x) exists) only from a specific set of axioms (like x >= x) + induction, then it is true that for every such proof corresponds to a Turing machine operating in some well-known complexity. I have a working formalization of proofs in arithmetic and now need to extract computations from them

[Paweł Balawender]

Is there an equivalent of lean virtual machine in lean4?

[Aaron Liu]

Paweł Balawender said:

Could you point me to how one would normally approach such a thing? I.e. getting your hands on the actual proof created by the user, and extracting computational content out of it?

You can get the proof term from the constant name like this (using Nat.pow_add as an example):

import Lean

run_meta do
  let name := ``Nat.pow_add
  let ci ← Lean.getConstInfo name
  let some val := ci.value? |
    throwError m!"{Lean.MessageData.ofConstName name} has no value"
  Lean.logInfo val

[Paweł Balawender]

Thank you! Following your hint, I was able to define a basic proof-term Expr traversal. What I'm trying to do is to, whenever I find an instance of Exists.intro, applied to some x and a proof x : P x, find the definition of x and recursively process it (to, ultimately, get to some exists that is an axiom in my view and to which i know how to extract code from). However, I am struggling dealing with eliminators such as Exists.rec, which in a rather opaque way bind one of their arguments as, say, a variable in the other (in the continuation of the proof).

Let's say we have a situation like:

• we know that in the currently processed node of Expr we have an occurrence of variable Y and we want to find its definition
• we know that Y is just a bound variable of a lambda, and that the lambda is an argument of an Exists.rec higher up in the proof tree
• we know the argument of Exists.rec that should bind to the Y

Since the definition of Exists.rec is opaque, I currently think I'd have to reinvent Exists.rec to manually bind the parameter. I tried to somehow unfold the .rec to a standard Expr.lam node and use Lean.Meta.withLocalDecl, as I do when encountering Expr.lam nodes:

partial def findExIntro (e : Lean.Expr) : Lean.MetaM Lean.Expr :=
  match e with
  | lam name type body binderInfo =>
    Lean.Meta.withLocalDecl name binderInfo type fun x => do
      let newBody <- findExIntro (body.instantiate1 x)
      Lean.Meta.mkLambdaFVars #[x] newBody

but I wasn't able to unfold this definition. Do you have any concept how we should properly do it in Lean?

[Aaron Liu]

what did you try?

[Paweł Balawender]

Okay, just after writing this I found one way to do it - from an expression of Exists.rec, filter out the argument arg[4] (creating the ex) and the continuation (intro: \x, hx -> rest of proof), then recurse down arg[4] (which reduces to a pair of x, hx) to extract the definition of x. This looks like:

| e@(app _ _) => do
    -- TODO: ideally, this case shouldn't be here, really...
    -- we should have something more general
    if isAppOfArity e ``Exists.rec 5 then
      let args := getAppArgsN e 5
      let witness_pair := args[4]!
      let witness <- findExIntro witness_pair
      let raw_intro := args[3]!
      let inst <- Lean.Meta.instantiateLambda raw_intro #[witness]
      return <- findExIntro inst

which is not fully general, but rather works for now. Perhaps there is more standard way of achieving this? Or more general, to also deal with other eliminators than Exists.rec?

[Aaron Liu]

Maybe you can use some sort of rewriting system instead

[Aaron Liu]

that would be more standard

[Eric Wieser]

If you are trying to extract a program, it is better to start with a program; so replace Exists with Subtype, Or with Sum, etc