Split theorem conclusion

Stream: metaprogramming / tactics

[Simon Sorg]

The following is potentially ill-defined. Please accept my apologies, as I'm lacking the knowledge to express myself more clearly. I just hope that Syntax is the right abstraction.

I frequently think of a theorem syntactically as a bunch of hypotheses and a single conclusion, where the conclusion is separated from the rest via :. Now, I'm searching for a nice way to split the conclusion from the hypotheses, i.e. get the Syntax object of said conclusion. More generally, I'd like to get this for each theorem in a file. I present my "solution" below. I would appreciate being told whether, and if so where, it is flawed, as I'm quite a novice in metaprogramming.

Using the InfoTree, I can check the syntax kinds to get information on the parser, and thereby figure out whether a certain CommandInfo is a theorem or something else.
Once that's obtained, I'm now obtaining all direct child nodes of such a CommandInfo node for a theorem, and simply get the syntax for the one with the largest starting line / column. This seems to work for me for now. Is there a known better way that I'm missing?

I'm unsure how to press this into an #mwe, so here's my current implementation. Note that this won't work on it's own. To run it, this PR could be used. Any input is greatly appreciated - thanks for taking the time!

partial def maxTermNode (terms: List (TermInfo × Option ContextInfo)) : Option (TermInfo × ContextInfo) :=
  match terms.head? with
  | some ⟨ti, ctx?⟩ =>
    let largestTail := maxTermNode terms.tail
    match largestTail with
    | some ⟨tailinfo, tailctx⟩ =>
      match ctx? with
      | some ctx =>
        let range := stxRange ctx.fileMap ti.stx
        let tailRange := stxRange tailctx.fileMap tailinfo.stx
        if tailRange.snd.line > range.snd.line then some ⟨tailinfo, tailctx⟩
        else
          if tailRange.snd.column > range.snd.column then some ⟨tailinfo, tailctx⟩
          else some ⟨ti, ctx⟩
      | none => some ⟨tailinfo, tailctx⟩
    | none => match ctx? with
      | some ctx => some ⟨ti, ctx⟩
      | none => none
  | none => none

def conclusion (t : InfoTree) : IO (List (TermInfo × ContextInfo)) := do
  let only_declarations := fun i => match i with
    | .ofCommandInfo m => if m.elaborator == ``Lean.Elab.Command.elabDeclaration then
      match m.stx.getArgs.toList.getLast? with
      | some stx => stx.getKind == ``Lean.Parser.Command.theorem
      | none => false
      else false
    | _ => false
  let only_term := fun i => match i with
    | .ofTermInfo _ => true
    | _ => false

  let trees := t.filter (fun i => only_declarations i) (stop := only_declarations)
  let terms_info : List (List (Info × Option ContextInfo)) := trees.map <| fun t => t.findAllInfo none only_term (stop := fun i => Bool.not <| only_declarations i)

  let terms: List (List (TermInfo × Option ContextInfo)) := terms_info.map <| fun t => t.flatMap (fun ⟨i, ctx?⟩ =>
    match i with
    | .ofTermInfo ti => match ti.stx.getHeadInfo with
      | .original .. => [⟨ti, ctx?⟩]
      | _ => []
    | _ => [])

  let optional_conclusions := terms.map <| fun ts => maxTermNode ts
  pure (optional_conclusions.flatMap <| fun c =>
    match c with
    | some s => [s]
    | _ => [])

[Jannis Limperg]

This would be easier to do if you don't hook into the InfoTree (where you first need to find all the commands), but into the code that actually calls elabCommand. At that point, you have the Syntax object and you can match on it to extract the conclusion. Is that an option?

[Jannis Limperg]

Btw, extracting the conclusion syntactically implies that the following theorems are treated differently:

theorem t1 : A -> B
theorem t2 (a : A) : B

