logo

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 Add, subtract
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
 ⊢