Core

This is a proofs validator to help students and hobbyists do mathematical thinking and problem solving.

Helper functions

---

source

equation

 equation (name, variables, expression)

Creates a function with the given name, variables, and expression.

---

source

not_equals

 not_equals (lhs:Union[sympy.core.expr.Expr,sympy.core.basic.Basic],
             rhs:Union[sympy.core.expr.Expr,sympy.core.basic.Basic])

---

source

equals

 equals (lhs:sympy.core.expr.Expr, rhs:sympy.core.expr.Expr)

---

source

constant

 constant (value:Union[int,float])

---

source

variable

 variable (name:str)

equation('f', [variable('x'), variable('y')], 1 - (1 - variable('x'))*(1- variable('y')))

\(\displaystyle f{\left(x,y \right)} = - \left(1 - x\right) \left(1 - y\right) + 1\)

Core functionality

---

source

make_examples

 make_examples (domain:str, N:int, equation:str, positive_only:bool=False,
                increasing_only:bool=False)

For a given domain and equation, select N examples and generate a list of N input-output pairs. Currently, the domain can only be ‘real’, and one variable is assumed.

	Type	Default	Details
domain	str		Domain of the example equation
N	int		Number of examples
equation	str		Equation to generate examples for
positive_only	bool	False	Whether to only generate positive inputs
increasing_only	bool	False	Whether the domain should be increasing
Returns	typing.List[typing.Tuple[sympy.core.expr.Expr, sympy.core.expr.Expr]]		List of input-output pairs

examples = make_examples('real', 10, 'x**2')
print(examples)

[(82, 6724), (-46, 2116), (-1, 1), (88, 7744), (-96, 9216), (27, 729), (24, 576), (-89, 7921), (75, 5625), (-33, 1089)]

examples = make_examples('real', 10, 'x**2', increasing_only=True)
examples

[(94, 8836),
 (115, 13225),
 (147, 21609),
 (218, 47524),
 (224, 50176),
 (314, 98596),
 (354, 125316),
 (390, 152100),
 (398, 158404),
 (466, 217156)]

make_examples('real', 10, 'x**2', positive_only=True)

[(85, 7225),
 (45, 2025),
 (73, 5329),
 (69, 4761),
 (89, 7921),
 (56, 3136),
 (7, 49),
 (28, 784),
 (74, 5476),
 (20, 400)]

make_examples('real', 10, 'x**2', positive_only=True, increasing_only=True)

[(4, 16),
 (65, 4225),
 (97, 9409),
 (188, 35344),
 (278, 77284),
 (288, 82944),
 (341, 116281),
 (409, 167281),
 (503, 253009),
 (540, 291600)]

assert len(examples) == 10

test_fail(lambda: make_examples('complex', 10, 'x**2'), contains="Domain complex not supported.")

---

source

prove

 prove (goal:Union[sympy.core.relational.Equality,sympy.core.relational.Un
        equality,sympy.core.relational.Relational], proof_func:Callable[..
        .,Union[sympy.core.relational.Equality,sympy.core.relational.Unequ
        ality,sympy.core.relational.Relational]], *args)

Prove a goal using a proof function and arguments. The proof function should take the goal as the last argument and return the derived result. The goal is proved if the derived result matches the goal.

	Type	Details
goal	typing.Union[sympy.core.relational.Equality, sympy.core.relational.Unequality, sympy.core.relational.Relational]	Goal to prove
proof_func	typing.Callable[…, typing.Union[sympy.core.relational.Equality, sympy.core.relational.Unequality, sympy.core.relational.Relational]]	Proof function
args
Returns	bool	True if proof succeeds, False otherwise

test_eq(prove(equals(variable('x'), constant(2)), equals, variable('x'), constant(2)), True)

\[\text \quad x = 2 \quad Q.E.D.\]

result = prove(equals(variable('x'), constant(2)), equals, variable('x'), constant(3))
test_ne(result, True)

Proof failed: Derived result Eq(x, 3) does not match goal Eq(x, 2)
Check your assumptions and proof function for errors.

---

source

print_proof

 print_proof (proof:Callable[...,Union[sympy.core.relational.Equality,symp
              y.core.relational.Unequality,sympy.core.relational.Relationa
              l]], *args)

Print a proof step by step. Mostly used when defining a proof evaluation function. The proof function should take the goal as the last argument and return the derived result. The goal is proved if the derived result matches the goal. Comments do not support latex formatting, but the rest of the proof does.

	Type	Details
proof	typing.Callable[…, typing.Union[sympy.core.relational.Equality, sympy.core.relational.Unequality, sympy.core.relational.Relational]]	the proof function
args
Returns	None	no return value

def print_proof_example():
    # This is a test function to show how print_proof works
    x = variable('x')
    # again
    y = variable('y')
    return equals(x, y)

latex = Latex(print_proof(print_proof_example))

\[\mathtt{\text{This is a test function to show how print\_proof works}}\]

\[x\]

\[\mathtt{\text{again}}\]

\[y\]

---

source

contradiction_proof

 contradiction_proof (proof:Callable[...,Union[sympy.core.relational.Equal
                      ity,sympy.core.relational.Unequality,sympy.core.rela
                      tional.Relational]])

Wrap a proof function to prove a contradiction. The proof function should take the goal as the last argument and return the derived result. The goal is proved if the derived result matches the goal.

	Type	Details
proof	typing.Callable[…, typing.Union[sympy.core.relational.Equality, sympy.core.relational.Unequality, sympy.core.relational.Relational]]	the proof function
Returns	typing.Callable[…, sympy.core.relational.Unequality]	the wrapped contradiction proof function to evaluate

---

source

direct_proof

 direct_proof (proof:Callable[...,Union[sympy.core.relational.Equality,sym
               py.core.relational.Unequality,sympy.core.relational.Relatio
               nal]])

Wrap a proof function to prove a direct proof. The proof function should take the goal as the last argument and return the derived result. The goal is proved if the derived result matches the goal.

	Type	Details
proof	typing.Callable[…, typing.Union[sympy.core.relational.Equality, sympy.core.relational.Unequality, sympy.core.relational.Relational]]	the proof function
Returns	typing.Callable[…, sympy.core.relational.Equality]	the wrapped proof function to evaluate

Here’s how to use a contradiction goal.

# Start by defining your domain
arbitrary_x = variable("x")
expression = arbitrary_x + 1

# Then define your goal
contradiction_goal = not_equals(expression, arbitrary_x)

@contradiction_proof
def proof_of_x_plus_one(x):
    # Given x, Assume x + 1 = x is true for arbitrary_x
    assumed_eq = equals(x + 1, x)

    # Calculate x + 1
    next = x + 1

    # Observing x + 1 != x, we have reached a contradiction
    return not_equals(next, assumed_eq.rhs)

assert prove(contradiction_goal, proof_of_x_plus_one, arbitrary_x)
# assert added for nbdev test

\[\mathtt{\text{Given x, Assume x + 1 = x is true for arbitrary\_x}}\]

\[x + 1 = x\]

\[\mathtt{\text{Calculate x + 1}}\]

\[x + 1\]

\[\mathtt{\text{Observing x + 1 != x, we have reached a contradiction}}\]

\[\text \quad x + 1 \neq x \quad Q.E.D.\]