Basic unverified symbolic calculations in Lean4 using PARI

Stream: lean4

[Anand Rao Tadipatri]

I have implemented some code for performing some quick unverified arithmetic and symbolic calculations in Lean4, using PARI/GP as a backend (this was inspired by a comment of @Siddhartha Gadgil after a lecture by @Kevin Buzzard today). This kind of interface is ideal for cases where one wants to do some quick calculations, say to plug in a suitable expression to close the goal, without leaving the Lean editor. The code is currently limited to only calculations involving the basic arithmetic operations, but can (in principle) be extended to do more.

Running it requires having PARI/GP installed; on Arch Linux, this can be done by running pacman -S pari. The code is available here, and is about 50 lines long.

import Lean

open Lean Elab Term Meta Tactic

declare_syntax_cat arith
syntax str : arith
syntax ident : arith
syntax num : arith
syntax arith "+" arith : arith
syntax arith "-" arith : arith
syntax arith "*" arith : arith
syntax arith "/" arith : arith
syntax arith "^" arith : arith
syntax "(" arith ")" : arith

partial def arithToString : TSyntax `arith → String
  | `(arith| $x:str) => x.getString
  | `(arith| $a:ident) => toString a.getId
  | `(arith| $n:num) => toString n.getNat
  | `(arith| $a + $b) => s!"{arithToString a} + {arithToString b}"
  | `(arith| $a - $b) => s!"{arithToString a} - {arithToString b}"
  | `(arith| $a * $b) => s!"{arithToString a} * {arithToString b}"
  | `(arith| $a / $b) => s!"{arithToString a} / {arithToString b}"
  | `(arith| $a ^ $b) => s!"{arithToString a} ^ {arithToString b}"
  | `(arith| ($a)) => s!"({arithToString a})"
  | _ => panic! "Invalid `arith` syntax"

open IO.Process in -- code by Max Nowak from https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/external.20process/near/345090183
/-- Pipe input into stdin of the spawned process, then return output upon completion. -/
def cmd_with_stdin (args : SpawnArgs) (input : String) : IO Output := do
  let child <- spawn { args with stdin := .piped, stdout := .piped, stderr := .piped }
  let (stdin, child) <- child.takeStdin
  stdin.putStr input
  stdin.flush
  let stdout <- IO.asTask child.stdout.readToEnd Task.Priority.dedicated
  let stderr <- child.stderr.readToEnd
  let exitCode <- child.wait
  let stdout <- IO.ofExcept stdout.get
  return { exitCode, stdout, stderr }

def queryPari (a : TSyntax `arith) : IO String := do
  let out ← cmd_with_stdin
              { cmd := "gp", args := #["-q"]}
              <| arithToString a
  return out.stdout

elab "#symbolic" e:arith : command => do
  -- dbg_trace (arithToString e)
  let out ← queryPari e
  logInfoAt e out

#symbolic 2 + 2                    -- 4
#symbolic (x ^ 2 - 1) / (x + 1)    -- x - 1
#symbolic (x + 2) * (8 * x + 17)   -- 8*x^2 + 33*x + 34

[Kevin Buzzard]

Ha ha! I was switching windows to do polynomial calculations and then verifying the solutions in lean. Nice!

[Shreyas Srinivas]

Can this be integrated with mathlib? Seems useful in many places.

[Siddhartha Gadgil]

By the way @Anand Rao it may be useful to have a term elaborator with this (using runParserCategorty).

[Miguel Marco]

Can this same technique be used with other computer algebra systems, or is it pari specific?

I was thinking, for example, of using it for running polyrith without depending on an internet connection.

[Anand Rao Tadipatri]

Shreyas Srinivas said:

Can this be integrated with mathlib? Seems useful in many places.

I'd be glad to open a PR to mathlib4, perhaps after adding a few minor improvements.

[Anand Rao Tadipatri]

Miguel Marco said:

Can this same technique be used with other computer algebra systems, or is it pari specific?

I was thinking, for example, of using it for running polyrith without depending on an internet connection.

In principle, it can be used with any computer algebra system that supports a command-line interface. It should be possible to use such a set-up for polyrith - where the tactic first attempts to run the computation with a locally-installed CAS and turns to using the internet only when the user has no CAS installed locally.

[Anand Rao Tadipatri]

Siddhartha Gadgil said:

By the way Anand Rao it may be useful to have a term elaborator with this (using runParserCategorty).

I have now added a tactic which interprets the answer back as a Lean term and attempts to prove that it is equal to the original expression using ring/linarith/norm_num.

def arithToTerm (a : TSyntax `arith) : TacticM <| TSyntax `term := do
  let .some s ← pure a.raw.reprint | failure
  let .ok stx ← pure $ Parser.runParserCategory (← getEnv) `term s | failure
  return ⟨stx⟩

elab "symb_calc" a:arith : tactic => do
  let out ← queryPari <| arithToString a
  let res ← ofExcept <| Parser.runParserCategory (← getEnv) `arith out
  let lhs : TSyntax `term ← arithToTerm a
  let rhs : TSyntax `term ← arithToTerm ⟨res⟩
  logInfo m!"{lhs} = {rhs}"
  evalTactic <| ← `(tactic| have : $lhs = $rhs := ?_; swap; first | ring | linarith | norm_num)

example (a : Int) : (a + 3) * (a + 5) = (a + 5) * (a + 3) := by
  symb_calc (a + 3) * (a + 5) -- (a + 3) * (a + 5) = a ^ 2 + 8 * a + 15
  rw [this]
  symb_calc (a + 5) * (a + 3) -- (a + 5) * (a + 3) = a ^ 2 + 8 * a + 15
  rw [this]

[Anand Rao Tadipatri]

I have also added a utility for running arbitrary PARI calculations from Lean, treating both the input and output as strings. Here is the code:

def queryPari (s : String) : IO String := do
  let out ← cmd_with_stdin { cmd := "gp", args := #["-q"]} s
  return out.stdout

elab "#pari" c:str : command => do
  let out ← queryPari c.getString
  logInfo out

#pari "nextprime(35)" -- 37

It will require a considerable amount of work to interpret the strings back as Lean terms for general PARI calculations.