Implies

class proveit.logic.Implies(antecedent, consequent, *, styles=None)

Bases: proveit.TransitiveRelation

Attributes Summary

known_left_sides
known_right_sides

Methods Summary

StrongRelationClass()	The Strong and Weak form of transitive relations are the same for implication.
WeakRelationClass()	The Strong and Weak form of transitive relations are the same for implication.
apply_transitivity(self, other_impl, …)	From A => B (self) and a given B => C (other_impl), derive and return A => C.
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.
conclude_negation(self, \*\*defaults_config)	Try to conclude Not(A => B) because A is true and B is false.
conclude_self_implication(self, …)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
conclude_via_double_negation(self, …)	From A => B return A => Not(Not(B)).
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:
deduce_in_bool(self, \*\*defaults_config)	Attempt to deduce, then return, that this implication expression is in the set of BOOLEANS.
deduce_negated_left_impl(self, …)	From Not(B => A) derive and return Not(A <=> B).
deduce_negated_reflex(self, \*\*defaults_config)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
deduce_negated_right_impl(self, …)	From Not(A => B) derive and return Not(A <=> B).
deny_antecedent(self, \*\*defaults_config)	From A => B, derive and return Not(A) assuming Not(B).
derive_consequent(self, \*\*defaults_config)	From A => B derive and return B assuming A.
derive_iff(self, \*\*defaults_config)	From A => B derive and return A <=> B assuming B => A.
derive_via_contradiction(self, …)	From (Not(A) => FALSE), derive and return A assuming A in Boolean.
evaluation(self, \*\*defaults_config)	If possible, return a Judgment of this expression equal to an irreducible value.
generalize(self, forall_vars[, domain, …])	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.
negation_side_effects(self, judgment)	Side-effect derivations to attempt automatically when an implication is negated.
side_effects(self, judgment)	Yield the TransitiveRelation side-effects (which also records known_left_sides nd known_right_sides).

Attributes Documentation

known_left_sides = {TRUE: OrderedSet([|- TRUE => TRUE]), FALSE: OrderedSet([|- FALSE => TRUE, |- FALSE => FALSE]), [not](_a): OrderedSet([{[not](_a) => FALSE} |- [not](_a) => FALSE]), [not](A): OrderedSet([{[not](A) => FALSE} |- [not](A) => FALSE]), _a: OrderedSet([{_a => FALSE} |- _a => FALSE]), A: OrderedSet([{A => FALSE} |- A => FALSE])}

known_right_sides = {TRUE: OrderedSet([|- TRUE => TRUE, |- FALSE => TRUE]), FALSE: OrderedSet([|- FALSE => FALSE, {[not](_a) => FALSE} |- [not](_a) => FALSE, {[not](A) => FALSE} |- [not](A) => FALSE, {_a => FALSE} |- _a => FALSE, {A => FALSE} |- A => FALSE])}

Methods Documentation

static StrongRelationClass()

The Strong and Weak form of transitive relations are the same for implication.

static 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.

apply_transitivity(self, other_impl, \*\*defaults_config)

From A => B (self) and a given B => C (other_impl), derive and return A => C.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

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.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_negation(self, \*\*defaults_config)

Try to conclude Not(A => B) because A is true and B is false.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_self_implication(self, \*\*defaults_config)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_via_double_negation(self, \*\*defaults_config)

From A => B return A => Not(Not(B)). implemented by JML on 6/18/19

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

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}.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_in_bool(self, \*\*defaults_config)

Attempt to deduce, then return, that this implication expression is in the set of BOOLEANS.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_negated_left_impl(self, \*\*defaults_config)

From Not(B => A) derive and return Not(A <=> B). implemented by JML on 6/18/19

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_negated_reflex(self, \*\*defaults_config)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_negated_right_impl(self, \*\*defaults_config)

From Not(A => B) derive and return Not(A <=> B). implemented by JML on 6/18/19

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deny_antecedent(self, \*\*defaults_config)

From A => B, derive and return Not(A) assuming Not(B).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_consequent(self, \*\*defaults_config)

From A => B derive and return B assuming A.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_iff(self, \*\*defaults_config)

From A => B derive and return A <=> B assuming B => A.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_via_contradiction(self, \*\*defaults_config)

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.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

evaluation(self, \*\*defaults_config)

If possible, return a Judgment of this expression equal to an irreducible value. This Operation.evaluation version simplifies the operands and then calls shallow_simplification with must_evaluat=True.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘evaluated’ returns the right-hand side of ‘evaluation’. ‘evaluate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘evaluation’ for the inner expression.

generalize(self, forall_vars, domain=None, conditions=(), \*\*defaults_config)

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).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

negation_side_effects(self, judgment)

Side-effect derivations to attempt automatically when an implication is negated. implemented by JML on 6/17/19

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.