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))
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)
expr: 
In [8]:
expr.copy().with_wrapping_at(3)
In [9]:
new_expr = expr.copy().with_wrapping_at(3)
new_expr: 
In [10]:
expr
In [11]:
new_expr
In [12]:
expr = And(Or(a, b, c), Or(b, c, d), Or(d, e, f))
expr: 
In [13]:
new_expr = expr.copy()
new_expr:
In [14]:
new_expr.inner_expr().operands[1].with_wrapping_at(3)
In [15]:
expr
In [16]:
print(expr==new_expr)
In [17]:
And(TRUE, TRUE).evaluation()
In [18]:
And(TRUE, TRUE, TRUE).evaluation()
In [19]:
Not(FALSE).prove()
In [20]:
And(TRUE, Not(FALSE), TRUE).evaluation()
In [21]:
And(TRUE, Not(FALSE), TRUE).prove()
In [22]:
And(TRUE, Not(FALSE), TRUE).evaluation()
In [23]:
Or(TRUE, FALSE).evaluation()
In [24]:
And(TRUE, Or(TRUE, FALSE)).evaluation()
In [25]:
And(TRUE, Or(TRUE, FALSE), FALSE).evaluation()
In [ ]:
In [ ]:
In [26]:
And(TRUE, TRUE).prove()
In [27]:
Not(And(TRUE, FALSE)).prove()
In [28]:
Not(And(FALSE,TRUE)).prove()
In [29]:
Not(And(FALSE,FALSE)).prove()
In [30]:
And(A,B).prove(assumptions=[A,B])
, 
⊢ 
In [31]:
Not(And(A,B)).prove(assumptions=[in_bool(A), in_bool(B), Not(B)])
, 
, 
⊢ 
In [32]:
Not(And(A,B)).prove(assumptions=[in_bool(A), in_bool(B), Not(A)])
, , 
⊢
In [33]:
Not(And(A,B,C)).prove(assumptions=[Not(B)])
In [34]:
And(A,B).derive_any(0, assumptions=[And(A,B), *in_bool(A,B)])
In [35]:
And(A,B).derive_any(1, assumptions=[And(A,B), *in_bool(A,B)])
In [36]:
And(A,B).commutation(assumptions=in_bool(A, B))
, ⊢ 
In [37]:
And(A,B).commute(assumptions=[And(A, B)])
In [38]:
in_bool(D).prove(assumptions=[in_bool(And(A,B,C,D))])
In [39]:
from proveit.logic.booleans.conjunction import each_is_bool
expr = each_is_bool.instance_expr.explicit_conditions()[0].element
expr: 
In [40]:
from proveit.logic import InSet
from proveit.numbers import Natural
expr.derive_any(1, assumptions=[InSet(m, Natural), InSet(n, Natural), expr])
, 
, ⊢
In [41]:
expr.derive_some(0, assumptions=[InSet(m, Natural), InSet(n, Natural), expr])
, , ⊢ 
In [42]:
and_C_1_to_n = expr.derive_some(2, assumptions=[InSet(m, Natural), InSet(n, Natural), expr])
and_C_1_to_n: 
, 
, ⊢ 
, , ⊢ 
In [43]:
and_C_1_to_n.derive_quantification(j)
, , ⊢ 
In [44]:
from proveit.logic.booleans.conjunction import any_from_and
any_from_and
In [ ]:
In [45]:
And(A,B,C).prove(assumptions=[A,C,B])
, , 
⊢ 
In [46]:
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)])
In [47]:
And(A,B,C,D,E).commute(1, 3, assumptions=[And(A,B,C,D,E), *in_bool(A,B,C,D,E)])
In [48]:
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)])
In [49]:
expr = Or(A, B, And(C, D, E))
expr: 
In [50]:
expr.inner_expr().operands[-1].commutation(0, -1, assumptions=in_bool(C, D, E))
, 
, 
⊢ 
In [51]:
kt = expr.inner_expr().operands[-1].associate(0, length=2, assumptions=[expr])
kt: ⊢ 
⊢ 
In [52]:
expr = kt.expr
expr:
In [53]:
expr = expr.inner_expr().operands[-1].disassociate(0, assumptions=[expr])
expr: ⊢
⊢ In [54]:
in_bool(And(A,B)).prove(assumptions=[in_bool(A), in_bool(B)])
, ⊢ 
In [55]:
in_bool(And(A,B,C,D)).prove(assumptions=[in_bool(A), in_bool(B), in_bool(C), in_bool(D)])
, , , ⊢ 
In [56]:
And(A,B).prove(assumptions=[Not(Or(Not(A), Not(B)))])
In [57]:
And(A,B,C).prove(assumptions=[Not(Or(Not(A), Not(B), Not(C)))])
Axioms¶
In [58]:
Equals(And(TRUE, TRUE), TRUE).prove()
In [59]:
Equals(And(TRUE, FALSE), FALSE).prove()
In [60]:
Equals(And(FALSE, TRUE), FALSE).prove()
In [61]:
Equals(And(FALSE, FALSE), FALSE).prove()
In [62]:
in_bool(A).prove(assumptions=[in_bool(And(A,B))])
In [63]:
in_bool(B).prove(assumptions=[in_bool(And(A,B))])
In [64]:
Equals(And(FALSE, TRUE), FALSE).prove()
In [65]:
Equals(And(FALSE, FALSE), FALSE).prove()
In [66]:
in_bool(A).prove(assumptions=[in_bool(And(A,B))])
In [67]:
in_bool(B).prove(assumptions=[in_bool(And(A,B))])
Testing And.conclude_over_expr_range()¶
In [68]:
from proveit import i, j, k, x, P, Q, Pk, Qx, ExprRange, Function, Lambda
from proveit.logic import Forall, InSet
from proveit.numbers import one, two, three, four, five, Add, Integer, Interval, LessEq
test_conj_over_expr_range_01 = And(ExprRange(x, Qx, j, k))
test_conj_over_expr_range_01: 
In [69]:
our_assumptions_01 = [InSet(i, Integer), InSet(j, Integer),
InSet(k, Integer), LessEq(j, Add(k, one)),
Forall(x, Qx, domain=Interval(j, k))]
our_assumptions_01: 
In [70]:
test_conj_over_expr_range_01.conclude_over_expr_range(assumptions=our_assumptions_01)
, 
, 
, 
⊢
A more concrete case …
In [71]:
test_conj_over_expr_range_02 = And(ExprRange(x, Qx, two, four))
test_conj_over_expr_range_02: 
In [72]:
our_assumptions_02 = [Function(Q, two), Function(Q, three), Function(Q, four),
Forall(x, Qx, domain=Interval(two, four))]
our_assumptions_02: 
In [73]:
LessEq(two, five).prove()
In [74]:
Equals(Add(four, one), five).prove()
In [75]:
test_conj_over_expr_range_02.conclude_over_expr_range(assumptions=our_assumptions_02)
Automatically proving conjunctions are equal via permutation¶
In [76]:
Equals(And(A, B, C, D), And(D, B, A, C)).prove(assumptions=in_bool(A, B, C, D))
, , , ⊢ 
In [77]:
Equals(And(A, C, B, D), And(D, B, C, A)).prove(assumptions=in_bool(A, B, C, D))
, , , ⊢ 
In [78]:
Equals(And(D, C, B, A), And(B, D, C, A)).prove(assumptions=in_bool(A, B, C, D))
, , , ⊢ 
This even works in a nested manner
In [79]:
Equals(And(D, C, Or(A, B), A), And(Or(B, A), D, C, A)).prove(assumptions=in_bool(A, B, C, D))
, , , ⊢ 
In [80]:
%end demonstrations