If you want to avoid this, you should probably go to the Expr level, i.e. get the type Exprs of all theorems in the file (this is actually quite annoying to do), do a forallTelescope to get the conclusion and pretty-print it. However, this introduces potential issues where the pretty-printer produces syntax that can't be elaborated for various reasons.

[Kyle Miller]

Could you say a bit about what will consume this collected information?

It's possible for example to take all the theorems in an imported module, get their conclusions as Exprs, and pretty print them. By "conclusion" I mean "the innermost body of universal quantification", which tends to be what's after : but isn't guaranteed to be the exact point (ah, Jannis just mentioned this while I was writing this comment)

[Simon Sorg]

Jannis Limperg said:

Btw, extracting the conclusion syntactically implies that the following theorems are treated differently:

theorem t1 : A -> B
theorem t2 (a : A) : B

If you want to avoid this, you should probably go to the Expr level, i.e. get the type Exprs of all theorems in the file (this is actually quite annoying to do), do a forallTelescope to get the conclusion and pretty-print it. However, this introduces potential issues where the pretty-printer produces syntax that can't be elaborated for various reasons.

I remember facing some delaborator issues like this with definite integrals a few months ago, which is why I'd like to stay at syntax. But your point on theorem t1: A -> B is quite convincing, thanks!

[Simon Sorg]

Kyle Miller said:

Could you say a bit about what will consume this collected information?

It's possible for example to take all the theorems in an imported module, get their conclusions as Exprs, and pretty print them. By "conclusion" I mean "the innermost body of universal quantification", which tends to be what's after : but isn't guaranteed to be the exact point (ah, Jannis just mentioned this while I was writing this comment)

Okay, so I simply want to either a) negate a conclusion or b) replace a conclusion with False automatically. For the latter, using Expr should not be a problem, but I'm a bit afraid of how this would work for the former. But I guess I could just wrap the conclusion Expr with a negation into the corresponding Expr.

[Kyle Miller]

Could you say more about what you want to do? What's the output? A negated theorem could mean an Expr, some Syntax, some source code to paste in, etc. There are lots of options for lots of applications, so this is why I'm asking about what will consume the data and how.

[Simon Sorg]

Kyle Miller said:

Could you say more about what you want to do? What's the output? A negated theorem could mean an Expr, some Syntax, some source code to paste in, etc. There are lots of options for lots of applications, so this is why I'm asking about what will consume the data and how.

Sure, sorry! Thanks for the patience so far! It's for Automated Theorem Proving via an external tool I'm working on (ideally not just LLM slop) - so I would like to have Lean code I can feed into c++ as string.
Ideally, it would be source code to paste in.
I take the string, do some processing in c++, and feed it back to Lean. So the negated conclusion's statement itself should make valid Lean source code.
Since this should be achievable from Syntax too (please correct me here), Syntax is also fine. But that's why I'm a bit hesitant with Expr.

[Simon Sorg]

Jannis Limperg said:

Btw, extracting the conclusion syntactically implies that the following theorems are treated differently:

theorem t1 : A -> B
theorem t2 (a : A) : B

If you want to avoid this, you should probably go to the Expr level, i.e. get the type Exprs of all theorems in the file (this is actually quite annoying to do), do a forallTelescope to get the conclusion and pretty-print it. However, this introduces potential issues where the pretty-printer produces syntax that can't be elaborated for various reasons.

So I did this now (and the InfoTree was quite helpful in getting the correct Expr terms).

let conclusion: Expr → MetaM String := fun (expr: Expr) => do pure (← Meta.ppExpr (← Lean.Meta.forallMetaTelescope (← Meta.inferType expr)).snd.snd).pretty'

which gives the following outputs:

theorem a : 1 + 1 = 2 := by rfl --1 + 1 = 2
theorem b : (p : Prop) -> (h : p) -> p := by intro p h; exact h --?p
theorem c (p : Prop) (h : p) : p := by exact h --?p

Quite amazing! For further processing, it should suffice to strip away the ?, and then treat this as this the conclusion. Thanks!