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

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,
        Rational,
        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

less_than_is_bool = Forall((x, y), InSet(Less(x, y), Boolean), domain=Real)

less_than_is_bool (conjecture without proof):

less_than_equals_is_bool = Forall((x, y), InSet(LessEq(x, y), Boolean), domain=Real)

less_than_equals_is_bool (conjecture without proof):

relax_less = Forall((x, y), LessEq(x, y), conditions=[Less(x, y)])

relax_less (conjecture without proof):

relax_equal_to_less_eq = Forall(
    (x, y),
    LessEq(x, y),
    domain=Real,
    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.

# 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):

# 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):

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):

symmetric_less_eq = Forall((x,y), Equals(x, y), conditions=[LessEq(x,y), LessEq(y, x)])

symmetric_less_eq (conjecture without proof):

positive_if_real_pos = Forall(a, greater(a, zero), domain=RealPos)

positive_if_real_pos (conjecture without proof):

negative_if_real_neg = Forall(a, Less(a, zero), domain=RealNeg)

negative_if_real_neg (conjecture without proof):

non_neg_if_real_non_neg = Forall(a, greater_eq(a, zero), domain=RealNonNeg)

non_neg_if_real_non_neg (conjecture without proof):

non_pos_if_real_non_pos = Forall(a, LessEq(a, zero), domain=RealNonPos)

non_pos_if_real_non_pos (conjecture without proof):

less_than_successor = Forall(a, Less(a, Add(a, one)), domain=Real)

less_than_successor (conjecture without proof):

less_than_left_successor = Forall(a, Less(a, Add(one, a)), domain=Real)

less_than_left_successor (conjecture without proof):

less_than_an_increase = Forall((a, b), Less(a, Add(a, b)), 
                            domains=(Real, RealPos))

less_than_an_increase (conjecture without proof):

less_than_an_left_increase = Forall((a, b), Less(a, Add(b, a)), 
                                    domains=(Real, RealPos))

less_than_an_left_increase (conjecture without proof):

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):

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):

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):

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):

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):

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):

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):

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):

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):

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):

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):

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):

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):

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):

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):

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):

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):

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):

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):

less_is_not_eq = Forall([a, b], NotEquals(a, b), domain=Real, conditions=[Less(a, b)])

less_is_not_eq (conjecture without proof):

min_real_closure = Forall(n, Forall(a_1_to_n, InSet(Min(a_1_to_n), Real), 
                                    domain=Real),
                          domain=Natural)

min_real_closure (conjecture without proof):

max_real_closure = Forall(n, Forall(a_1_to_n, InSet(Max(a_1_to_n), Real), 
                                    domain=Real),
                          domain=Natural)

max_real_closure (conjecture without proof):

min_set_closure = (
    Forall(S,
    Forall(n,
    Forall(a_1_to_n,
           InSet(Min(a_1_to_n), S), 
           domain=S),
    domain=Natural),
    condition=SubsetEq(S, Real)))

min_set_closure (conjecture without proof):

max_set_closure = (
    Forall(S,
    Forall(n,
    Forall(a_1_to_n,
           InSet(Max(a_1_to_n), S), 
           domain=S),
    domain=NaturalPos),
    condition=SubsetEq(S, Real)))

max_set_closure (conjecture without proof):

not_equals_is_less_than_or_greater_than = (
    Forall((a, x),
           Or(Less(x, a), greater(x, a)),
           domain=Real,
           conditions=[NotEquals(x, a)]))

not_equals_is_less_than_or_greater_than (conjecture without proof):

less_complement_is_greater_eq = (
    Forall((x, y), Equals(Not(Less(x, y)), LessEq(y, x)),
           domain=Real))

less_complement_is_greater_eq (conjecture without proof):

less_eq_complement_is_greater = (
    Forall((x, y), Equals(Not(LessEq(x, y)), Less(y, x)),
           domain=Real))

less_eq_complement_is_greater (conjecture without proof):

less_from_not_less_eq = (
    Forall((x, y),
       Less(y, x),
       domain=Real,
       condition=Not(LessEq(x, y))))

less_from_not_less_eq (conjecture without proof):

less_eq_from_not_less = (
    Forall((x, y),
       LessEq(y, x),
       domain=Real,
       condition=Not(Less(x, y))))

less_eq_from_not_less (conjecture without proof):

not_less_from_less_eq = (
    Forall((x, y),
       Not(Less(y, x)),
       domain=Real,
       condition=LessEq(x, y)))

not_less_from_less_eq (conjecture without proof):

not_less_eq_from_less = (
    Forall((x, y),
       Not(LessEq(y, x)),
       domain=Real,
       condition=Less(x, y)))

not_less_eq_from_less (conjecture without proof):

less_or_greater_eq = Forall((x, y), Or(Less(x, y), greater_eq(x, y)),
                            domain=Real)

less_or_greater_eq (conjecture without proof):

less_eq_or_greater = Forall((x, y), Or(LessEq(x, y), greater(x, y)),
                            domain=Real)

less_eq_or_greater (conjecture without proof):

Misc Additional Min/Max Theorems

max_x_x_is_x = (
    Forall(x,
           Equals(Max(x, x), x),
           domain=Real))

max_x_x_is_x (conjecture with conjecture-based proof):

min_x_x_is_x = (
    Forall(x,
           Equals(Min(x, x), x),
           domain=Real))

min_x_x_is_x (conjecture with conjecture-based proof):

max_nat_n_zero_is_n = (
    Forall(n,
           Equals(Max(n, zero), n),
           domain=Natural))

max_nat_n_zero_is_n (conjecture with conjecture-based proof):

min_nat_n_zero_is_zero = (
    Forall(n,
           Equals(Min(n, zero), zero),
           domain=Natural))

min_nat_n_zero_is_zero (conjecture with conjecture-based proof):

max_bin_args_commute = (
    Forall((x, y),
           Equals(Max(x, y), Max(y, x)),
           domain=Real))

max_bin_args_commute (conjecture with conjecture-based proof):

min_bin_args_commute = (
    Forall((x, y),
           Equals(Min(x, y), Min(y, x)),
           domain=Real))

min_bin_args_commute (conjecture with conjecture-based proof):

max_y_ge_x = (
    Forall((x, y),
           Equals(Max(x, y), y),
           domain=Real,
           condition=greater_eq(y, x)))

max_y_ge_x (conjecture with conjecture-based proof):

min_y_le_x = (
    Forall((x, y),
           Equals(Min(x, y), y),
           domain=Real,
           condition=LessEq(y, x)))

min_y_le_x (conjecture with conjecture-based proof):

%end theorems

These theorems may now be imported from the theory package: proveit.numbers.ordering