logo

Demonstrations for the theory of proveit.logic.booleans.conjunction

In [1]:
from proveit import ExprTuple
from proveit import a, b, c, d, e, f, A,B,C,D,E,F,G,H, i, j, k, l, m,n
from proveit.core_expr_types import A_1_to_m, B_1_to_n,C_1_to_n
from proveit.logic import And, Or, Not, TRUE, FALSE, Equals, in_bool, Boolean
from proveit.numbers import zero, one, two, three,five,Add, Exp, subtract
%begin demonstrations
In [2]:
#And(A,B,C,D,E,F).derive_some_from_and(3, assumptions=[And(A,B,C,var_iter(D, one, one),E,F)])
In [3]:
#And(var_iter(A, one, five), var_iter(B, one, two), var_iter(C, one, three)).derive_some_from_and(1)
In [4]:
#And(A_1_to_m, B_1_to_n, C_1_to_n).derive_some_from_and(1)
In [5]:
Equals(Add(zero, Add(subtract(m, one), one)), Add(subtract(m, one), one))
Out[5]:
In [6]:
#Equals(Add(zero, Add(subtract(m, one), one)), Add(subtract(m, one), one)).prove()
In [7]:
expr = And(a, b, c, d, e, f)
Out[7]:
expr:
In [8]:
expr.copy().with_wrapping_at(3)
Out[8]:
In [9]:
new_expr = expr.copy().with_wrapping_at(3)
Out[9]:
new_expr:
In [10]:
expr
Out[10]:
In [11]:
new_expr
Out[11]:
In [12]:
expr = And(Or(a, b, c), Or(b, c, d), Or(d, e, f))
Out[12]:
expr:
In [13]:
new_expr = expr.copy()
Out[13]:
new_expr:
In [14]:
new_expr.inner_expr().operands[1].with_wrapping_at(3)
Out[14]:
In [15]:
expr
Out[15]:
In [16]:
print(expr==new_expr)
True
In [17]:
And(TRUE, TRUE).evaluation()
Out[17]:
In [18]:
And(TRUE, TRUE, TRUE).evaluation()
Out[18]:
In [19]:
Not(FALSE).prove()
Out[19]:
In [20]:
And(TRUE, Not(FALSE), TRUE).evaluation()
Out[20]:
In [21]:
And(TRUE, Not(FALSE), TRUE).prove()
Out[21]:
In [22]:
And(TRUE, Not(FALSE), TRUE).evaluation()
Out[22]:
In [23]:
And(TRUE, Or(TRUE, FALSE)).evaluation()
Out[23]:
In [24]:
And(TRUE, Or(TRUE, FALSE), FALSE).evaluation()
Out[24]:
In [ ]:
 
In [ ]:
 
In [25]:
And(TRUE, TRUE).prove()
Out[25]:
In [26]:
Not(And(TRUE, FALSE)).prove()
Out[26]:
In [27]:
Not(And(FALSE,TRUE)).prove()
Out[27]:
In [28]:
Not(And(FALSE,FALSE)).prove()
Out[28]:
In [29]:
And(A,B).prove([A,B])
Out[29]:
In [30]:
Not(And(A,B)).prove([in_bool(A), in_bool(B), Not(B)])
Out[30]:
, ,  ⊢  
In [31]:
Not(And(A,B)).prove([in_bool(A), in_bool(B), Not(A)])
Out[31]:
, ,  ⊢  
In [32]:
Not(And(A,B,C)).prove([Not(B)])
Out[32]:
In [33]:
And(A,B).derive_any(0,[And(A,B), *in_bool(A,B)])
Out[33]:
In [34]:
And(A,B).derive_any(1,[And(A,B), *in_bool(A,B)])
Out[34]:
In [35]:
And(A,B).commutation(assumptions=in_bool(A, B))
Out[35]:
In [36]:
And(A,B).commute(assumptions=[And(A, B)])
Out[36]:
In [37]:
in_bool(D).prove([in_bool(And(A,B,C,D))])
Out[37]:
In [38]:
from  proveit.logic.booleans.conjunction import each_is_bool
expr = each_is_bool.instance_expr.explicit_conditions()[0].element
Out[38]:
expr:
In [39]:
from proveit.logic import InSet
from proveit.numbers import Natural
expr.derive_any(1, assumptions=[InSet(m, Natural), InSet(n, Natural), expr])
Out[39]:
, ,  ⊢  
In [40]:
expr.derive_some(0, assumptions=[InSet(m, Natural), InSet(n, Natural), expr])
Out[40]:
, ,  ⊢  
In [41]:
expr.derive_some(2, assumptions=[InSet(m, Natural), InSet(n, Natural), expr])
Out[41]:
, ,  ⊢  
In [42]:
from  proveit.logic.booleans.conjunction import any_from_and
any_from_and
Out[42]:
In [ ]:
 
