Skip to content

Expressions and Domains

Building Expressions

LeanCert uses symbolic expressions that are reified to the Lean AST.

Variables

import leancert as lc

x = lc.var('x')
y = lc.var('y')

Constants

c = lc.const(3.14159)
half = lc.const(1, 2)  # Fraction 1/2

Arithmetic

expr = x**2 + 2*x + 1
expr = (x + y) / (x - y)

Transcendental Functions

lc.sin(x)
lc.cos(x)
lc.exp(x)
lc.log(x)
lc.tan(x)
lc.atan(x)
lc.sinh(x)
lc.cosh(x)
lc.tanh(x)
lc.arsinh(x)
lc.atanh(x)

Special Functions

lc.sinc(x)  # sin(x)/x with sinc(0) = 1
lc.erf(x)   # Error function

Min/Max/Clamp

lc.Min(x, y)
lc.Max(x, y)
lc.clamp(x, lo, hi)  # Equivalent to Min(Max(x, lo), hi)

Domain Specification

Intervals

from leancert import Interval

I = Interval(0, 1)       # [0, 1]
I = Interval(-1, 1)      # [-1, 1]
I = Interval("1/3", 1)   # [1/3, 1] (exact rational)

Boxes (Multi-dimensional)

from leancert import Box

# Using a dictionary
box = Box({'x': (0, 1), 'y': (-1, 1)})

# Or pass directly to solver functions
result = lc.find_bounds(x + y, {'x': (0, 1), 'y': (0, 1)})

Simplification

LeanCert includes symbolic simplification to mitigate the dependency problem in interval arithmetic.

leancert.simplify.simplify(expr)

Simplify an expression algebraically.

This applies multiple simplification strategies: 1. Constant folding (2 + 3 -> 5) 2. Identity removal (x + 0 -> x, x * 1 -> x) 3. Zero propagation (x * 0 -> 0) 4. Negation simplification (--x -> x) 5. Like term collection in polynomial form 6. Subexpression cancellation

Parameters:

Name Type Description Default
expr Expr

Expression to simplify

 required

Returns:

Type Description
Expr

Simplified expression (mathematically equivalent)
Source code in python/leancert/simplify.py 
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
def simplify(expr: Expr) -> Expr:
    """
    Simplify an expression algebraically.

    This applies multiple simplification strategies:
    1. Constant folding (2 + 3 -> 5)
    2. Identity removal (x + 0 -> x, x * 1 -> x)
    3. Zero propagation (x * 0 -> 0)
    4. Negation simplification (--x -> x)
    5. Like term collection in polynomial form
    6. Subexpression cancellation

    Args:
        expr: Expression to simplify

    Returns:
        Simplified expression (mathematically equivalent)
    """
    # Convert to polynomial form, simplify, convert back
    poly = to_polynomial(expr)
    if poly is not None:
        return from_polynomial(poly)

    # Fall back to recursive simplification for non-polynomial expressions
    return _simplify_recursive(expr)

leancert.simplify.expand(expr)

Fully expand an expression (distribute multiplication over addition).

This is useful when you want to expose all terms for cancellation.

Source code in python/leancert/simplify.py 
350
351
352
353
354
355
356
357
358
359
def expand(expr: Expr) -> Expr:
    """
    Fully expand an expression (distribute multiplication over addition).

    This is useful when you want to expose all terms for cancellation.
    """
    poly = to_polynomial(expr)
    if poly is not None:
        return from_polynomial(poly)
    return _simplify_recursive(expr)

Example

x = lc.var('x')

# Without simplification, (x*100 + 5) - (x*100) on [0, 1e10]
# would give bounds like [-1e12, 1e12] due to dependency

# With simplification, it reduces to 5
expr = (x * 100 + 5) - (x * 100)
simplified = lc.simplify(expr)
# simplified is const(5)

Expression Reference

leancert.expr.Expr

Bases: ABC

Base class for symbolic expressions.

Expressions are immutable and can be composed using Python operators. They track their free variables and can be compiled to kernel representation.

Source code in python/leancert/expr.py 
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
class Expr(ABC):
    """
    Base class for symbolic expressions.

    Expressions are immutable and can be composed using Python operators.
    They track their free variables and can be compiled to kernel representation.
    """

    @abstractmethod
    def free_vars(self) -> FrozenSet[str]:
        """Return all variable names used in this expression."""
        ...

    @abstractmethod
    def compile(self, var_order: list[str]) -> KernelExpr:
        """
        Compile to De Bruijn representation given variable ordering.

        Args:
            var_order: List of variable names. Index in list = De Bruijn index.

        Returns:
            JSON-serializable dict for the Lean kernel.

        Raises:
            CompilationError: If a variable is not in var_order.
        """
        ...

    @abstractmethod
    def evaluate(self, env: EvalEnv) -> EvalResult:
        """
        Evaluate the expression concretely using Python math.

        Used for counterexample verification to filter false positives.
        When the solver reports a potential bug, we evaluate the expression
        at the reported point using standard Python arithmetic. If the
        concrete value doesn't violate the bound, it's a false positive
        caused by interval over-approximation.

        Args:
            env: Dictionary mapping variable names to concrete values.

        Returns:
            The concrete value (float for transcendentals, Fraction for polynomials).

        Raises:
            ValueError: If a required variable is not in env.
        """
        ...

    # Operator overloading for natural math syntax
    def __neg__(self) -> Expr:
        return Neg(self)

    def __add__(self, other: ExprLike) -> Expr:
        return Add(self, _to_expr(other))

    def __radd__(self, other: ExprLike) -> Expr:
        return Add(_to_expr(other), self)

    def __sub__(self, other: ExprLike) -> Expr:
        return Sub(self, _to_expr(other))

    def __rsub__(self, other: ExprLike) -> Expr:
        return Sub(_to_expr(other), self)

    def __mul__(self, other: ExprLike) -> Expr:
        return Mul(self, _to_expr(other))

    def __rmul__(self, other: ExprLike) -> Expr:
        return Mul(_to_expr(other), self)

    def __truediv__(self, other: ExprLike) -> Expr:
        return Div(self, _to_expr(other))

    def __rtruediv__(self, other: ExprLike) -> Expr:
        return Div(_to_expr(other), self)

    def __pow__(self, n: int) -> Expr:
        if not isinstance(n, int) or n < 0:
            raise ValueError("Only non-negative integer powers are supported")
        return Pow(self, n)

free_vars() abstractmethod

Return all variable names used in this expression.

Source code in python/leancert/expr.py 
53
54
55
56
@abstractmethod
def free_vars(self) -> FrozenSet[str]:
    """Return all variable names used in this expression."""
    ...

leancert.expr.var(name)

Create a symbolic variable with the given name.

Source code in python/leancert/expr.py 
624
625
626
627
628
629
630
def var(name: str) -> Variable:
    """Create a symbolic variable with the given name."""
    if not isinstance(name, str):
        raise TypeError(f"Variable name must be a string, got {type(name).__name__}")
    if not name:
        raise ValueError("Variable name cannot be empty")
    return Variable(name)

leancert.expr.const(value)

Create a constant expression.

Source code in python/leancert/expr.py 
633
634
635
def const(value: Union[int, float, Fraction]) -> Const:
    """Create a constant expression."""
    return Const(value)