Demonstrations for the theory of proveit.logic.booleans¶
In [1]:
import proveit
from proveit.logic import Boolean, TRUE, FALSE, in_bool, Implies, Not, And, Or, Forall
from proveit.logic import Equals, NotEquals, InSet
from proveit import A, B, C, P, Q, PofA, QofA, Function
from proveit.logic import PofTrue, PofFalse, QimplPofTrue, QimplPofFalse
%begin demonstrations
In [2]:
Equals(TRUE, TRUE).prove()
In [3]:
Equals(FALSE, FALSE).prove()
In [4]:
NotEquals(TRUE, FALSE).prove()
In [5]:
in_bool(A).fold(assumptions=[Or(Equals(A, TRUE), Equals(A, FALSE))])
In [6]:
InSet(TRUE, Boolean).prove()
In [7]:
InSet(FALSE, Boolean).prove()
In [8]:
in_bool(A).prove(assumptions=[A])
in_bool_if_false
In [9]:
in_bool(A).conclude(assumptions=[Not(A)])
In [10]:
NotEquals(A, FALSE).prove(assumptions=[A])
from_not_false
In [11]:
A.prove(assumptions=[NotEquals(A, FALSE), in_bool(A)])
, 
⊢ 
fold_forall_over_bool
In [12]:
Forall(A, PofA, domain=Boolean).prove(assumptions=[PofTrue, PofFalse])
, 
⊢ 
fold_conditioned_forall_over_bool
In [13]:
Forall(A, PofA, domain=Boolean, conditions=[QofA]).prove(assumptions=[QimplPofTrue, QimplPofFalse])
, 
⊢ 
forall_bool_eval_true
In [14]:
Equals(Forall(A, PofA, domain=Boolean), TRUE).prove(assumptions=[Equals(PofTrue, TRUE), Equals(PofFalse, TRUE)])
, 
⊢ 
unfold_forall_over_bool
In [15]:
Forall(A, PofA, domain=Boolean).unfold(assumptions=[Forall(A, PofA, domain=Boolean)])
ForallBoolEvalFalseViaFF
In [16]:
#Implies(And(Equals(PofTrue, FALSE), Equals(PofFalse, FALSE)), Equals(Forall(A, PofA, domain=Boolean), FALSE)).prove().proof()
ForallBoolEvalFalseViaFT
In [17]:
#Implies(And(Equals(PofTrue, FALSE), Equals(PofFalse, TRUE)), Equals(Forall(A, PofA, domain=Boolean), FALSE)).prove().proof()
ForallBoolEvalFalseViaTF
In [18]:
#Implies(And(Equals(PofTrue, TRUE), Equals(PofFalse, FALSE)), Equals(Forall(A, PofA, domain=Boolean), FALSE)).prove().proof()
In [19]:
Or(A, Not(A)).prove(assumptions=[in_bool(A)])
from_excluded_middle
In [20]:
Forall(A, C, domain=Boolean,conditions=[Implies(A, C),Implies(Not(A), C)]).prove()
In [21]:
example_forall = Forall(A, Forall(B, Function(P, [A, B]), domain=Boolean), domain=Boolean)
example_forall: 
In [22]:
example_forall.all_instance_exprs()[-1]
In [23]:
%end demonstrations