a single step fully verified using SymPy and Lean

As very simple example, start with the equation

T = 1/f 

where T is period of oscillation and f is frequency of oscillation. A transformation would be to multiply both sides by f to get

f T = 1

Verification of a step using a Computer Algebra System like SymPy

The single step above could be verified using a Computer Algebra System like SymPy. The generic form of the inference rule is "multiply both sides of (LHS=RHS) by feed to get (LHS*feed=RHS*feed)". To show the inference rule was correctly applied, we want to show that

LHS_in*feed == LHS_out
and
RHS_in*feed == RHS_out

Another way to describe the equivalence is that the difference should be zero:

LHS_in*feed - LHS_out = 0
and
RHS_in*feed - RHS_out = 0

That's the generic formulation of the inference rule check. In this step,

LHS_in = T
RHS_in = 1/f
feed = f
LHS_out = f T
RHS_out = 1

This check is implemented in line 496 of validate_steps_sympy.py as

import sympy
def multiply_both_sides_by(LHS_in, RHS_in, feed, LHS_out, RHS_out):
    diff1 = sympy.simplify(sympy.Mul(LHS_in, feed) - LHS_out)
    diff2 = sympy.simplify(sympy.Mul(RHS_in, feed) - RHS_out)
    if (diff1 == 0) and (diff2 == 0):
        return "valid"
    else:
        return "LHS diff is " + str(diff1) + "\n" + "RHS diff is " + str(diff2)

We can run that using

>>> import sympy
>>> print(sympy.__version__)
1.11.1
>>> f, T = sympy.symbols('f T')
>>> multiply_both_sides_by(T, 1/f, f, f*T, 1)
'valid'

Wahoo! The step has been validated using SymPy to show the inference rule is applied correctly.

The cool part is that the "multiply_both_sides()" Python function is generic to any input expression. The same check can be used for many different steps that use the inference rule. Using SymPy we can gain confidence that the expressions associated with a step were correctly transformed. 

Consistency of dimensionality using SymPy

In addition to evaluating the transformation of symbols in a step, we can verify the consistency of dimensions for each expression. That requires more than just the symbols -- the user will have to specify the dimensions of each symbol.

For example, in JSON for period T we have

        "9491": {
            "category": "variable",
            "dimensions": {
                "amount of substance": 0,
                "electric charge": 0,
                "length": 0,
                "luminous intensity": 0,
                "mass": 0,
                "temperature": 0,
                "time": 1
            },
            "latex": "T",
            "name": "period",
            "scope": [
                "real"
            ]
        },

The script validate_dimensions_sympy.py

>>> import sympy
>>> from sympy.physics.units import mass, length, time, temperature, luminous_intensity, amount_of_substance, charge  # type: ignore
>>> from sympy.physics.units.systems.si import dimsys_SI

>>> from sympy.parsing.latex import parse_latex
>>> sympy.srepr(parse_latex('T = 1/f'))

TODO
>>> determine_consistency = dimsys_SI.equivalent_dims( eval(str(LHS)), eval(str(RHS)) )

See https://physicsderivationgraph.blogspot.com/2020/07/function-latex-for-sympy.html

Verification of the step using Lean

To prove

(T=1/f) -> (f*T=1)

additional constraints are needed for reasoning around division by 0. If you expect to avoid negative or zero frequency or period, you could define f and T to have be "positive real numbers" (which exclude zero; non-negative reals include zero). This does define the context more precisely, but there is a price - we won’t have nearly as many proofs for positive reals as we have for reals. The alternative is to add additional hypotheses as constraints. The latter case (additional hypotheses) is favored.

import Mathlib.Data.Real.Basic
import Mathlib.Tactic -- Import standard tactics, specifically import Mathlib.Tactic.FieldSimp

theorem inversion_amultbeq1
  (a b : Real)
  (hb_ne_zero : b ≠ 0) :
  a = 1 / b <-> a * b = 1 := by
  -- field_simp clears the denominator 'b' on the LHS,
  -- turning (a = 1 / b) into (a * b = 1) automatically.
  field_simp [hb_ne_zero]