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

import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import ExprRange, IndexedVar
from proveit.logic import Forall, Equals, NotEquals, InSet
from proveit.numbers import (zero, one, Natural, NaturalPos, Complex, 
                             Add, Neg, subtract, Less, LessEq, greater, greater_eq,
                             Exp)
from proveit import a, b, c, d, i, j, k
from proveit.core_expr_types import a_1_to_i, b_1_to_j, c_1_to_j, c_1_to_k, d_1_to_k, e_1_to_k

%begin theorems

Defining theorems for theory 'proveit.numbers.addition.subtraction'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

subtract_from_add = Forall((a, b, c), Equals(subtract(c, b), a), conditions=[Equals(Add(a, b), c)], domain=Complex)

subtract_from_add (conjecture without proof):

negated_add = Forall((a, b, c), Equals(Add(Neg(a), Neg(b)), Neg(c)), conditions=[Equals(Add(a, b), c)], domain=Complex)

negated_add (conjecture without proof):

subtract_from_add_reversed = Forall((a, b, c), Equals(subtract(b, c), Neg(a)), conditions=[Equals(Add(a, b), c)], domain=Complex)

subtract_from_add_reversed (conjecture without proof):

add_from_subtract = Forall((a, b, c), Equals(Add(c, b), a), conditions=[Equals(subtract(a, b), c)], domain=Complex)

add_from_subtract (conjecture without proof):

add_cancel_basic = Forall((a, b), Equals(subtract(a, b), zero), domain=Complex,
                         condition=Equals(a, b))

add_cancel_basic (conjecture without proof):

add_cancel_reverse = Forall((a, b), Equals(Add(Neg(a), b), zero), domain=Complex,
                            condition=Equals(a, b))

add_cancel_reverse (conjecture without proof):

add_cancel_triple_12 = Forall((a, b, c), Equals(Add(a, Neg(b), c), c), domain=Complex,
                              condition=Equals(a, b))

add_cancel_triple_12 (conjecture without proof):

add_cancel_triple_21 = Forall((a, b, c), Equals(Add(Neg(a), b, c), c), domain=Complex,
                              condition=Equals(a, b))

add_cancel_triple_21 (conjecture without proof):

add_cancel_triple_13 = Forall((a, b, c), Equals(Add(a, c, Neg(b)), c), domain=Complex,
                              condition=Equals(a, b))

add_cancel_triple_13 (conjecture without proof):

add_cancel_triple_31 = Forall((a, b, c), Equals(Add(Neg(a), c, b), c), domain=Complex,
                              condition=Equals(a, b))

add_cancel_triple_31 (conjecture without proof):

add_cancel_triple_23 = Forall((a, b, c), Equals(Add(c, a, Neg(b)), c), domain=Complex,
                              condition=Equals(a, b))

add_cancel_triple_23 (conjecture without proof):

add_cancel_triple_32 = Forall((a, b, c), Equals(Add(c, Neg(a), b), c), domain=Complex,
                              condition=Equals(a, b))

add_cancel_triple_32 (conjecture without proof):

pos_difference = Forall((a, b), greater(subtract(a, b), zero), condition=greater(a, b))

pos_difference (conjecture without proof):

nonneg_difference = Forall((a, b), greater_eq(subtract(a, b), zero), 
                           condition=greater_eq(a, b))

nonneg_difference (conjecture without proof):

neg_difference = Forall((a, b), Less(subtract(a, b), zero), condition=Less(a, b))

neg_difference (conjecture without proof):

nonpos_difference = Forall((a, b), LessEq(subtract(a, b), zero), 
                           condition=LessEq(a, b))

nonpos_difference (conjecture without proof):

nonzero_difference_if_different = Forall((a, b), NotEquals(subtract(a, b), zero), condition=NotEquals(a, b))

nonzero_difference_if_different (conjecture without proof):

subtract_nat_closure_bin = Forall((a, b), InSet(subtract(a, b), Natural), domain=Natural,
                               conditions=[LessEq(b, a)])

subtract_nat_closure_bin (conjecture without proof):

sub_one_is_nat = Forall(a, InSet(subtract(a, one), Natural), domain=NaturalPos)

sub_one_is_nat (conjecture without proof):

Need to deal with cancelation in 3 operand cases in which only a single term remains.

add_cancel_general = Forall((i,j,k), 
                          Forall((a_1_to_i,b,c_1_to_j,d,e_1_to_k), 
                                 Equals(Add(a_1_to_i, b, c_1_to_j, Neg(d), e_1_to_k),
                                        Add(a_1_to_i, c_1_to_j, e_1_to_k)),
                                 domain=Complex, condition=Equals(b, d)), 
                          domain=Natural)

add_cancel_general (conjecture without proof):

add_cancel_general_rev = Forall((i,j,k), 
                             Forall((a_1_to_i,b,c_1_to_j,d,e_1_to_k), 
                                    Equals(Add(a_1_to_i, Neg(b), c_1_to_j, d, e_1_to_k), 
                                           Add(a_1_to_i, c_1_to_j, e_1_to_k)),
                                    domain=Complex), 
                             domain=Natural)

add_cancel_general_rev (conjecture without proof):

subtraction_disassociation = \
    Forall((i,j,k), 
           Forall((a_1_to_i,b_1_to_j,c_1_to_k), 
                  Equals(Add(a_1_to_i, Neg(Add(b_1_to_j)), c_1_to_k),
                         Add(a_1_to_i, ExprRange(a, Neg(IndexedVar(b, a)), one, j), c_1_to_k)) \
                  .with_wrapping_at(2),
                  domain=Complex),
           domain=Natural)

subtraction_disassociation (conjecture without proof):

%end theorems

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