In [43]:
And(A,B,C).prove([A,C,B])
Out[43]:
, ,  ⊢  
In [44]:
And(A,B,C,D,E,F,G).associate(2,length=2,assumptions=[And(A,B,And(C,D),E,F,G),And(A,B,C,D,E,F,G),in_bool(A), in_bool(B),in_bool(C),in_bool(D),in_bool(E),in_bool(F),in_bool(G)])
Out[44]:
In [45]:
And(A,B,C,D,E).commute(1,3,[And(A,B,C,D,E), *in_bool(A,B,C,D,E)])
Out[45]:
In [46]:
And(A,B,C,D,E).group_commute(0,1,length=3, assumptions=[And(A,B,C,D,E), *in_bool(A,B,C,D,E)])
Out[46]:
In [47]:
expr = Or(A, B, And(C, D, E))
Out[47]:
expr:
In [48]:
expr.inner_expr().operands[-1].commutation(0, -1, assumptions=in_bool(C, D, E))
Out[48]:
, ,  ⊢  
In [49]:
kt = expr.inner_expr().operands[-1].associate(0, length=2, assumptions=[expr])
Out[49]:
kt:  ⊢  
In [50]:
expr = kt.expr
Out[50]:
expr:
In [51]:
expr = expr.inner_expr().operands[-1].disassociate(0, assumptions=[expr])
Out[51]:
expr:  ⊢  
In [52]:
in_bool(And(A,B)).prove([in_bool(A), in_bool(B)])
Out[52]:
In [53]:
in_bool(And(A,B,C,D)).prove([in_bool(A), in_bool(B), in_bool(C), in_bool(D)])
Out[53]:
, , ,  ⊢  
In [54]:
And(A,B).prove([Not(Or(Not(A), Not(B)))])
Out[54]:
In [55]:
And(A,B,C).prove([Not(Or(Not(A), Not(B), Not(C)))])
Out[55]:

Axioms

In [56]:
Equals(And(TRUE, TRUE), TRUE).prove()
Out[56]:
In [57]:
Equals(And(TRUE, FALSE), FALSE).prove()
Out[57]:
In [58]:
Equals(And(FALSE, TRUE), FALSE).prove()
Out[58]:
In [59]:
Equals(And(FALSE, FALSE), FALSE).prove()
Out[59]:
In [60]:
in_bool(A).prove([in_bool(And(A,B))])
Out[60]:
In [61]:
in_bool(B).prove([in_bool(And(A,B))])
Out[61]:
In [62]:
Equals(And(FALSE, TRUE), FALSE).prove()
Out[62]:
In [63]:
Equals(And(FALSE, FALSE), FALSE).prove()
Out[63]:
In [64]:
in_bool(A).prove([in_bool(And(A,B))])
Out[64]:
In [65]:
in_bool(B).prove([in_bool(And(A,B))])
Out[65]:
In [66]:
%end demonstrations