Demonstrations for the theory of proveit.numbers.ordering ¶

import proveit
%begin demonstrations

from proveit import ExprTuple, extract_var_tuple_indices, ProofFailure
from proveit.core_expr_types import Len
from proveit.logic import Equals, InSet, Not
from proveit.numbers import (zero, one, two, three, four, num, 
                             Add, Neg, frac)
from proveit.numbers import (
        Integer, Natural, NaturalPos, IntegerNeg, IntegerNonZero, Real, Less,
        LessEq, greater, greater_eq, Min, Max)
from proveit.numbers import number_ordering
from proveit import a, b, c, d, e, n, t, u, v, w, x, y, z, rho
import random

Transitivity search¶

assumptions = [greater_eq(t, a), Less(t, u), Equals(u, v), LessEq(v, w), greater(x, w), Less(x, y), greater_eq(z, y), Less(u, z), greater(w, t)]

random.shuffle(assumptions)

Less(a, z).prove(assumptions=assumptions)

greater(z, a).prove(assumptions=assumptions)

Transitivity sort¶

from proveit.numbers import one, four, Less
Less.sort([one, four], reorder=False)

assumptions = [Less(b, a), greater_eq(c, a), Equals(c, d), LessEq(d, e)]

We can use Less.sort as long as we only have strict ordering relations between the items being sorted (i.e., no $\leq$).

to_sort = [b, e]
random.shuffle(to_sort)
random.shuffle(assumptions)
print(to_sort)

Less.sort(to_sort, assumptions=assumptions)

[b, e]

Otherwise, if $\leq$ is involved, use LessEq.sort.

to_sort = [b, c, e]
random.shuffle(to_sort)
random.shuffle(assumptions)
print(to_sort)
LessEq.sort(to_sort, assumptions=assumptions)

[e, c, b]

to_sort = [a, b, c, e]
random.shuffle(to_sort)
random.shuffle(assumptions)
print(to_sort)
LessEq.sort(to_sort, assumptions=assumptions)

[a, e, c, b]

to_sort = [a, b, c, d, e]
random.shuffle(to_sort)
random.shuffle(assumptions)
print(to_sort)
LessEq.sort(to_sort, assumptions=assumptions)

[c, a, d, b, e]

LessEq(one, four).prove(automation=False)

to_sort = [a, b, c, d, e]
random.shuffle(to_sort)
random.shuffle(assumptions)
print(to_sort)
LessEq.sort(to_sort, assumptions=assumptions)

[b, a, d, e, c]

to_sort = [a, b, c, d, e]
random.shuffle(to_sort)
random.shuffle(assumptions)
print(to_sort)
LessEq.sort(to_sort, assumptions=assumptions)

[d, c, b, a, e]

Number ordering¶

A number ordering is simply a total-ordering style for presenting a conjunction of number ordering relations.

ordering = number_ordering(Less(w, x), LessEq(x, y), Less(y, z)).prove(
    assumptions=[Less(w, x), LessEq(x, y), Less(y, z)])

ordering.expr_info()

Min and Max closure¶

# some number sets for testing
from proveit.numbers import (
        NaturalPos, IntegerNeg, Natural, IntegerNonPos, IntegerNonZero, Integer,
        RationalPos, RationalNeg, RationalNonNeg, RationalNonPos, RationalNonZero, Rational,
        RealPos, RealNeg, RealNonNeg, RealNonPos, RealNonZero, Real, ComplexNonZero, Complex)

InSet(Max(a, b, c), Real).prove(
    assumptions=[InSet(a, Real), InSet(b, Real), InSet(c, Real)])

InSet(Max(a, b, c), Integer).prove(
    assumptions=[InSet(a, Integer), InSet(b, Integer), InSet(c, Integer)])

Max(a, b, c).deduce_in_number_set(Integer,
    assumptions=[InSet(a, Integer), InSet(b, Integer), InSet(c, Integer)])

Max(a, b, c).deduce_in_number_set(NaturalPos,
    assumptions=[InSet(a, NaturalPos), InSet(b, NaturalPos), InSet(c, NaturalPos)])

# Notice that this will work if the user-designated number_set just
# CONTAINS the number sets in which the arguments exist
InSet(Max(a, b, c), Integer).prove(
    assumptions=[InSet(a, NaturalPos), InSet(b, NaturalPos), InSet(c, NaturalPos)])

