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

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 ExprTuple, IndexedVar
from proveit.logic import Forall, Not, Equals, InSet, NotInSet, EmptySet, in_bool
from proveit import i, m, n, x, S
from proveit.numbers import zero, num, Natural, Exp, Interval
%begin theorems

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

exp_set_0 = Forall(S, InSet(ExprTuple(), Exp(S, zero)))def nvars(n): return [proveit._common_.__getattr__(chr(ord('a')+k)) for k in range(n)] exp_set_1, exp_set_2, exp_set_3, exp_set_4, exp_set_5, exp_set_6, exp_set_7, exp_set_8, exp_set_9 = \ [Forall(S, Forall(nvars(n), InSet(ExprTuple(*nvars(n)), Exp(S, num(n))), domain=S)) for n in range(1, 10)]mem_exp_set_length = Forall( m, Forall(S, Forall(x, Equals(Len(x), m), domain = Exp(S, m))), domain = Natural)mem_exp_set_item_set = Forall( m, Forall(S, Forall(x, Forall(i, InSet(IndexedVar(x,i),S), domain = Interval(num(1),m)), domain = Exp(S, m))), domain = Natural)

# Proven. Used by the NotInSet class's deduce_in_bool() method
not_in_set_is_bool = Forall( (x, S), in_bool(NotInSet(x, S)), conditions=[in_bool(InSet(x, S))] )

not_in_set_is_bool (conjecture with conjecture-based proof):

unfold_not_in_set = Forall((x, S), Not(InSet(x, S)), conditions=[NotInSet(x, S)])

unfold_not_in_set (established theorem):

fold_not_in_set = Forall((x, S), NotInSet(x, S), conditions=[Not(InSet(x, S))])

fold_not_in_set (established theorem):

double_negated_membership = Forall((x, S), Not(NotInSet(x, S)), conditions=[InSet(x, S)])

double_negated_membership (conjecture without proof):

Might be useful to have an additional theorem here along the lines of: $(x\in S \Rightarrow \bot) \Rightarrow (x\notin S)$ (a form of “deny_via_contradiction” or some similar name)

%end theorems

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