Theorems (or conjectures) for the theory of proveit.numbers.ordering

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit.logic import (Forall, Not, Or, Equals, NotEquals, Iff, Implies,
                           InSet, Boolean, SubsetEq)
from proveit.numbers import (
        Integer, IntegerNeg, IntegerNonZero, Natural, NaturalPos,
        Real, RealPos, RealNonNeg, RealNeg, RealNonPos, RealNonZero,
        Add, zero, one)
from proveit.numbers import Neg, Less, LessEq, greater, greater_eq, Min, Max
from proveit import a, b, c, d, n, x, y, z, S
from proveit.core_expr_types import a_1_to_n

%begin theorems
Defining theorems for theory 'proveit.numbers.ordering'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [2]:
less_than_is_bool = Forall((x, y), InSet(Less(x, y), Boolean), domain=Real)
less_than_is_bool (conjecture without proof):

In [3]:
less_than_equals_is_bool = Forall((x, y), InSet(LessEq(x, y), Boolean), domain=Real)
less_than_equals_is_bool (conjecture without proof):

In [4]:
relax_less = Forall((x, y), LessEq(x, y), conditions=[Less(x, y)])
relax_less (conjecture without proof):

In [5]:
relax_equal_to_less_eq = Forall(
    (x, y),
    LessEq(x, y),
    conditions=[Equals(x, y)])
relax_equal_to_less_eq (conjecture without proof):

Transitivity Theorems

Notice that transitivity_less_less is an axiom, not a theorem. The other transitivity theorems can be derived from that axiom.

In [6]:
# proven
transitivity_less_eq_less = Forall((x,y,z), Less(x, z), conditions=[LessEq(x,y), Less(y, z)])
transitivity_less_eq_less (conjecture with conjecture-based proof):

In [7]:
# proven
transitivity_less_less_eq = Forall((x,y,z), Less(x, z), conditions=[Less(x,y), LessEq(y, z)])
transitivity_less_less_eq (conjecture with conjecture-based proof):

In [8]:
transitivity_less_eq_less_eq = Forall((x,y,z), LessEq(x, z), conditions=[LessEq(x,y), LessEq(y, z)])
transitivity_less_eq_less_eq (conjecture with conjecture-based proof):

In [9]:
symmetric_less_eq = Forall((x,y), Equals(x, y), conditions=[LessEq(x,y), LessEq(y, x)])
symmetric_less_eq (conjecture without proof):

In [10]:
positive_if_real_pos = Forall(a, greater(a, zero), domain=RealPos)
positive_if_real_pos (conjecture without proof):

In [11]:
negative_if_real_neg = Forall(a, Less(a, zero), domain=RealNeg)
negative_if_real_neg (conjecture without proof):

In [12]:
non_neg_if_real_non_neg = Forall(a, greater_eq(a, zero), domain=RealNonNeg)
non_neg_if_real_non_neg (conjecture without proof):

In [13]:
non_pos_if_real_non_pos = Forall(a, LessEq(a, zero), domain=RealNonPos)
non_pos_if_real_non_pos (conjecture without proof):

In [14]:
less_than_successor = Forall(a, Less(a, Add(a, one)), domain=Real)
less_than_successor (conjecture without proof):

In [15]:
less_than_left_successor = Forall(a, Less(a, Add(one, a)), domain=Real)
less_than_left_successor (conjecture without proof):

In [16]:
less_than_an_increase = Forall((a, b), Less(a, Add(a, b)), 
                            domains=(Real, RealPos))
less_than_an_increase (conjecture without proof):

In [17]:
less_than_an_left_increase = Forall((a, b), Less(a, Add(b, a)), 
                                    domains=(Real, RealPos))
less_than_an_left_increase (conjecture without proof):

In [18]:
less_eq_shift_add_right = Forall([a, b, c], LessEq(Add(a, c), Add(b, c)), domain=Real, conditions=[LessEq(a, b)])
less_eq_shift_add_right (conjecture without proof):