# Notice that this will work even if the user-designated number_set
# simply CONTAINS the number sets in which the arguments exist
InSet(Max(a, b, c), Integer).prove(
    assumptions=[InSet(a, NaturalPos), InSet(b, Natural), InSet(c, IntegerNeg)])

InSet(Max(a, b, c), NaturalPos).prove(
    assumptions=[InSet(a, NaturalPos), InSet(b, NaturalPos), InSet(c, NaturalPos)])

InSet(Min(a, b, c), Real).prove(
    assumptions=[InSet(a, Real), InSet(b, Real), InSet(c, Real)])

InSet(Min(a, b, c), Integer).prove(
    assumptions=[InSet(a, Natural), InSet(b, IntegerNeg), InSet(c, NaturalPos)])

Min and Max evaluation, simplification (testing & development)¶

from proveit.numbers.ordering import max_def_bin
max_def_bin

temp_max_assumptions = [InSet(a, Real), InSet(b, Real),
                    InSet(c, Real), InSet(d, Real),
                    greater_eq(a, b), greater(c, a), Less(d, b)]

# notice that the assumptions then imply that c > d
greater(c, d).prove(assumptions=temp_max_assumptions)

# instantiating the Max definition axiom for binary
_x_sub = a
_y_sub = b
max_def_bin_inst = max_def_bin.instantiate(
    {x: _x_sub, y: _y_sub},
    assumptions=temp_max_assumptions,
    auto_simplify=False)

# then simplify/evaluate with assumptions about a, b relation
max_def_bin_inst.inner_expr().rhs.simplify(assumptions=temp_max_assumptions)

# alternatively, execute the definition() method:
Max(a, b).definition(assumptions=temp_max_assumptions)

# Notice that side_effects for a <= b include Not(b < a):
Not(Less(b, a)).prove(assumptions=[InSet(a, Real), InSet(b, Real), LessEq(a, b)])

# And notice side effects of Not(a > b) include a <= b
LessEq(a, b).prove(
        assumptions=[InSet(a, Real), InSet(b, Real), Not(greater(a, b))])

Max(a, b).simplification(assumptions=[InSet(a, Real), InSet(b, Real), greater_eq(a, b)])

max_multi_test = Max(a, b, c, d)

max_multi_test_01 = max_multi_test.definition(assumptions=temp_max_assumptions)

# And to see an intermediate step that was already simplified above,
# try the same without auto_simplify:
max_multi_test_02 = max_multi_test.definition(
    assumptions=temp_max_assumptions, auto_simplify=False)

max_multi_test_01.lhs.simplification(assumptions=temp_max_assumptions)

# As long as we know the arg is Real, Max(arg) = arg.
Max(a).definition(assumptions=temp_max_assumptions)

Max(a).simplification(assumptions=temp_max_assumptions)

# If we don't know the relationship between a and b,
# we simply get a self-equality in the binary case
Max(a, b).simplification()

# If we only know 2nd op ≥ 1st op? This now simplifies nicely as well.
Max(a, b).simplification(assumptions=[InSet(a, Real), InSet(b, Real), greater_eq(b, a)])

temp_min_assumptions = [
        InSet(a, Real), InSet(b, Real), InSet(c, Real), InSet(d, Real),
        LessEq(b, a), Less(a, c), Less(d, b)]

min_multi_test = Min(a, b, c, d)

# Notice here that the assumptions allow us to INFER that b < c
# but b < c is not actually present as an assumption, so processing stops
min_multi_test_01 = min_multi_test.definition(assumptions=temp_min_assumptions)

# but if we then augment the assumptions with an explicit b < c
# we obtain a complete reduction
min_multi_test_01 = min_multi_test.definition(
        assumptions=temp_min_assumptions+[Less(b, c)])

# As long as we know the arg is Real, Min(arg) = arg.
Min(a).definition(assumptions=temp_min_assumptions)

Min(a).simplification(assumptions=temp_min_assumptions)

# If we don't know the relationship between a and b,
# we simply get a self-equality in the binary case
Min(a, b).simplification()

`LessEq.add_left` and `LessEq.add_right`¶

a_less_eq_b = LessEq(a, b)

a_less_eq_b.add_left(Neg(three), assumptions=[InSet(a, Real), InSet(b, Real), a_less_eq_b])

a_less_eq_b.add_right(three, assumptions=[InSet(a, Real), InSet(b, Real), a_less_eq_b])

# shouldn't be able to add_left a positive value to a LessEq:
try:
    a_less_eq_b.add_left(three, assumptions=[InSet(a, Real), InSet(b, Real), a_less_eq_b])
    print("Shouldn't get this far!")
