# Demonstrations for the theory of proveit.numbers.ordering¶

In [1]:
import proveit
%begin demonstrations

In [2]:
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,
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

In [3]:
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)]

assumptions:
In [4]:
random.shuffle(assumptions)

In [5]:
Less(a, z).prove(assumptions=assumptions)

, ,  ⊢
In [6]:
greater(z, a).prove(assumptions=assumptions)

, ,  ⊢

### Transitivity sort¶

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

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

assumptions:

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

In [9]:
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.

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

[e, c, b]

, , ,  ⊢
In [11]:
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]

, , ,  ⊢
In [12]:
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]

, , ,  ⊢
In [13]:
LessEq(one, four).prove(automation=False)

In [14]:
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]

, , ,  ⊢
In [15]:
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.

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

ordering: , ,  ⊢
In [17]:
ordering.expr_info()

core typesub-expressionsexpression
0Operationoperator: 1
operands: 2
1Literal
2ExprTuple3, 4, 5
3Operationoperator: 9
operands: 6
4Operationoperator: 7
operands: 8
5Operationoperator: 9
operands: 10
6ExprTuple11, 12
7Literal
8ExprTuple12, 13
9Literal
10ExprTuple13, 14
11Variable
12Variable
13Variable
14Variable

### Min and Max closure¶

In [18]:
# 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)

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

, ,  ⊢
In [20]:
InSet(Max(a, b, c), Integer).prove(
assumptions=[InSet(a, Integer), InSet(b, Integer), InSet(c, Integer)])

, ,  ⊢
In [21]:
Max(a, b, c).deduce_in_number_set(Integer,
assumptions=[InSet(a, Integer), InSet(b, Integer), InSet(c, Integer)])

, ,  ⊢
In [22]:
Max(a, b, c).deduce_in_number_set(NaturalPos,
assumptions=[InSet(a, NaturalPos), InSet(b, NaturalPos), InSet(c, NaturalPos)])

, ,  ⊢
In [23]:
# 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)])

, ,  ⊢
In [24]:
# 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)])

, ,  ⊢
In [25]:
InSet(Max(a, b, c), NaturalPos).prove(
assumptions=[InSet(a, NaturalPos), InSet(b, NaturalPos), InSet(c, NaturalPos)])

, ,  ⊢
In [26]:
InSet(Min(a, b, c), Real).prove(
assumptions=[InSet(a, Real), InSet(b, Real), InSet(c, Real)])

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

, ,  ⊢

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

In [28]:
from proveit.numbers.ordering import max_def_bin
max_def_bin

In [29]:
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)]

temp_max_assumptions:
In [30]:
# notice that the assumptions then imply that c > d
greater(c, d).prove(assumptions=temp_max_assumptions)

, ,  ⊢
In [31]:
# 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)

max_def_bin_inst: ,  ⊢
In [32]:
# then simplify/evaluate with assumptions about a, b relation
max_def_bin_inst.inner_expr().rhs.simplify(assumptions=temp_max_assumptions)

, ,  ⊢
In [33]:
# alternatively, execute the definition() method:
Max(a, b).definition(assumptions=temp_max_assumptions)

, ,  ⊢
In [34]:
# 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)])

, ,  ⊢
In [35]:
# 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))])

, ,  ⊢
In [36]:
Max(a, b).simplification(assumptions=[InSet(a, Real), InSet(b, Real), greater_eq(a, b)])

, ,  ⊢
In [37]:
max_multi_test = Max(a, b, c, d)

max_multi_test:
In [38]:
max_multi_test_01 = max_multi_test.definition(assumptions=temp_max_assumptions)

max_multi_test_01: , , , , , ,  ⊢
In [39]:
# 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_02: , , ,  ⊢
In [40]:
max_multi_test_01.lhs.simplification(assumptions=temp_max_assumptions)

, , , , , ,  ⊢
In [41]:
# As long as we know the arg is Real, Max(arg) = arg.
Max(a).definition(assumptions=temp_max_assumptions)

In [42]:
Max(a).simplification(assumptions=temp_max_assumptions)

In [43]:
# 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()

In [44]:
# 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)])

, ,  ⊢
In [45]:
temp_min_assumptions = [
InSet(a, Real), InSet(b, Real), InSet(c, Real), InSet(d, Real),
LessEq(b, a), Less(a, c), Less(d, b)]

temp_min_assumptions:
In [46]:
min_multi_test = Min(a, b, c, d)

min_multi_test:
In [47]:
# 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)

min_multi_test_01: , , , ,  ⊢
In [48]:
# 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)])

min_multi_test_01: , , , , , ,  ⊢
In [49]:
# As long as we know the arg is Real, Min(arg) = arg.
Min(a).definition(assumptions=temp_min_assumptions)

In [50]:
Min(a).simplification(assumptions=temp_min_assumptions)

In [51]:
# 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¶

In [52]:
a_less_eq_b = LessEq(a, b)

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

, ,  ⊢
In [54]:
a_less_eq_b.add_right(three, assumptions=[InSet(a, Real), InSet(b, Real), a_less_eq_b])

, ,  ⊢
In [55]:
# 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.

In [56]:
d_greater_eq_c = greater_eq(d, c)

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

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

, ,  ⊢
In [59]:
# 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.


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:

In [60]:
# 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:

In [61]:
# merging_dict


### Automation via canonical forms¶

In [62]:
expr = Less(Add(t, three), four)
display(expr)
expr.canonical_form()

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

In [64]:
expr = Less(Add(t, three), num(6))
display(expr)
expr.canonical_form()

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

In [66]:
expr = Less(Add(frac(t, two), three), num(5))
display(expr)
expr.canonical_form()

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


Make sure simple numeric cases work as a special case

In [68]:
Less(zero, num(5)).prove()

In [69]:
Less(two, num(10)).prove()

In [70]:
Less(four, one).disprove()

In [71]:
Less(Neg(two), four).prove()

In [72]:
Less(three, Neg(one)).disprove()

In [73]:
Less(frac(one, two), frac(two, three)).prove()

In [74]:
Less(frac(one, three), frac(one, two)).prove()

In [75]:
Less(frac(Neg(one), three), frac(one, two)).prove()

In [76]:
%end demonstrations