In [19]:
less_eq_shift_add_left = Forall([a, b, c], LessEq(Add(c, a), Add(c, b)), domain=Real, conditions=[LessEq(a, b)])
less_eq_shift_add_left (conjecture without proof):

In [20]:
less_shift_add_right = Forall([a, b, c], Less(Add(a, c), Add(b, c)), domain=Real, conditions=[Less(a, b)])
less_shift_add_right (conjecture without proof):

In [21]:
less_shift_add_left = Forall([a, b, c], Less(Add(c, a), Add(c, b)), domain=Real, conditions=[Less(a, b)])
less_shift_add_left (conjecture without proof):

In [22]:
less_add_both = Forall([a, b, c, d], Less(Add(a, c), Add(b, d)), domain=Real, conditions=[Less(a, b), LessEq(c, d)])
less_add_both (conjecture without proof):

In [23]:
less_add_right = Forall([a, b, c], Less(a, Add(b, c)), domain=Real, conditions=[Less(a, b), LessEq(zero, c)])
less_add_right (conjecture without proof):

In [24]:
less_add_left = Forall([a, b, c], Less(Add(a, c), b), domain=Real, conditions=[Less(a, b), LessEq(c, zero)])
less_add_left (conjecture without proof):

In [25]:
less_add_right_weak = Forall([a, b, c], LessEq(a, Add(b, c)), domain=Real, conditions=[Less(a, b), LessEq(zero, c)])
less_add_right_weak (conjecture without proof):

In [26]:
less_add_left_weak = Forall([a, b, c], LessEq(Add(a, c), b), domain=Real, conditions=[Less(a, b), LessEq(c, zero)])
less_add_left_weak (conjecture without proof):

In [27]:
less_add_right_weak_int = Forall([a, b, c], LessEq(a, Add(b, c)), domain=Integer, 
                                 conditions=[Less(a, b), LessEq(Neg(one), c)])
less_add_right_weak_int (conjecture without proof):

In [28]:
less_add_left_weak_int = Forall([a, b, c], LessEq(Add(a, c), b), domain=Integer, 
                                conditions=[Less(a, b), LessEq(c, one)])
less_add_left_weak_int (conjecture without proof):

In [29]:
less_eq_add_both = Forall([a, b, c, d], LessEq(Add(a, c), Add(b, d)), domain=Real, conditions=[LessEq(a, b), LessEq(c, d)])
less_eq_add_both (conjecture without proof):

In [30]:
less_eq_add_right = Forall([a, b, c], LessEq(a, Add(b, c)), domain=Real, conditions=[LessEq(a, b), LessEq(zero, c)])
less_eq_add_right (conjecture without proof):

In [31]:
less_eq_add_left = Forall([a, b, c], LessEq(Add(a, b), c), domain=Real, conditions=[LessEq(a, b), LessEq(c, zero)])
less_eq_add_left (conjecture without proof):

In [32]:
less_eq_add_right_strong = Forall([a, b, c], Less(a, Add(b, c)), domain=Real, 
                                 conditions=[LessEq(a, b), Less(zero, c)])
less_eq_add_right_strong (conjecture without proof):

In [33]:
less_eq_add_left_strong = Forall([a, b, c], Less(Add(a, c), b), domain=Real, 
                                 conditions=[LessEq(a, b), Less(c, zero)])
less_eq_add_left_strong (conjecture without proof):

In [34]:
less_is_not_eq_nat = Forall([a, b], NotEquals(a, b), domain=Natural, conditions=[Less(a, b)])
less_is_not_eq_nat (conjecture without proof):

In [35]:
less_is_not_eq_int = Forall([a, b], NotEquals(a, b), domain=Integer, conditions=[Less(a, b)])
less_is_not_eq_int (conjecture without proof):

In [36]:
less_is_not_eq_rational = Forall([a, b], NotEquals(a, b), domain=Rational, conditions=[Less(a, b)])
less_is_not_eq_rational (conjecture without proof):

In [37]:
less_is_not_eq = Forall([a, b], NotEquals(a, b), domain=Real, conditions=[Less(a, b)])
less_is_not_eq (conjecture without proof):

