Theorems (or conjectures) for the theory of proveit.logic.sets.enumeration

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, Function, IndexedVar
from proveit import a, b, c, d, i, j, k, m, n, x, y, A, P, Q, Px, Qx
from proveit.logic import And, Boolean, TRUE, FALSE, Forall, Or
from proveit.logic import (Equals, Implies, NotEquals, InSet, NotInSet, ProperSubset,
                           Set, ProperSubset, SubsetEq)
from proveit.numbers import one
from proveit.core_expr_types import (a_1_to_i, a_1_to_m, a_1_to_n, b_1_to_j, b_1_to_n,
                                              c_1_to_j, c_1_to_k, c_1_to_n,
                                              d_1_to_k, Pk_a1_to_an, Qk_implies_Pk_a1_to_an, y_1_to_n)
from proveit.logic.sets import x_equals_any_y, x_notequals_all_y
from proveit.numbers import Natural
%begin theorems

Defining theorems for theory 'proveit.logic.sets.enumeration'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

unfold = Forall(n, Forall((x, y_1_to_n), 
                          x_equals_any_y, 
                          conditions=[InSet(x, Set(y_1_to_n))]),
                domain=Natural)

unfold (conjecture without proof):

fold = Forall(n, Forall((x, y_1_to_n), 
                        InSet(x, Set(y_1_to_n)), 
                        conditions=[x_equals_any_y]),
              domain=Natural)

fold (established theorem):

nonmembership_equiv = Forall(n, Forall((x, y_1_to_n), 
                                      Equals(NotInSet(x, Set(y_1_to_n)), 
                                             x_notequals_all_y)),
                           domain=Natural)

nonmembership_equiv (conjecture without proof):

nonmembership_unfold = Forall(
        n,
        Forall((x, y_1_to_n), 
               x_notequals_all_y,
               conditions=[NotInSet(x, Set(y_1_to_n))]),
        domain=Natural)

nonmembership_unfold (conjecture without proof):

nonmembership_fold = Forall(
        n,
        Forall((x, y_1_to_n), 
               NotInSet(x, Set(y_1_to_n)), 
               conditions=[x_notequals_all_y]),
        domain=Natural)

nonmembership_fold (conjecture without proof):

singleton_def = Forall((x, y), Equals(InSet(x, Set(y)), Equals(x, y)))

singleton_def (conjecture with conjecture-based proof):

unfold_singleton = Forall((x, y), Equals(x, y), conditions=[InSet(x, Set(y))])

unfold_singleton (conjecture without proof):

fold_singleton = Forall((x, y), InSet(x, Set(y)), conditions=[Equals(x, y)])

fold_singleton (conjecture without proof):

nonmembership_unfold_singleton = Forall(
        (x, y),
        NotEquals(x, y),
        conditions = [NotInSet(x, Set(y))])

nonmembership_unfold_singleton (conjecture without proof):

nonmembership_fold_singleton = Forall(
        (x, y),
        NotInSet(x, Set(y)),
        conditions = [NotEquals(x, y)])

nonmembership_fold_singleton (conjecture without proof):

not_in_singleton_equiv = Forall((x, y), Equals(NotInSet(x, Set(y)), NotEquals(x, y)))

not_in_singleton_equiv (conjecture without proof):

in_enumerated_set = Forall(
        (m, n),
        Forall( (a_1_to_m, b, c_1_to_n),
                InSet(b, Set(a_1_to_m, b, c_1_to_n))),
        domain=Natural)

in_enumerated_set (conjecture without proof):

in_singleton_is_bool = Forall((x, y), InSet(InSet(x, Set(y)), Boolean))

in_singleton_is_bool (conjecture with conjecture-based proof):

not_in_singleton_is_bool = Forall((x, y), InSet(NotInSet(x, Set(y)), Boolean))

not_in_singleton_is_bool (conjecture without proof):

in_enum_set_is_bool = Forall(
        n,
        Forall((x, y_1_to_n), 
               InSet(InSet(x, Set(y_1_to_n)), Boolean)),
        domain=Natural)

in_enum_set_is_bool (conjecture without proof):

not_in_enum_set_is_bool = Forall(
        n,
        Forall((x, y_1_to_n), 
               InSet(NotInSet(x, Set(y_1_to_n)), Boolean)),
        domain=Natural)

not_in_enum_set_is_bool (conjecture without proof):

in_singleton_eval_true = Forall(
    (x, y),
    Equals(InSet(x, Set(y)), TRUE),
    conditions=[Equals(x, y)])

in_singleton_eval_true (conjecture with conjecture-based proof):

in_singleton_eval_false = Forall(
    (x, y),
    Equals(InSet(x, Set(y)), FALSE),
    conditions=[NotEquals(x, y)])

in_singleton_eval_false (conjecture with conjecture-based proof):

Theorems related to permutations of enumerated sets

For example, the set {1, 2, 3} should be equivalent to the set {3, 2, 1}.
Here we adopt some of the terminology used in analogous theorems for disjunctions and conjunctions.
These theorems are generally not expected to be used directly but instead are intended to be implemented via Set methods such as permutation_simple() and permutation_general().

For these permutation thms, we can use equals (=) instead of equivalence, because permutations of an enumerated Set are all actually the same set (even if expressed so they look like multisets). Thus {a, b} = {b, a}, of course, but we also have {a, b} = {a, b, a, b}.

binary_permutation = Forall((a, b), Equals(Set(a, b), Set(b, a)))

binary_permutation (conjecture without proof):

