What would interactive use of a simplifier look like?

Stream: Computer algebra

[Niels Voss]

I don't know anything about how computer algebra systems actually work, but here are some random thoughts:

In SageMath I can do something like

var('x')
expr = 3*x + 2*log(exp(x))
print(expr) # 3*x + 2*log(e^x)
print(expr.simplify()) # 5*x

What would such a thing look like in Lean?

My understanding is that in Sage and SymPy (and maybe other CAS languages, not sure about Mathematica) they construct a special type of symbolic expressions and then implement operator overloading on them to allow multiplying expressions. Then functions like exp take in symbolic expressions and spit out symbolic expressions. In Lean, functions like exp take in actual real numbers and spit out actual real numbers, which is very different.

We could of course use the Sage/SymPy approach of having a new custom type of expressions, but I think it's possible to do better. There's already an Expr type in Lean, so we could just use that as our type of expressions. This has the following advantages:

1. Expressions of type Q(Int) actually correspond to object-level integers, whereas to my knowledge symbolic expressions about integers in Sage don't really have anything to do with sage integers.
2. When we define a function like Real.exp : Real -> Real, then we don't have to define another function exp : Expr -> Expr.
3. If we had a simplifier of type Expr -> Expr or Expr -> M Expr for some monad M, then we could use the same simplifier as a tactic for normal theorem proving.
4. If we want some assurance of correctness, we don't actually have to formally verify the correctness of the simplifier (which would require formally defining the semantics of expressions), since we can instead just make the simplifier proof-producing, like a tactic.

Let's suppose we already have access to some powerful simplifier of type Expr -> Expr or Expr -> M Expr, which maybe produces proofs of correctness as well (so let's say we aren't worried about what algorithms to use right now). How would we invoke that in Lean?

The most direct equivalent of the Sage code, where we use Expr instead of a custom expression type, would be something like

import Mathlib
open Real Qq Lean

def mysimplifier : Expr → Expr := id -- pretend this has a more interesting definition

-- Realistically, a simplifier would probably need some way to know that `x` is a Real number
-- which we don't provide right now.
def x : Q(ℝ) := Expr.fvar (Lean.FVarId.mk `x)
def expr : Q(ℝ) := (fun x ↦ q(3 * $x + 2 * log (exp $x))) x
  -- Ideally I would just write `def expr := q(3 * $x + 2 * log (exp $x))` but this gave me an error

#eval Lean.PrettyPrinter.ppExpr expr -- 3 * x + 2 * Real.log (rexp x)
#eval Lean.PrettyPrinter.ppExpr (mysimplifier expr) -- result of simplification

But maybe there are some better ways to do this? Like, maybe we can reflect definitions from the object level to the meta level somehow?

import Mathlib
open Real Lean

def mysimplifier : Expr → Expr := id -- pretend this has a more interesting definition
def reflect : Name → Expr := sorry -- some function which converts a declaration name to its actual expression

variable (x : ℝ)
def e := 3 * x + 2 * log (exp x)

#eval Lean.PrettyPrinter.ppExpr (reflect `e)
#eval Lean.PrettyPrinter.ppExpr (mysimplifier (reflect `e))

Or, we could make no attempt to reflect the definition of e at all and just create an expression at the time of invoking the simplifier:

import Mathlib
open Real Qq Lean

def mysimplifier : Expr → Expr := id -- pretend this has a more interesting definition

variable (x : ℝ)
def x_expr : Q(ℝ) := Expr.fvar (Lean.FVarId.mk `x)
def e := 3 * x + 2 * log (exp x)

#eval Lean.PrettyPrinter.ppExpr ((fun x ↦ q(e $x)) x_expr) -- e x
  -- Ideally I would like to have just written `q(e $x_expr)`, but this gave me an error.
#eval Lean.PrettyPrinter.ppExpr (mysimplifier ((fun x ↦ q(e $x)) x_expr)) -- result of simplification

In any case, this seems like a difficult problem to solve. Does anyone have any thoughts on how this should be done?

[Ilmārs Cīrulis]

TIL about the Expr type. Thank you!

[Ilmārs Cīrulis]

In my opinion, the common and the most important part of all three cases is the mysimplifier function. And all three ways to use it seems to be valid, at first glance.

[Niels Voss]

For the sake of this question, I am assuming that we already have a mysimplifier function, and I'm wondering what the most ergonomic way to invoke it would be.

I guess my question is maybe a little bit more general: In the long run, if we wanted Lean to become a viable alternative to Sage, Matlab, Mathematica, Maple, Python, etc. (assuming sufficient labor was available), what would an average user's session look like in the best case scenario, and how do we best take advantage of Lean's unique features (e.g. dependent types, powerful metaprogramming, and extensible UI)?

This is of course a hypothetical question, because we don't have the labor to match Mathematica. But I think it's still an important question.

[Jacques Carette]

A lot depends on what theorems you will want to prove. There is a huge amount of related work on coupling CAS and proof assistants.

[Jacques Carette]

There is also work (by yours truly) on defining what 'simplification' means.

[Andrés Goens]

Jacques Carette said:

There is also work (by yours truly) on defining what 'simplification' means.

that sounds interesting, do you mind pointing us to said work?

[Marcus Rossel]

(Ignoring the example implementation) are you looking for something in this direction?

import Mathlib
open Lean Meta Elab Term Command Real

noncomputable section

elab "#apply " simp:ident " to " tgt:term : command => liftTermElabM do
  let tgt ← elabTerm tgt none
  let simp ← elabTerm simp none
  let expr := Lean.mkConst ``Expr
  let simp ← unsafe evalExpr (Expr → TermElabM Expr) (← mkArrow expr (← mkAppM ``TermElabM #[expr])) simp
  let result ← simp tgt
  logInfo result

-- Example:

variable (x : ℝ)
def e := 3 * x + 2 * log (exp x)

-- "Simplifiers":

def nothing : Expr → TermElabM Expr := pure

#apply nothing to e -- e

def zero (_ : Expr) : TermElabM Expr := do
  elabTerm (← `(0)) (mkConst ``Real)

#apply zero to e -- 0

[Jacques Carette]

Understanding Expression Simplification published at ISSAC 2004.

Quick take-home:

• simplification is "denotationally equivalent yet representationally shorter"
• the only stable notion of representation length is Kolmogorov complexity (which is uncomputable but easily approximable)

• consequences:

  1. minor differences in length may be an illusion of 'simpler' due to encoding
  2. definitional extensions are a crucial component of 'simpler'.