In [38]:
min_real_closure = Forall(n, Forall(a_1_to_n, InSet(Min(a_1_to_n), Real), 
min_real_closure (conjecture without proof):

In [39]:
max_real_closure = Forall(n, Forall(a_1_to_n, InSet(Max(a_1_to_n), Real), 
max_real_closure (conjecture without proof):

In [40]:
min_set_closure = (
           InSet(Min(a_1_to_n), S), 
    condition=SubsetEq(S, Real)))
min_set_closure (conjecture without proof):

In [41]:
max_set_closure = (
           InSet(Max(a_1_to_n), S), 
    condition=SubsetEq(S, Real)))
max_set_closure (conjecture without proof):

In [42]:
not_equals_is_less_than_or_greater_than = (
    Forall((a, x),
           Or(Less(x, a), greater(x, a)),
           conditions=[NotEquals(x, a)]))
not_equals_is_less_than_or_greater_than (conjecture without proof):

In [43]:
less_complement_is_greater_eq = (
    Forall((x, y), Equals(Not(Less(x, y)), LessEq(y, x)),
less_complement_is_greater_eq (conjecture without proof):

In [44]:
less_eq_complement_is_greater = (
    Forall((x, y), Equals(Not(LessEq(x, y)), Less(y, x)),
less_eq_complement_is_greater (conjecture without proof):

In [45]:
less_from_not_less_eq = (
    Forall((x, y),
       Less(y, x),
       condition=Not(LessEq(x, y))))
less_from_not_less_eq (conjecture without proof):

In [46]:
less_eq_from_not_less = (
    Forall((x, y),
       LessEq(y, x),
       condition=Not(Less(x, y))))
less_eq_from_not_less (conjecture without proof):

In [47]:
not_less_from_less_eq = (
    Forall((x, y),
       Not(Less(y, x)),
       condition=LessEq(x, y)))
not_less_from_less_eq (conjecture without proof):

In [48]:
not_less_eq_from_less = (
    Forall((x, y),
       Not(LessEq(y, x)),
       condition=Less(x, y)))
not_less_eq_from_less (conjecture without proof):

In [49]:
less_or_greater_eq = Forall((x, y), Or(Less(x, y), greater_eq(x, y)),
less_or_greater_eq (conjecture without proof):

In [50]:
less_eq_or_greater = Forall((x, y), Or(LessEq(x, y), greater(x, y)),
less_eq_or_greater (conjecture without proof):

Misc Additional Min/Max Theorems

In [51]:
max_x_x_is_x = (
           Equals(Max(x, x), x),
max_x_x_is_x (conjecture with conjecture-based proof):

In [52]:
min_x_x_is_x = (
           Equals(Min(x, x), x),
min_x_x_is_x (conjecture with conjecture-based proof):

In [53]:
max_nat_n_zero_is_n = (
           Equals(Max(n, zero), n),
max_nat_n_zero_is_n (conjecture with conjecture-based proof):

In [54]:
min_nat_n_zero_is_zero = (
           Equals(Min(n, zero), zero),
min_nat_n_zero_is_zero (conjecture with conjecture-based proof):

In [55]:
max_bin_args_commute = (
    Forall((x, y),
           Equals(Max(x, y), Max(y, x)),
max_bin_args_commute (conjecture with conjecture-based proof):

In [56]:
min_bin_args_commute = (
    Forall((x, y),
           Equals(Min(x, y), Min(y, x)),
min_bin_args_commute (conjecture with conjecture-based proof):

In [57]:
max_y_ge_x = (
    Forall((x, y),
           Equals(Max(x, y), y),
           condition=greater_eq(y, x)))
max_y_ge_x (conjecture with conjecture-based proof):

In [58]:
min_y_le_x = (
    Forall((x, y),
           Equals(Min(x, y), y),
           condition=LessEq(y, x)))
min_y_le_x (conjecture with conjecture-based proof):

In [59]:
%end theorems
These theorems may now be imported from the theory package: proveit.numbers.ordering