from proveit import (Literal, Operation, defaults, USE_DEFAULTS,
composite_expression, ProofFailure,
prover, relation_prover, equality_prover)
from proveit.logic.booleans.negation import Not
from proveit import A, B, C
from proveit import TransitiveRelation
[docs]class Implies(TransitiveRelation):
_operator_ = Literal(
string_format='=>',
latex_format=r'\Rightarrow',
theory=__file__)
# map left-hand-sides to Subset Judgments
# (populated in TransitivityRelation.derive_side_effects)
known_left_sides = dict()
# map right-hand-sides to Subset Judgments
# (populated in TransitivityRelation.derive_side_effects)
known_right_sides = dict()
def __init__(self, antecedent, consequent, *, styles=None):
TransitiveRelation.__init__(
self, Implies._operator_, antecedent, consequent,
styles=styles)
self.antecedent = antecedent
self.consequent = consequent
[docs] @staticmethod
def WeakRelationClass():
'''
The Strong and Weak form of transitive relations are the same for implication.
It counts as a weak form because (A => A) is always true.
'''
return Implies
[docs] @staticmethod
def StrongRelationClass():
'''
The Strong and Weak form of transitive relations are the same for implication.
'''
return Implies
[docs] def side_effects(self, judgment):
'''
Yield the TransitiveRelation side-effects (which also records
known_left_sides nd known_right_sides). Also derive the consequent
as a side-effect if the antecedent is known to be true
(under the "side-effect" assumptions).
As a special case, if the consequent is FALSE, do
derive_via_contradiction.
'''
from proveit.logic.booleans import FALSE
for side_effect in TransitiveRelation.side_effects(self, judgment):
yield side_effect
if self.antecedent.readily_provable():
# Derive the consequent by proving the antecedent.
yield self.derive_consequent # B given A=>B and A
else:
# Derive the consequent by assuming the antecedent, but
# don't propogate further side-effects.
yield self._derive_consequent_generically
if self.consequent == FALSE:
# Not(A) given A=>FALSE or A given Not(A)=>FALSE
yield self.derive_via_contradiction
[docs] def negation_side_effects(self, judgment):
'''
Side-effect derivations to attempt automatically when an implication is negated.
implemented by JML on 6/17/19
'''
yield self.deduce_negated_left_impl # Not(A <=> B) given Not(B => A)
yield self.deduce_negated_right_impl # Not(A <=> B) given Not(A => B)
yield self.deduce_negated_reflex # B => A given Not(A => B)
def _readily_provable(self):
'''
A => B is readily provable if B is readily provable given A
or A is readily disprovable.
'''
cons_assumptions = defaults.assumptions + (self.antecedent,)
return self.consequent.readily_provable(
assumptions=cons_assumptions) or (
self.antecedent.readily_disprovable())
def _readily_disprovable(self):
'''
A => B is readily disprovable if A is readily provable
and B is readily disprovable.
'''
return self.consequent.readily_disprovable() and (
self.antecedent.readily_provable())
[docs] @prover
def conclude(self, **defaults_config):
'''
Try to automatically conclude this implication by reducing its
operands to true/false, or by doing a "transitivity" search
amongst known true implications whose assumptions are covered by
the given assumptions.
'''
from . import (
true_implies_true, false_implies_true, false_implies_false,
false_antecedent_implication, falsified_antecedent_implication,
untrue_antecedent_implication)
from proveit.logic import TRUE, FALSE, NotEquals
if self.antecedent == self.consequent:
return self.conclude_self_implication()
if self in {
true_implies_true,
false_implies_true,
false_implies_false}:
# should be proven via one of the imported theorems as a simple
# special case
try:
return self.evaluation()
except BaseException:
return self.prove()
if self.antecedent == FALSE:
# The antecedent is FALSE, so we should try to prove the
# implication via false_antecedent_implication.
return false_antecedent_implication.instantiate(
{A: self.consequent})
elif NotEquals(self.antecedent, TRUE).proven():
# The antecedent is known to be not equal to true, so
# prove the implication via untrue_antecedent_implication.
return untrue_antecedent_implication.instantiate(
{A: self.antecedent, B: self.consequent})
elif (self.antecedent.readily_disprovable() or
self.consequent.readily_disprovable()):
# Either the consequent or the antecedent is disprovable
# so we should try to prove the implication via
# falsified_antecedent_implication.
return falsified_antecedent_implication.instantiate(
{A: self.antecedent, B: self.consequent})
with defaults.temporary() as tmp_defaults:
tmp_defaults.assumptions = (
defaults.assumptions + (self.antecedent,))
if self.consequent.readily_provable():
# The consequent is provable assuming the antecedent,
# so we can prove the implication via Deduction.
return self.consequent.prove().as_implication(
self.antecedent)
try:
# try to prove the implication via deduction.
with defaults.temporary() as temp_defaults:
temp_defaults.assumptions = (defaults.assumptions +
(self.antecedent,))
return self.consequent.prove().as_implication(
self.antecedent)
except ProofFailure:
raise ProofFailure(self, defaults.assumptions,
"Unable to automatically conclude by "
"standard means. To try to prove this via "
"transitive implication relations, try "
"'conclude_via_transitivity'.")
[docs] @prover
def conclude_negation(self, **defaults_config):
'''
Try to conclude Not(A => B) because A is true and B is false.
'''
from proveit.logic.booleans import FALSE, TRUE
if self.antecedent == TRUE and self.consequent == FALSE:
from . import true_implies_false_negated
return true_implies_false_negated
else:
from . import invalid_implication
return invalid_implication.instantiate(
{A:self.antecedent, B:self.consequent})
[docs] @prover
def conclude_via_double_negation(self, **defaults_config):
'''
From A => B return A => Not(Not(B)).
implemented by JML on 6/18/19
'''
from . import double_negate_consequent
if isinstance(self.consequent.operand, Not):
return double_negate_consequent.instantiate(
{A: self.antecedent, B: self.consequent.operand.operand})
return "Not of the form 'A => B'"
@equality_prover('shallow_simplified', 'shallow_simplify')
def shallow_simplification(self, *, must_evaluate=False,
**defaults_config):
'''
If the operands that to TRUE or FALSE, we can
evaluate this expression as TRUE or FALSE.
'''
# IMPORTANT: load in truth-table evaluations
from . import implies_t_t, implies_t_f, implies_f_t, implies_f_f
try:
return Operation.shallow_simplification(
self, must_evaluate=must_evaluate)
except NotImplementedError:
# Should have been able to do the evaluation from the
# loaded truth table.
# If it can't we are unable to evaluate it.
from proveit.logic import EvaluationError
raise EvaluationError(self)
[docs] @prover
def derive_consequent(self, **defaults_config):
r'''
From A => B derive and return B assuming A.
'''
from proveit._core_.proof import ModusPonens
self.antecedent.prove()
return ModusPonens(self, defaults.assumptions).proven_truth
def _derive_consequent_generically(self, **defaults_config):
'''
Drive the consequent assuming the antecedent.
Do not propagate further side-effects.
'''
with defaults.temporary() as tmp_defaults:
tmp_defaults.automation = False
tmp_defaults.assumptions = defaults.assumptions + (
self.antecedent,)
return self.derive_consequent()
[docs] @prover
def derive_iff(self, **defaults_config):
r'''
From A => B derive and return A <=> B assuming B => A.
'''
from proveit.logic import Iff
return Iff(self.A, self.B).conclude_via_definition()
[docs] @prover
def deduce_negated_right_impl(self, **defaults_config):
r'''
From Not(A => B) derive and return Not(A <=> B).
implemented by JML on 6/18/19
'''
from . import not_iff_via_not_right_impl
return not_iff_via_not_right_impl.instantiate(
{A: self.antecedent, B: self.consequent})
[docs] @prover
def deduce_negated_left_impl(self, **defaults_config):
r'''
From Not(B => A) derive and return Not(A <=> B).
implemented by JML on 6/18/19
'''
from . import not_iff_via_not_left_impl
return not_iff_via_not_left_impl.instantiate(
{B: self.antecedent, A: self.consequent})
[docs] @prover
def deduce_negated_reflex(self, **defaults_config):
# implemented by JML on 6/18/19
from . import negated_reflex
return negated_reflex.instantiate(
{A: self.antecedent, B: self.consequent})
[docs] @prover
def deny_antecedent(self, **defaults_config):
'''
From A => B, derive and return Not(A) assuming Not(B).
'''
from . import modus_tollens_affirmation, modus_tollens_denial
if isinstance(self.antecedent, Not):
return modus_tollens_affirmation.instantiate(
{A: self.antecedent.operand, B: self.consequent})
else:
return modus_tollens_denial.instantiate(
{A: self.antecedent, B: self.consequent})
[docs] @prover
def apply_transitivity(self, other_impl, **defaults_config):
'''
From A => B (self) and a given B => C (other_impl),
derive and return A => C.
'''
from . import implication_transitivity
if self.consequent == other_impl.antecedent:
return implication_transitivity.instantiate(
{A: self.antecedent, B: self.consequent,
C: other_impl.consequent}, preserve_all=True)
elif self.antecedent == other_impl.consequent:
return implication_transitivity.instantiate(
{A: other_impl.antecedent, B: self.antecedent,
C: self.consequent}, preserve_all=True)
[docs] @prover
def derive_via_contradiction(self, **defaults_config):
r'''
From (Not(A) => FALSE), derive and return A assuming A in Boolean.
Or from (A => FALSE), derive and return Not(A) assuming A in Boolean.
Or from (A => FALSE), derive and return A != TRUE.
'''
from proveit.logic import FALSE, in_bool
from . import affirmation_via_contradiction, denial_via_contradiction
from . import not_true_via_contradiction
if self.consequent != FALSE:
raise ValueError(
'derive_via_contradiction method is only applicable if FALSE is implicated, not for ' +
str(self))
if isinstance(self.antecedent, Not):
stmt = self.antecedent.operand
return affirmation_via_contradiction.instantiate({A: stmt})
else:
if in_bool(self.antecedent).proven():
return denial_via_contradiction.instantiate(
{A: self.antecedent})
else:
return not_true_via_contradiction.instantiate(
{A: self.antecedent})
[docs] @prover
def conclude_self_implication(self, **defaults_config):
from . import self_implication
if self.antecedent != self.consequent:
raise ValueError(
'May only conclude a self implementation when the antecedent and consequent are the same')
return self_implication.instantiate({A: self.antecedent})
[docs] @prover
def generalize(self, forall_vars, domain=None, conditions=tuple(), **defaults_config):
r'''
This makes a generalization of this expression, prepending Forall
operations according to new_forall_vars and new_conditions and/or new_domain
that will bind 'arbitrary' free variables. This overrides the expr
version to absorb antecedent into conditions if they match. For example,
[A(x) => [B(x, y) => P(x, y)]] generalized
forall x, y such that A(x), B(x, y)
becomes forall_{x, y | A(x), B(x, y)} P(x, y).
'''
from proveit.logic import InSet
hypothesized_conditions = set()
conditions_set = set(composite_expression(conditions))
if domain is not None:
# add in the effective conditions from the domain
for var in composite_expression(forall_vars):
conditions_set.add(InSet(var, domain))
expr = self
while isinstance(expr, Implies) and expr.antecedent in conditions_set:
hypothesized_conditions.add(expr.antecedent)
expr = expr.consequent
if len(hypothesized_conditions) == 0:
# Just use the expr version
return expr.generalize(self, forall_vars, domain, conditions)
return expr.generalize(expr, forall_vars, domain, conditions)
# return Forall(new_forall_vars, expr, new_conditions)
[docs] @prover
def contrapose(self, **defaults_config):
'''
Depending upon the form of self with respect to negation of the antecedent and/or consequent,
will derive from self and return as follows:
* From [not(A) => not(B)], derive [B => A] assuming A in \mathcal{B}.
* From [not(A) => B], derive [not(B) => A] assuming A in \mathcal{B}, B in \mathcal{B}.
* From [A => not(B)], derive [B => not(A)] assuming A in \mathcal{B}.
* From [A => B], derive [not(B) => not(A)]` assuming A in \mathcal{B}, B in \mathcal{B}.
'''
from . import from_contraposition, to_contraposition, contrapose_neg_consequent, contrapose_neg_antecedent
from proveit.logic import Not
if isinstance(
self.antecedent,
Not) and isinstance(
self.consequent,
Not):
return from_contraposition.instantiate(
{B: self.antecedent.operand, A: self.consequent.operand})
elif isinstance(self.antecedent, Not):
return contrapose_neg_antecedent.instantiate(
{A: self.antecedent.operand, B: self.consequent})
elif isinstance(self.consequent, Not):
return contrapose_neg_consequent.instantiate(
{A: self.antecedent, B: self.consequent.operand})
else:
return to_contraposition.instantiate(
{A: self.antecedent, B: self.consequent})
@equality_prover('shallow_simplified', 'shallow_simplify')
def shallow_simplification(self, *, must_evaluate=False,
**defaults_config):
'''
Given operands that evaluate to TRUE or FALSE, derive and
return the equality of this expression with TRUE or FALSE.
'''
from proveit.logic import TRUE, FALSE
# load in truth-table evaluations
from . import implies_t_f, implies_t_t, implies_f_t, implies_f_f
if must_evaluate:
start_over = False
for operand in self.operands:
if operand not in (TRUE, FALSE):
# The simplification of the operands may not have
# worked hard enough. Let's work harder if we
# must evaluate.
operand.evaluation()
start_over = True
if start_over: return self.evaluation()
# May now be able to evaluate via loaded truth tables.
return Operation.shallow_simplification(
self, must_evaluate=must_evaluate)
def readily_in_bool(self):
'''
Returns True if we can readily prove that the operands are
provably boolean and therefore this implication is boolean.
'''
from proveit.logic import in_bool
return (in_bool(self.antecedent).readily_provable() and
in_bool(self.consequent).readily_provable())
[docs] @relation_prover
def deduce_in_bool(self, **defaults_config):
'''
Attempt to deduce, then return, that this implication expression is in the set of BOOLEANS.
'''
from . import implication_closure
return implication_closure.instantiate(
{A: self.antecedent, B: self.consequent})
[docs]@prover
def conclude_via_implication(consequent, **defaults_config):
'''
Perform a breadth-first search of implications going in reverse from the consequent
until reaching an antecedent that has been proven.
'''
visited = set()
# map antecedents to consequents that arise durent the breadth-first search
consequent_map = dict()
queue = [consequent]
while len(queue) > 0:
expr = queue.pop()
if expr not in visited:
visited.add(expr)
if expr not in Implies.known_right_sides:
continue # no known implications with the expr as the consequent; skip it
for known_implication in Implies.known_right_sides[expr]:
# see if the known_implication is applicable under the given
# set of assumptions
if known_implication.is_applicable():
local_antecedent, local_consequent = known_implication.antecedent, known_implication.consequent
consequent_map[local_antecedent] = local_consequent
try:
known_implication.antecedent.prove(automation=False)
# found a solution; use it by deriving "local"
# consequents until getting to the desired consequent
while True:
judgment = Implies(
local_antecedent,
local_consequent).derive_consequent()
if judgment.expr == consequent:
return judgment
local_antecedent = judgment.expr
local_consequent = consequent_map[local_antecedent]
except ProofFailure:
queue.append(local_antecedent)
raise ProofFailure(
consequent,
defaults.assumptions,
'Unable to conclude via implications')
@prover
def affirm_via_contradiction(contradictory_expr, conclusion,
**defaults_config):
'''
Affirms the conclusion via reductio ad absurdum.
First calls derive_contradiction on the contradictory_expr to derive
FALSE, then derive the conclusion after proving that the negated
conclusion implies FALSE. The conclusion must be a Boolean.
'''
from proveit.logic import Not
extended_assumptions = defaults.assumptions + (Not(conclusion),)
contradiction = contradictory_expr.derive_contradiction(
assumptions=extended_assumptions)
impl = contradiction.as_implication(Not(conclusion))
return impl.derive_via_contradiction(preserve_expr=contradictory_expr)
@prover
def deny_via_contradiction(contradictory_expr, conclusion,
**defaults_config):
'''
Deny the conclusion (affirm its negation) via reductio ad absurdum.
First calls derive_contradiction on the contradictory_expr to derive
FALSE, then derive the negated conclusion after proving that the
conclusion itself implies FALSE. The conclusion must be a Boolean.
'''
extended_assumptions = defaults.assumptions + (conclusion,)
contradiction = contradictory_expr.derive_contradiction(
assumptions=extended_assumptions)
impl = contradiction.as_implication(conclusion)
return impl.derive_via_contradiction(preserve_expr=contradictory_expr)