# Proof of proveit.logic.sets.enumeration.in_enumerated_set theorem¶

In [1]:
import proveit
from proveit import ExprRange, ExprTuple, Function, IndexedVar
from proveit import a, b, c, k, m, n, x, y, A, B, C
from proveit.logic import Equals, InSet, Or, Boolean
from proveit.logic.booleans.disjunction import or_if_any
from proveit.logic.sets.enumeration  import enum_set_def
from proveit.logic.sets.enumeration import fold
from proveit.numbers import zero, one, two, three, Neg, Complex, Natural, NaturalPos
from proveit.core_expr_types import a_1_to_m, c_1_to_n, x_1_to_n, y_1_to_n
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving in_enumerated_set

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
in_enumerated_set:
(see dependencies)
in_enumerated_set may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

In [3]:
enum_set_def

In [4]:
enum_set_def_with_k = enum_set_def.instantiate({n:k}, assumptions=[InSet(k, Natural)], num_forall_eliminations=0,
auto_simplify=False)

enum_set_def_with_k:
In [5]:
# this also works, first instantiating, then generalizing over the new var
# enum_set_def_inst_n_to_k = enum_set_def.instantiate({n:k}, assumptions=[InSet(k, Natural)])
# enum_set_def_with_k = enum_set_def_inst_n_to_k.generalize([[k]], [[Natural]])

In [6]:
enum_set_def_with_k_inst = enum_set_def_with_k.instantiate(
{k:k, x:b, y:ExprTuple(a_1_to_m, b, c_1_to_n)},
assumptions=[InSet(k, Natural), InSet(m, Natural), InSet(n, Natural), InSet(Add(subtract(m, one), one), Natural), Equals(Add(m, one, n), k)],
auto_simplify=False)

enum_set_def_with_k_inst: , , ,  ⊢
In [7]:
enum_set_def_with_k_inst.expr.rhs

In [8]:
or_if_any

In [9]:
A_sub, C_sub = (
ExprRange(k, Equals(b, IndexedVar(a, k)), one, m),
ExprRange(k, Equals(b, IndexedVar(c, k)), one, n))

A_sub:
C_sub:
In [10]:
A_in_Bool_assumptions, C_in_Bool_assumptions = (
ExprRange(k, InSet(Equals(b, IndexedVar(a, k)), Boolean), one, m),
ExprRange(k, InSet(Equals(b, IndexedVar(c, k)), Boolean), one, n))

A_in_Bool_assumptions:
C_in_Bool_assumptions:
In [11]:
or_if_any_inst = or_if_any.instantiate(
{m:m, n:n, A:A_sub, B:Equals(b,b), C:C_sub},
assumptions=[InSet(m, Natural), InSet(n, Natural),
A_in_Bool_assumptions, C_in_Bool_assumptions])

or_if_any_inst: , , ,  ⊢
In [12]:
the_or_expr = Or(Equals(b, b),
ExprRange(
k,
Equals(b, IndexedVar(a, k)),
one, m))

the_or_expr:
In [13]:
another_or_expr = Or(Equals(b, a), Equals(b, b), Equals(b, c))

another_or_expr:
In [14]:
another_or_expr.associate(1, 2)

In [15]:
the_operands = the_or_expr.operands

the_operands:
In [16]:
or_if_any

In [17]:
A_sub, C_sub = (
ExprRange(k, Equals(b, IndexedVar(a, k)), one, m),
ExprRange(k, Equals(b, IndexedVar(c, k)), one, n))

A_sub:
C_sub:
In [18]:
A_in_Bool_assumptions, B_in_Bool_assumptions = (
ExprRange(k, InSet(Equals(b, IndexedVar(a, k)), Boolean), one, m),
ExprRange(k, InSet(Equals(b, IndexedVar(c, k)), Boolean), one, n))

A_in_Bool_assumptions:
B_in_Bool_assumptions:
In [19]:
# why are the equalities having to be ASSUMED to be in Boolean?
Equals(b, IndexedVar(a, one)).deduce_in_bool()

In [20]:
or_if_any_inst = or_if_any.instantiate(
{m:m, n:n, A:A_sub, B:Equals(b,b), C:C_sub},
assumptions=[InSet(m, Natural), InSet(n, Natural), A_in_Bool_assumptions, B_in_Bool_assumptions])

or_if_any_inst: , , ,  ⊢
In [21]:
A_in_Bool_assumptions = ExprRange(k, InSet(Equals(b, IndexedVar(a, k)), Boolean), one, m)

A_in_Bool_assumptions:
In [22]:
# Or(Equals(b, b),
#    ExprRange(
#        k,
#        Equals(b, IndexedVar(a, k)),
#        one, m)).conclude_via_example(Equals(b, b),
#                 assumptions=[ExprRange(k, InSet(Equals(b, IndexedVar(a, k)), Boolean), one, m)])

In [23]:
# Example to help construct a multi-Or of equalities
# Or(ExprRange(k, Equals(IndexedVar(x, k), Function(f, Add(i, k))),
#               zero, subtract(j, i)))

In [24]:
# Or(ExprRange(
#        k,
#        Equals(b, IndexedVar(a, k)),
#        one, m),
#    Equals(b, b),
#    ExprRange(
#        k,
#        Equals(b, IndexedVar(c, k)),
#        one, n)).prove()

In [25]:
enum_set_def_inst = enum_set_def.instantiate(
{n:n, x:b}, assumptions=[InSet(n, Natural)])

enum_set_def_inst:
In [26]:
fold