from proveit import (Expression, Literal, Operation, Conditional,
defaults, USE_DEFAULTS, ProofFailure, InnerExpr,
prover, relation_prover, equality_prover,
SimplificationDirectives, TransRelUpdater)
from proveit.logic.equality import Equals, SimplificationError
from proveit import i, j, k, l, m, n, A, B, C, D, E, F, G, P
from proveit.logic.booleans.booleans import in_bool
from proveit.abstract_algebra.generic_methods import (
apply_commutation_thm, apply_association_thm, apply_disassociation_thm,
group_commutation, group_commute, generic_permutation,
deduce_equality_via_commutation, prove_via_grouping_ranges)
[docs]class And(Operation):
# The operator of the And operation
_operator_ = Literal(
string_format='and',
latex_format=r'\land',
theory=__file__)
_simplification_directives_ = SimplificationDirectives(
ungroup=True)
def __init__(self, *operands, styles=None):
r'''
And together any number of operands: :math:`A \land B \land C`
'''
Operation.__init__(self, And._operator_, operands, styles=styles)
def _formatted(self, format_type, **kwargs):
'''
Override Operation._formatted when formatting a conjunction
of relations as a total ordering.
'''
if self.get_style('as_total_ordering', 'False') == 'True':
self._check_total_ordering_applicability()
relations = self.operands.entries
operands = [rel.lhs for rel in relations] + [relations[-1].rhs]
formatted_operators = [
rel.operator.formatted(format_type) if
rel.get_style('direction', 'normal') == 'normal'
else rel.__class__.reversed_operator_str(format_type)
for rel in relations]
return Operation._formatted_operation(
format_type,
formatted_operators,
operands,
wrap_positions=self.wrap_positions(),
justification=self.get_style('justification'),
**kwargs)
else:
# Just use the default Operation._formatted method.
return Operation._formatted(self, format_type, **kwargs)
[docs] def remake_with_style_calls(self):
'''
In order to reconstruct this Expression to have the same styles,
what "with..." method calls are most appropriate? Return a
tuple of strings with the calls to make. The default for the
Operation class is to include appropriate 'with_wrapping_at'
and 'with_justification' calls.
'''
call_strs = Operation.remake_with_style_calls(self)
if self.get_style('as_total_ordering', 'False') == 'True':
call_strs.append('with_total_ordering_style()')
return call_strs
def _check_total_ordering_applicability(self):
'''
Check to see if the total ordering style is
applicable, raising an exception otherwise.
'''
from proveit.relation import TransitiveRelation
relations = self.operands.entries
for relation in relations:
if not isinstance(relation, TransitiveRelation):
raise TypeError(
"Can only to effect a total ordering style on "
"a conjunction of TransitiveRelation objects, "
"not %s of type %s"
%(relation, relation.__class__))
for rel1, rel2 in zip(relations[:-1], relations[1:]):
if rel1.rhs != rel2.lhs:
raise ValueError(
"Consecutive total ordering relations must "
"match rhs to lhs: %s and %s do not match"
%(rel1, rel2))
[docs] def style_options(self):
'''
Return the StyleOptions object for this And expression.
'''
style_options = Operation.style_options(self)
try:
self._check_total_ordering_applicability()
style_options.add_option(
name = "as_total_ordering",
description = ("When 'True', style the conjunction as a "
"total ordering (e.g. x < y < z from "
"(x < y) and (y < z))"),
default = None,
related_methods = ('with_total_ordering_style',))
except (TypeError, ValueError):
pass # total ordering is not applicable
return style_options
[docs] def with_total_ordering_style(self):
'''
Use the total ordering style.
'''
self._check_total_ordering_applicability()
return self.with_styles(as_total_ordering='True')
def _readily_provable(self):
'''
Return True iff we should be able to conclude this conjunction.
Specifically, if all operands are provable, than the conjunction
should be provable.
'''
from proveit import ExprRange
univ_quant = self._as_quantification()
if univ_quant is not None:
# See if the corresponding universal quantification is
# readily provable:
# P(i) and ... and P(j) <=>
# forall_{k in {i .. j}} P(k)
return univ_quant.readily_provable()
for operand in self.operands:
if isinstance(operand, ExprRange):
if not And(operand).readily_provable():
return False
elif not operand.readily_provable():
return False
return True
def _readily_disprovable(self):
'''
Return True iff we should be able to conclude the negation
of this conjunction.
Specifically, if any operands is disprovable, than the
negation of the conjunction should be provable.
'''
from proveit import ExprRange
univ_quant = self._as_quantification()
if univ_quant is not None:
# See if the corresponding universal quantification is
# readily disprovable:
# P(i) and ... and P(j) <=>
# forall_{k in {i .. j}} P(k)
return univ_quant.readily_disprovable()
for operand in self.operands:
if isinstance(operand, ExprRange):
if And(operand).readily_disprovable():
return True
elif operand.readily_disprovable():
return True
return False
def _as_quantification(self):
'''
If this is a conjunction over a single ExprRange entry,
return the equivalent universal quantification:
P(i) and ... and P(j) <=> forall_{k in {i .. j}} P(k)
'''
from proveit import ExprRange
if (self.operands.num_entries() == 1 and
isinstance(self.operands[0], ExprRange)):
from proveit.logic import Forall
expr_range = self.operands[0]
univ_quant = Forall(
expr_range.parameter,
expr_range.body,
condition = expr_range.parameter_condition())
return univ_quant
return None
[docs] @prover
def conclude(self, **defaults_config):
'''
Try to automatically conclude this conjunction via composing
the constituents.
That is, conclude some A and B and ... and Z via
A, B, ..., Z individually.
'''
from proveit import ExprRange
from . import true_and_true
if self == true_and_true.expr:
return true_and_true # simple special case
# if (self.operands.num_entries() == 1 and
# isinstance(self.operands[0], ExprRange) and
# self.operands[0].is_parameter_independent):
# return self.conclude_as_redundant()
if (self.operands.num_entries() == 1 and
isinstance(self.operands[0], ExprRange)):
if self.operands[0].is_parameter_independent:
return self.conclude_as_redundant()
else:
return self.conclude_over_expr_range()
return self.conclude_via_composition()
[docs] @prover
def conclude_negation(self, **defaults_config):
'''
Prove the negation of this conjunction (by disproving any
operand).
'''
from . import (
true_and_false_negated,
false_and_true_negated,
false_and_false_negated)
from proveit.logic import Not, FALSE
not_self = Not(self)
if not_self in {
true_and_false_negated.expr,
false_and_true_negated.expr,
false_and_false_negated.expr}:
# should be disproven via one of the imported theorems as a
# simple special case
return not_self.prove()
# Prove that the conjunction is true by proving that one of
# its operands is false and then negate it.
if self.operands.contains_range():
if self.operands.num_entries()==1:
# Just a single ExprRange. Conclude the negation
# through an evaluation which will equate it to
# a universal quantification.
evaluation = self.evaluation()
if evaluation.rhs == FALSE:
return self.disprove()
raise ProofFailure(Not(self), defaults.assumptions,
"Expected evaluation to be FALSE, got %s"
%evaluation)
# Group each ExprRange operand, call conclude_negation,
# then disassociate the ExprRange operands.
return prove_via_grouping_ranges(
self,
lambda expr, **kwargs: expr.conclude_negation(**kwargs))
for operand in self.operands:
if operand.readily_disprovable():
# With one disprovable operand, we can prove the
# negated conjunction.
return self.conclude_negation_via_example(operand)
raise ProofFailure(not_self, defaults.assumptions,
"Unable to conclude the negated conjunction; "
"we could not disprove any of the conjunction "
"operands.")
[docs] def side_effects(self, judgment):
'''
Side-effect derivations to attempt automatically.
'''
from proveit.logic import Not
from proveit import ExprRange
if self.operands.num_entries() == 0:
return # No side-effects needed for [And]().
if self.operands.is_double():
if self.operands[1] == Not(self.operands[0]):
# (A or not(A)) is an unfolded Boolean
return # stop to avoid infinite recursion.
yield self.derive_in_bool
for _i, operand in enumerate(self.operands):
if (isinstance(operand, ExprRange) and
self.operands.num_entries()==1):
yield lambda : self.derive_quantification()
else:
yield lambda : self.derive_any(_i)
# yield self.derive_commutation
[docs] def negation_side_effects(self, judgment):
'''
Side-effect derivations to attempt automatically for
Not(A and B and .. and .. Z).
'''
from proveit.logic import Not, Or
yield self.derive_in_bool # (A and B and ... and Z) in Boolean
# implemented by JML on 7/2/19
# If all of the operands are negated call the disjunction form of
# DeMorgan's
if all(isinstance(operand, Not) for operand in self.operands):
demorgan_or = Or(*[operand.operand for operand in self.operands])
yield demorgan_or.conclude_via_demorgans
[docs] def in_bool_side_effects(self, judgment):
'''
From (A and B and .. and Z) in Boolean deduce
(A in Boolean), (B in Boolean), ... (Z in Boolean).
'''
from proveit import ExprRange
for _i in range(self.operands.num_entries()):
if not isinstance(self.operands[_i], ExprRange):
yield lambda : self.deduce_part_in_bool(_i)
def _build_canonical_form(self):
'''
Returns a form of this operation in which the operands are
in a deterministically sorted order used to determine equal
expressions given commutativity of this operation under
appropriate conditions.
'''
return And(*sorted([operand.canonical_form() for operand
in self.operands.entries], key=hash))
def _deduce_canonically_equal(self, rhs):
equality = Equals(self, rhs)
return deduce_equality_via_commutation(equality, one_side=self)
[docs] @prover
def derive_any(self, index_or_expr, **defaults_config):
r'''
From (A and ... and X and ... and Z) derive X.
index_or_expr specifies X, either by index or the expression.
If X is an ExprRange, derive the universally quantified
form of And(X).
'''
from proveit import ExprRange
from . import (any_from_and, left_from_and, right_from_and,
from_unary_and)
if isinstance(index_or_expr, int):
idx = index_or_expr
else:
idx = list(self.operands).index(index_or_expr)
if idx < 0 or idx >= self.operands.num_entries():
raise IndexError("Operand out of range: " + str(idx))
contains_range = self.operands.contains_range()
if self.operands.num_entries() == 1 and not contains_range:
# Derive A from And(A).
return from_unary_and.instantiate({A: self.operands[0]})
if self.operands.is_double() and not contains_range:
# Two operand special case:
if idx == 0:
return left_from_and.instantiate(
{A: self.operands[0], B: self.operands[1]})
elif idx == 1:
return right_from_and.instantiate(
{A: self.operands[0], B: self.operands[1]})
else:
# Multiple operands.
from proveit.core_expr_types import Len
operand_to_extract = self.operands[idx]
if isinstance(operand_to_extract, ExprRange):
# Derive the conjunction of a range of operands.
return self.derive_some(idx)
else:
A_sub = self.operands[:idx]
B_sub = self.operands[idx]
C_sub = self.operands[idx + 1:]
m_val = Len(A_sub).computed()
n_val = Len(C_sub).computed()
return any_from_and.instantiate(
{m: m_val, n: n_val, A: A_sub, B: B_sub, C: C_sub})
[docs] @prover
def derive_some(self, start_idx, end_idx=None, **defaults_config):
'''
From (A and ... and B and ... Z) derive a range of the
conjunction, such as (C and ... and F). Specify the range
by providing the start and end indices (inclusive) w.r.t.
operand entries. If end_idx is not provided, it defaults
to start_idx for a single entry which should be an ExprRange.
'''
from proveit.core_expr_types import Len
from proveit.logic.booleans.conjunction import some_from_and
if end_idx is None:
end_idx = start_idx
A_sub = self.operands[:start_idx]
B_sub = self.operands[start_idx:end_idx + 1]
C_sub = self.operands[end_idx + 1:]
l_val = Len(A_sub).computed()
m_val = Len(B_sub).computed()
n_val = Len(C_sub).computed()
return some_from_and.instantiate({l: l_val, m: m_val, n: n_val,
A: A_sub, B: B_sub, C: C_sub})
@prover
def derive_quantification(self, instance_param=None, **defaults_config):
'''
From P(i) and ... and P(j), represented as a single ExprRange
in a conjunction, prove
forall_{k in {i .. j}} P(k).
If 'instance_param' is provided, use it as the 'k' parameter.
Otherwise, use the parameter of the ExprRange.
'''
from proveit import ExprRange
from proveit.logic import InSet
from proveit.numbers import Interval
from . import quantification_from_conjunction
if (self.operands.num_entries() != 1 or
not isinstance(self.operands[0], ExprRange)):
raise ValueError("'derive_quantification' may only be used "
"on a conjunction with a single ExprRange "
"operand entry.")
expr_range = self.operands[0]
_i = expr_range.true_start_index
_j = expr_range.true_end_index
_k = expr_range.parameter if instance_param is None else instance_param
_P = expr_range.lambda_map
proven_quantification = quantification_from_conjunction.instantiate(
{i:_i, j:_j, k:_k, P:_P},
preserve_expr=self).derive_consequent()
if defaults.sideeffect_automation:
# While we are at it, as an "unofficial" side-effect,
# let's instantatiate forall_{k in {i .. j}} P(k) to derive
# {k in {i .. j}} |- P(k)
# and induce side-effects for P(k).
assumptions = defaults.assumptions + (
InSet(_k, Interval(_i, _j)), )
proven_quantification.instantiate(assumptions=assumptions)
# We'll do it with the canonical variable as well for good
# measure, if it is any different.
canonical_version = proven_quantification.canonically_labeled()
if canonical_version._style_id != proven_quantification._style_id:
_k = canonical_version.instance_var
assumptions = defaults.assumptions + (
InSet(_k, Interval(_i, _j)), )
canonical_version.instantiate(assumptions=assumptions)
return proven_quantification
[docs] @prover
def derive_left(self, **defaults_config):
r'''
From A and B derive A.
'''
if self.operands.num_entries() != 2:
raise Exception(
'derive_left only applicable for binary conjunction operations')
return self.derive_any(0)
[docs] @prover
def derive_right(self, **defaults_config):
r'''
From A and B derive B.
'''
if self.operands.num_entries() != 2:
raise Exception(
'derive_right only applicable for binary conjunction operations')
return self.derive_any(1)
[docs] @equality_prover('unary_reduced', 'unary_reduce')
def unary_reduction(self, **defaults_config):
from proveit.logic.booleans.conjunction import \
unary_and_reduction
if not self.operands.is_single():
raise ValueError("Expression must have a single operand in "
"order to invoke unary_reduction")
operand = self.operands[0]
return unary_and_reduction.instantiate({A: operand})
[docs] @prover
def conclude_via_composition(self, **defaults_config):
'''
Prove and return some (A and B ... and ... Z) via
A, B, ..., Z each proven individually.
See also the compose method to do this constructively.
'''
return compose(*self.operands.entries)
[docs] @prover
def deduce_left_in_bool(self, **defaults_config):
'''
Deduce A in Boolean from (A and B) in Boolean.
'''
from . import left_in_bool
if self.operands.is_double():
return left_in_bool.instantiate(
{A: self.operands[0], B: self.operands[1]})
raise ValueError("'deduce_left_in_bool' not applicable to %s, "
"only applicable when there are two operands."
%self)
[docs] @prover
def deduce_right_in_bool(self, **defaults_config):
'''
Deduce B in Boolean from (A and B) in Boolean.
'''
from . import right_in_bool
if self.operands.is_double():
return right_in_bool.instantiate(
{A: self.operands[0], B: self.operands[1]})
raise ValueError("'deduce_right_in_bool' not applicable to %s, "
"only applicable when there are two operands."
%self)
[docs] @prover
def deduce_part_in_bool(self, index_or_expr, **defaults_config):
'''
Deduce X in Boolean from (A and B and .. and X and .. and Z) in Boolean
provided X by expression or index number.
'''
from . import each_is_bool
idx = (index_or_expr if isinstance(index_or_expr, int) else
self.operands.entries.index(index_or_expr))
if idx < 0 or idx >= self.operands.num_entries():
raise IndexError("Operand out of range: " + str(idx))
if self.operands.is_double():
if idx == 0:
return self.deduce_left_in_bool()
elif idx == 1:
return self.deduce_right_in_bool()
else:
_A = self.operands[:idx]
_B = self.operands[idx]
_C = self.operands[idx + 1:]
_m = _A.num_elements()
_n = _C.num_elements()
return each_is_bool.instantiate(
{m: _m, n: _n, A: _A, B: _B, C: _C})
[docs] @prover
def conclude_via_demorgans(self, **defaults_config):
'''
# created by JML 6/28/19
From A and B and C conclude Not(Not(A) or Not(B) or Not(C))
'''
from . import demorgans_law_or_to_and, demorgans_law_or_to_and_bin
if self.operands.is_double():
return demorgans_law_or_to_and_bin.instantiate(
{A: self.operands[0], B: self.operands[1]})
else:
_A = self.operands
_m = _A.num_elements()
return demorgans_law_or_to_and.instantiate({m: _m, A: _A})
@prover
def conclude_negation_via_example(self, false_operand, **defaults_config):
'''
From one false operand, conclude the negation of this
conjunction. Requires all of the operands to be in the
BOOLEAN set.
'''
from . import (nand_if_not_one, nand_if_not_left, nand_if_not_right,
nand_if_neither, nand_if_right_but_not_left,
nand_if_left_but_not_right)
index = self.operands.index(false_operand)
if self.operands.is_double():
_A, _B = self.operands
if index == 0:
if self.operands[1].readily_disprovable():
# May be a shorter proof
nand_if_neither.instantiate({A:_A, B:_B})
elif self.operands[1].readily_provable():
# May be a shorter proof
nand_if_right_but_not_left.instantiate({A:_A, B:_B})
return nand_if_not_left.instantiate(
{A: self.operands[0], B: self.operands[1]})
elif index == 1:
if self.operands[0].readily_disprovable():
# May be a shorter proof
nand_if_neither.instantiate({A:_A, B:_B})
elif self.operands[0].readily_provable():
# May be a shorter proof
nand_if_left_but_not_right.instantiate({A:_A, B:_B})
return nand_if_not_right.instantiate(
{A: self.operands[0], B: self.operands[1]})
_A = self.operands[:index]
_B = self.operands[index]
_C = self.operands[index + 1:]
_m = _A.num_elements()
_n = _C.num_elements()
return nand_if_not_one.instantiate(
{m: _m, n: _n, A: _A, B: _B, C: _C})
[docs] @prover
def conclude_as_redundant(self, **defaults_config):
'''
Conclude an expression of the form
A and ..n repeats.. and A
given n in Natural and A is TRUE.
'''
from proveit import ExprRange
from proveit.numbers import one
from . import redundant_conjunction, redundant_conjunction_general
if (self.operands.num_entries() != 1 or
not isinstance(self.operands[0], ExprRange) or
not self.operands[0].is_parameter_independent):
raise ValueError("`And.conclude_as_redundant` only allowed for a "
"conjunction of the form "
"A and ..n repeats.. and A, not %s" % self)
expr_range = self.operands[0]
_A = expr_range.body
if expr_range.true_start_index == one:
return redundant_conjunction.instantiate(
{n: expr_range.true_end_index, A: _A})
else:
_i, _j = expr_range.true_start_index, expr_range.true_end_index
return redundant_conjunction_general.instantiate(
{i:_i, j:_j, A:_A})
@prover
def conclude_over_expr_range(self, **defaults_config):
'''
Conclude a conjunction over an ExprRange via the
equivalent universal quantification.
'''
from proveit import ExprRange, Lambda
from . import conjunction_from_quantification
if (self.operands.num_entries() != 1 or
not isinstance(self.operands[0], ExprRange)):
raise ValueError(
"'And.conclude_over_expr_range()' only allowed "
"for a conjunction of the form "
"P(i) and P(i+1) and .. and P(j) (i.e. a conjunction "
"over a single ExprRange), but instead you have: {}".
format(self))
the_expr_range = self.operands[0]
_i_sub = the_expr_range.true_start_index
_j_sub = the_expr_range.true_end_index
_k_sub = the_expr_range.parameter
_P_sub = Lambda(the_expr_range.parameter, the_expr_range.body)
impl = conjunction_from_quantification.instantiate(
{i: _i_sub, j: _j_sub, k: _k_sub, P: _P_sub})
return impl.derive_consequent()
@equality_prover('shallow_simplified', 'shallow_simplify')
def shallow_simplification(self, *, must_evaluate=False,
**defaults_config):
'''
Attempt to determine whether this conjunction, with
simplified operands, evaluates to TRUE or FALSE under the given
assumptions. If all operands have simplified to TRUE,
the conjunction is TRUE. If any of the operands have
simplified to FALSE, the conjunction may be FALSE (if the
other operands are provably Boolean).
If it can't be evaluated, and must_evaluate is False,
ungroup nested conjunctions if that is an active
simplification direction. Also, if applicable, perform
a unary reduction: And(A) = A.
'''
from proveit import ExprRange
from proveit.logic import (Equals, FALSE, TRUE, EvaluationError,
is_irreducible_value)
# load in truth-table evaluations
from . import (and_t_t, and_t_f, and_f_t, and_f_f,
conjunction_eq_quantification)
if self.operands.num_entries() == 0:
from proveit.logic.booleans.conjunction import \
empty_conjunction_eval
# And() = TRUE
return empty_conjunction_eval
# Check whether or not all of the operands are TRUE
# or any are FALSE.
all_are_true = True
for operand in self.operands:
if operand != TRUE:
all_are_true = False
if operand == FALSE:
# If any simplified operand is FALSE, the conjunction
# may only evaluate to FALSE if it can be evaluated.
# Only use automation here if 'must_evaluate' is True.
self.conclude_negation(automation=must_evaluate)
return Equals(self, FALSE).prove()
# If all of the operands are TRUE, we can prove that the
# conjunction is equal to TRUE.
if all_are_true:
self.conclude()
return Equals(self, TRUE).prove()
if must_evaluate:
if self.operands.contains_range():
if self.operands.num_entries() == 1:
# Conjunction of a single ExprRange. Convert
# to a universal quantification and evaluate that.
expr_range = self.operands[0]
_i = expr_range.true_start_index
_j = expr_range.true_end_index
_P = expr_range.lambda_map
conj_eq_quant = (conjunction_eq_quantification
.instantiate({i:_i, j:_j, P:_P},
preserve_all=True))
return conj_eq_quant.apply_transitivity(
conj_eq_quant.rhs.evaluation())
return prove_via_grouping_ranges(
self, lambda expr, **kwargs: expr.evaluation(**kwargs))
if not all(is_irreducible_value(operand) for
operand in self.operands):
# The simplification of the operands may not have
# worked hard enough. Let's work harder if we
# must evaluate.
for operand in self.operands:
if not is_irreducible_value(operand):
operand.evaluation()
return self.evaluation()
# Can't evaluate the conjunction if no operand was
# FALSE but they aren't all TRUE.
raise EvaluationError(self)
if self.operands.is_single():
# And(A) = A
return self.unary_reduction()
expr = self
# for convenience updating our equation
eq = TransRelUpdater(expr)
if And._simplification_directives_.ungroup:
# ungroup the expression (disassociate nested conjunctions).
_n = 0
length = expr.operands.num_entries() - 1
# loop through all operands
while _n < length:
operand = expr.operands[_n]
if isinstance(operand, And):
# if it is grouped, ungroup it
expr = eq.update(expr.disassociation(
_n, auto_simplify=False))
length = expr.operands.num_entries()
_n += 1
return Expression.shallow_simplification(self)
def readily_in_bool(self):
'''
Returns True if we can readily prove that all of the operands
are provably boolean and therefore this conjunction is
provably boolean.
'''
from proveit.logic import And
# Or.readily_in_bool calls And.readily_in_bool for convenience,
# so we have to check if this is really and And:
if isinstance(self, And):
from . import closure
if not self.operands.is_double() and not closure.is_usable():
return False
return And(*self.operands.map_elements(in_bool)).readily_provable()
[docs] @relation_prover
def deduce_in_bool(self, **defaults_config):
'''
Attempt to deduce, then return, that this 'and' expression is
in the BOOLEAN set.
'''
from . import binary_closure, closure
if self.operands.is_double():
return binary_closure.instantiate(
{A: self.operands[0], B: self.operands[1]})
_A = self.operands
_m = _A.num_elements()
return closure.instantiate({m: _m, A: _A})
[docs] @equality_prover('commuted', 'commute')
def commutation(self, init_idx=None, final_idx=None,
**defaults_config):
'''
Given Boolean operands, deduce that this expression is equal to a form in which the operand
at index init_idx has been moved to final_idx.
For example, (A and B and ... and Y and Z) = (A and ... and Y and B and Z)
via init_idx = 1 and final_idx = -2.
'''
from . import commutation, leftward_commutation, rightward_commutation
return apply_commutation_thm(
self,
init_idx,
final_idx,
commutation,
leftward_commutation,
rightward_commutation)
[docs] @equality_prover('group_commuted', 'group_commute')
def group_commutation(self, init_idx, final_idx, length,
disassociate=True, **defaults_config):
'''
Given Boolean operands, deduce that this expression is equal to a form in which the operands
at indices [init_idx, init_idx+length) have been moved to [final_idx. final_idx+length).
It will do this by performing association first. If disassociate is True, it
will be disassociated afterwards.
'''
return group_commutation(
self,
init_idx,
final_idx,
length,
disassociate)
[docs] @prover
def commute(self, init_idx=None, final_idx=None, **defaults_config):
'''
From self, derive and return a form in which the operand
at index init_idx has been moved to final_idx.
For example, given (A and B and ... and Y and Z) derive
(A and ... and Y and B and Z)
via init_idx = 1 and final_idx = -2.
'''
from . import commute, leftward_commute, rightward_commute
return apply_commutation_thm(
self, init_idx, final_idx, commute,
leftward_commute, rightward_commute)
[docs] @prover
def group_commute(self, init_idx, final_idx, length, disassociate=True,
**defaults_config):
'''
Given self, deduce and return a form in which the operands
at indices [init_idx, init_idx+length) have been moved to
[final_idx. final_idx+length).
It will do this by performing association first.
If disassocate is True, it will be disassociated afterwards.
'''
return group_commute(
self, init_idx, final_idx, length, disassociate)
@equality_prover('moved', 'move')
def permutation_move(self, init_idx=None, final_idx=None,
**defaults_config):
'''
Given numerical operands, deduce that this expression is equal
to a form in which the operand
at index init_idx has been moved to final_idx.
For example, (a ∧ b · ... ∧ y ∧ z) = (a ∧ ... ∧ y ∧ b ∧ z)
via init_idx = 1 and final_idx = -2.
'''
return self.commutation(init_idx=init_idx, final_idx=final_idx)
@equality_prover('permuted', 'permute')
def permutation(self, new_order=None, cycles=None, **defaults_config):
'''
Deduce that this Add expression is equal to an Add in which
the terms at indices 0, 1, …, n-1 have been reordered as
specified EITHER by the new_order list OR by the cycles list
parameter. For example,
(a∧b∧c∧d).permutation_general(new_order=[0, 2, 3, 1])
and
(a∧b∧c∧d).permutation_general(cycles=[(1, 2, 3)])
would both return ⊢ (a∧b∧c∧d) = (a∧c∧d∧b).
'''
return generic_permutation(self, new_order, cycles)
[docs] @equality_prover('associated', 'associate')
def association(self, start_idx, length, **defaults_config):
'''
Given Boolean operands, deduce that this expression is equal to
a form in which operands in the
range [start_idx, start_idx+length) are grouped together.
For example,
(A and B and ... and Y and Z) =
(A and B ... and (L and ... and M) and ... and Y and Z)
'''
from . import association
return apply_association_thm(
self, start_idx, length, association)
[docs] @prover
def associate(self, start_idx, length, **defaults_config):
'''
From self, derive and return a form in which operands in the
range [start_idx, start_idx+length) are grouped together.
For example, from (A and B and ... and Y and Z) derive
(A and B ... and (L and ... and M) and ... and Y and Z).
'''
from . import associate
return apply_association_thm(
self, start_idx, length, associate)
[docs] @equality_prover('disassociated', 'disassociate')
def disassociation(self, idx, **defaults_config):
'''
Given Boolean operands, deduce that this expression is equal to
a form in which the operand at index idx is no longer grouped
together.
For example,
(A and B ... and (L and ... and M) and ... and Y and Z) =
(A and B and ... and Y and Z)
'''
from . import disassociation
return apply_disassociation_thm(self, idx, disassociation)
[docs] @prover
def disassociate(self, idx, **defaults_config):
'''
From self, derive and return a form in which the operand
at the given index is ungrouped.
For example, from
(A and B ... and (L and ... and M) and ... and Y and Z)
derive (A and B and ... and Y and Z).
'''
from . import disassociate
return apply_disassociation_thm(self, idx, disassociate)
[docs]@prover
def compose(*expressions, **defaults_config):
'''
Returns [A and B and ...], the And operator applied to the
collection of given arguments, derived from each separately.
'''
from proveit._core_.expression.composite import (
ExprRange, composite_expression)
expressions = composite_expression(expressions)
if expressions.num_entries() == 0:
from proveit.logic.booleans.conjunction import \
empty_conjunction
return empty_conjunction
if expressions.is_double():
from . import and_if_both
return and_if_both.instantiate(
{A: expressions[0], B: expressions[1]}, auto_simplify=False)
elif expressions.contains_range():
# If there are ranges, prove these portions separately
# (grouped together) and then disassociate.
new_expressions = []
to_expand = []
# Group the ExprRanges and record their entry indices.
for _k, entry in enumerate(expressions):
if isinstance(entry, ExprRange):
new_expressions.append(And(entry))
to_expand.append(_k)
else:
new_expressions.append(entry)
# Prove the composition with ExprRanges grouped:
composed = compose(*new_expressions)
# Disassociate each ExprRange in reverse order so we don't
# have to update indices.
for _idx in reversed(to_expand):
composed = composed.disassociate(_idx)
return composed
else:
from . import and_if_all
_m = expressions.num_elements()
return and_if_all.instantiate({m: _m, A: expressions}, auto_simplify=False)