except ProofFailure as the_error:
    print("ProofFailure, InstantiationFailure: {}".format(the_error))

ProofFailure, InstantiationFailure: Proof step failed assuming {a in Real, b in Real, a <= b}:
Attempting to instantiate |- forall_{a, b, c in Real | a <= b, c <= 0} ((a + b) <= c) with {a: a, b: b, c: 3}:
Unsatisfied condition: 3 <= 0. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

d_greater_eq_c = greater_eq(d, c)

d_greater_eq_c.add_left(three, assumptions=[InSet(c, Real), InSet(d, Real), d_greater_eq_c])

d_greater_eq_c.add_right(Neg(three), assumptions=[InSet(c, Real), InSet(d, Real), d_greater_eq_c])

# shouldn't be able to add_right a positive value to a greater_eq:
try:
    d_greater_eq_c.add_right(three, assumptions=[InSet(c, Real), InSet(d, Real), d_greater_eq_c])
    print("Shouldn't get this far!")
except ProofFailure as the_error:
    print("ProofFailure, InstantiationFailure: {}".format(the_error))

ProofFailure, InstantiationFailure: Proof step failed assuming {c in Real, d in Real, d >= c}:
Attempting to instantiate |- forall_{a, b, c in Real | a <= b, c <= 0} ((a + b) <= c) with {a: c, b: d, c: 3}:
Unsatisfied condition: 3 <= 0. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

Work & Notes Related to the Creation of a `merging_dict` and Related merging function(s)¶

Create a 'merging_dict' that maps each pair of standard number sets to the minimal standard number set that includes both. This dictionary can then be found in the number_operation.py file in the proveit.numbers package. Un-comment the following two code cells to see this in action:

# from proveit.numbers import (
#         NaturalPos, IntegerNeg, Natural, IntegerNonPos, IntegerNonZero, Integer,
#         RationalPos, RationalNeg, RationalNonNeg, RationalNonPos, RationalNonZero, Rational,
#         RealPos, RealNeg, RealNonNeg, RealNonPos, RealNonZero, Real, ComplexNonZero, Complex)
# sorted_number_sets = (
#     NaturalPos, IntegerNeg, Natural, IntegerNonPos, IntegerNonZero, Integer,
#     RationalPos, RationalNeg, RationalNonNeg, RationalNonPos, RationalNonZero, Rational,
#     RealPos, RealNeg, RealNonNeg, RealNonPos, RealNonZero, Real, ComplexNonZero, Complex)
# merging_dict = {}
# for i in range(0, len(sorted_number_sets)):
#     print(sorted_number_sets[i])
#     for j in range (i+1, len(sorted_number_sets)):
#         for number_set in sorted_number_sets:
#             if (number_set.includes(sorted_number_sets[i])
#                 and number_set.includes(sorted_number_sets[j])):
#                 merging_dict[(sorted_number_sets[i], sorted_number_sets[j])] = number_set
#                 break

The merging_dict then looks like this:

# merging_dict

Automation via canonical forms¶

expr = Less(Add(t, three), four)
display(expr)
expr.canonical_form()

expr.prove(assumptions=[Less(t, one), InSet(t, Real)])

expr = Less(Add(t, three), num(6))
display(expr)
expr.canonical_form()

expr.prove(
    assumptions=[Less(t, one), InSet(t, Real)])

expr = Less(Add(frac(t, two), three), num(5))
display(expr)
expr.canonical_form()

expr.prove(assumptions=[Less(t, one), InSet(t, Real)])

Make sure simple numeric cases work as a special case

Less(zero, num(5)).prove()

Less(two, num(10)).prove()

Less(four, one).disprove()

Less(Neg(two), four).prove()

Less(three, Neg(one)).disprove()

Less(frac(one, two), frac(two, three)).prove()

Less(frac(one, three), frac(one, two)).prove()

Less(frac(Neg(one), three), frac(one, two)).prove()

%end demonstrations

	core type	sub-expressions
0	Operation	operator: 1 operands: 2
1	Literal
2	ExprTuple	3, 4, 5
3	Operation	operator: 9 operands: 6
4	Operation	operator: 7 operands: 8
5	Operation	operator: 9 operands: 10
6	ExprTuple	11, 12
7	Literal
8	ExprTuple	12, 13
9	Literal
10	ExprTuple	13, 14
11	Variable
12	Variable
13	Variable
14	Variable

Demonstrations for the theory of proveit.numbers.ordering¶