leftward_permutation = Forall(
    (i, j, k),
    Forall((a_1_to_i, b_1_to_j, c, d_1_to_k),
           Equals(Set(a_1_to_i, b_1_to_j, c, d_1_to_k),
                  Set(a_1_to_i, c, b_1_to_j, d_1_to_k))),
    domain = Natural)

leftward_permutation (conjecture without proof):

rightward_permutation = Forall(
    (i, j, k),
    Forall((a_1_to_i, b, c_1_to_j, d_1_to_k),
           Equals(Set(a_1_to_i, b, c_1_to_j, d_1_to_k),
                  Set(a_1_to_i, c_1_to_j, b, d_1_to_k))),
    domain = Natural)

rightward_permutation (conjecture without proof):

Theorems related to reductions of enumerated sets

For example, the set {1, 2, 3, 3} should be equal to the “reduced” version {1, 2, 3}, and more generally, any enumerated set written with multiplicities should be reduceable to a set where any or all of the multiplicites are reduced to single occurences.

reduction_right = Forall(
    (i, j, k),
    Forall((a_1_to_i, x, b_1_to_j, c_1_to_k),
           Equals(Set(a_1_to_i, x, b_1_to_j, x, c_1_to_k),
                  Set(a_1_to_i, x, b_1_to_j, c_1_to_k)).with_wrap_after_operator()),
    
    domain = Natural)

reduction_right (conjecture without proof):

reduction_left = Forall(
    (i, j, k),
    Forall((a_1_to_i, x, b_1_to_j, c_1_to_k),
           Equals(Set(a_1_to_i, x, b_1_to_j, x, c_1_to_k),
                  Set(a_1_to_i, b_1_to_j, x, c_1_to_k)).with_wrap_after_operator()),
    
    domain = Natural)

reduction_left (conjecture without proof):

Theorems related to equality of enumerated sets

For example, an enumerated set such as $\{a, b, c\}$ should be equal to the enumerated set $\{a, d, c\}$ when $b=d$.

equal_element_equality = Forall(
        (m, n),
        Forall((a_1_to_m, b, c_1_to_n, d),
               Equals(Set(a_1_to_m, b, c_1_to_n), Set(a_1_to_m, d, c_1_to_n)).with_wrap_after_operator(),
               conditions=[Equals(b, d)]),
        domain = Natural)

equal_element_equality (conjecture without proof):

Theorems related to containment

For example, any enumerated set is an improper subset of itself, and the enumerated set {1, 2, 3} is clearly a proper subset of {1, 2, 3, 4}. The SubsetEq version is easier to express than the proper subset version.

subset_eq_of_superset = Forall(
        (m, n),
        Forall((a_1_to_m, b_1_to_n),
               SubsetEq(Set(a_1_to_m), Set(a_1_to_m, b_1_to_n))),
        domain = Natural)

subset_eq_of_superset (conjecture without proof):

proper_subset_of_superset = Forall(
        (m, n),
        Forall((a_1_to_m, b, c_1_to_n),
               ProperSubset(Set(a_1_to_m), Set(a_1_to_m, b, c_1_to_n)),
               conditions=[NotInSet(b, Set(a_1_to_m))]),
        domain = Natural)

proper_subset_of_superset (conjecture without proof):

Theorems related to propositions over sets

A proposition that is true for each element of a set is true for all elements in the set, and vice versa. For example, if $P(i)=\text{TRUE}$ for $i\in S=\{1, 2, 3\}$, then we have $\forall_{i\in S} P(i)$. On the other hand, if we know $\forall_{i\in S} P(i)$, then we know $P(1)\land P(2)\land P(3)$.

true_for_each_is_true_for_all = Forall(
        n,
        Forall(
            a_1_to_n,
            Forall(
                P,
                Equals(And(Pk_a1_to_an), Forall(x, Px, domain=Set(a_1_to_n))))),
        domain = Natural)

true_for_each_is_true_for_all (conjecture without proof):

true_for_each_then_true_for_all = Forall(
        n,
        Forall(
            a_1_to_n,
            Forall(
                P,
                Forall(x, Px, domain=Set(a_1_to_n)),
                condition=Pk_a1_to_an)),
        domain = Natural)

true_for_each_then_true_for_all (conjecture without proof):

true_for_all_then_true_for_each = Forall(
        n,
        Forall(
            a_1_to_n,
            Forall(
                P,
                And(Pk_a1_to_an),
                condition=Forall(x, Px, domain=Set(a_1_to_n)))),
        domain = Natural)

true_for_all_then_true_for_each (conjecture without proof):

true_for_each_then_true_for_all_conditioned = Forall(
        n,
        Forall(
            a_1_to_n,
            Forall(
                (P, Q),
                Forall(x, Px, domain=Set(a_1_to_n), condition=Qx),
                condition=Qk_implies_Pk_a1_to_an)),
        domain = Natural)

true_for_each_then_true_for_all_conditioned (conjecture without proof):

For the claim $\forall_{i\in S} P(i)$ to be false, we need only have a single $P(i)$ to be false.

Pk_a1_to_an_false = ExprRange(k, Equals(Function(P, IndexedVar(a, k)), FALSE), one, n)
false_for_one_is_false_for_all = Forall(
        n,
        Forall(
            a_1_to_n,
            Forall(
                P,
                Equals(Or(Pk_a1_to_an_false), Equals(Forall(x, Px, domain=Set(a_1_to_n)), FALSE)))),
        domain = Natural)

false_for_one_is_false_for_all (conjecture without proof):

%end theorems

These theorems may now be imported from the theory package: proveit.logic.sets.enumeration