Forall

class proveit.logic.Forall(instance_param_or_params, instance_expr, *, domain=None, domains=None, condition=None, conditions=None, styles=None, _lambda_map=None)[source]

Bases: proveit.OperationOverInstances

Attributes Summary

known_instance_maps

Methods Summary

bundle(self[, num_levels])

Given a nested forall, derive an equivalent form in which a

bundle_equality(self[, num_levels])

Given a nested forall, equate it with an equivalent form in

conclude(self, \*\*defaults_config)

If the instance expression, or some instance expression of

conclude_by_cases(self, \*\*defaults_config)

Conclude this forall statement from an “unfolded” version

conclude_via_domain_inclusion(self, …)

Conclude this forall statement from a similar forall statement

conclude_via_generalization(self, …)

Conclude this universal quantification by proving the instance

deduce_in_bool(self, \*\*defaults_config)

Attempt to deduce, then return, that this forall expression

instantiate(self[, repl_map])

First attempt to prove that this Forall statement is true under

shallow_simplification(self, \*[, must_evaluate])

From this forall statement, evaluate it to TRUE or FALSE if

shallow_simplified(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘shallow_simplification’.

side_effects(self, judgment)

Side-effect derivations to attempt automatically for this forall operation.

unbundle(self[, num_param_entries])

From a nested forall, derive an equivalent form in which the

unbundle_equality(self[, num_param_entries])

From a nested forall, equate it with an equivalent form in

unfold(self, \*\*defaults_config)

From this forall statement, derive an “unfolded” version

Attributes Documentation

known_instance_maps = {(x, y) -> (y = x): {|- forall_{x, y | x = y} (y = x)}, A -> A: {|- forall_{A in BOOLEAN | [not](A) => FALSE} A, |- forall_{A in BOOLEAN | A != FALSE} A, |- forall_{A | not(not(A))} A, |- forall_{A | A = TRUE} A}, A -> (A != TRUE): {|- forall_{A | A => FALSE} (A != TRUE), |- forall_{A | not(A)} (A != TRUE)}, (x, y) -> (y != x): {|- forall_{x, y | x != y} (y != x)}, x -> (x = x): {|- forall_{x} (x = x)}, A -> (A in BOOLEAN): {|- forall_{A | [not](A) in BOOLEAN} (A in BOOLEAN), |- forall_{A | not(A)} (A in BOOLEAN), |- forall_{A | A} (A in BOOLEAN), |- forall_{A | (A = TRUE) or (A = FALSE)} (A in BOOLEAN)}, A -> (A or not(A)): {|- forall_{A in BOOLEAN} (A or not(A))}, A -> ((A = TRUE) or (A = FALSE)): {|- forall_{A in BOOLEAN} ((A = TRUE) or (A = FALSE))}, (x, y) -> not(x = y): {|- forall_{x, y | x != y} not(x = y)}, A -> (A = FALSE): {|- forall_{A | [not](A)} (A = FALSE)}, A -> not(A): {|- forall_{A in BOOLEAN | A => FALSE} [not](A), |- forall_{A | A = FALSE} not(A)}, (x, y) -> (x != y): {|- forall_{a, b in Real | a < b} (a != b), |- forall_{x, y | not(x = y)} (x != y)}, (A, B) -> (A subset_eq B): {|- forall_{A, B | A proper_subset B} (A subset_eq B)}, (A, B) -> [forall_{x in A} (x in B)]: {|- forall_{A, B | A subset_eq B} [forall_{x in A} (x in B)], |- forall_{A, B | A proper_subset B} [forall_{x in A} (x in B)]}, n -> (n >= 0): {|- forall_{x in RealNonNeg} (x >= 0), |- forall_{n in Natural} (n >= 0), |- forall_{q in RationalNonNeg} (q >= 0)}, (x, y) -> (x <= y): {|- forall_{x, y | x < y} (x <= y)}, n -> (n >= 1): {|- forall_{n in NaturalPos} (n >= 1)}, a -> (a != 0): {|- forall_{n in NaturalPos} (n != 0), |- forall_{a in IntegerNonZero} (a != 0), |- forall_{q in RationalNonZero} (q != 0), |- forall_{x in RealNonZero} (x != 0), |- forall_{x in ComplexNonZero} (x != 0)}, q -> (q > 0): {|- forall_{x in RealPos} (x > 0), |- forall_{q in RationalPos} (q > 0)}}

Methods Documentation

bundle(self, num_levels=2, \*\*defaults_config)[source]

Given a nested forall, derive an equivalent form in which a given number of nested levels is bundled together.

For example,

orall_{x, y | Q(x, y)} orall_{z | R(z)} P(x, y, z)

can become

orall_{x, y, z | Q(x, y), R(z)} P(x, y, z)

via bundle with num_levels=2.

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

bundle_equality(self, num_levels=2, \*\*defaults_config)[source]

Given a nested forall, equate it with an equivalent form in which a given number of nested levels is bundled together.

For example,

orall_{x, y | Q(x, y)} orall_{z | R(z)} P(x, y, z)

can be equated with

orall_{x, y, z | Q(x, y), R(z)} P(x, y, z)

via bundle with num_levels=2.

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

conclude(self, \*\*defaults_config)[source]

If the instance expression, or some instance expression of nested universal quantifiers, is known to be true, conclude via generalization. Otherwise, if the domain has a ‘fold_forall’ method, attempt to conclude this Forall statement via ‘conclude_by_cases’.

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

conclude_by_cases(self, \*\*defaults_config)[source]

Conclude this forall statement from an “unfolded” version dependent upon the domain of the forall, calling prove_by_cases on the domain. For example, conclude forall_{A in BOOLEANS} P(A) from P(TRUE) and P(FALSE).

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

conclude_via_domain_inclusion(self, superset_domain, \*\*defaults_config)[source]

Conclude this forall statement from a similar forall statement over a broader domain. For example, conclude forall_{x in B} P(x) from forall_{x in A} P(x) given A superset_eq B.

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

conclude_via_generalization(self, \*\*defaults_config)[source]

Conclude this universal quantification by proving the instance expression with assumptions that include the conditions of the quantification and then performing generalization step(s). This will delve into any number of nested universal quantifications if necessary. With automation turned on, we will attempt to prove the innermost instance expression, under appropriate assumptions, via automation if necessary.

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

deduce_in_bool(self, \*\*defaults_config)[source]

Attempt to deduce, then return, that this forall expression is in the set of BOOLEANS, as all forall expressions are (they are taken to be false when not true).

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

instantiate(self, repl_map=None, \*\*defaults_config)[source]

First attempt to prove that this Forall statement is true under the assumptions, and then call instantiate on the Judgment.

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

shallow_simplification(self, \*, must_evaluate=False, \*\*defaults_config)[source]

From this forall statement, evaluate it to TRUE or FALSE if possible by calling the domain’s forall_evaluation method

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

shallow_simplified(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘shallow_simplification’.

side_effects(self, judgment)[source]

Side-effect derivations to attempt automatically for this forall operation.

unbundle(self, num_param_entries=(1, ), \*\*defaults_config)[source]

From a nested forall, derive an equivalent form in which the parameter entries are split in number according to ‘num_param_entries’.

For example,

orall_{x, y, z | Q(x, y), R(z)} P(x, y, z)

can become

orall_{x, y | Q(x, y)} orall_{z | R(z)} P(x, y, z)

via bundle with num_param_entries=(2, 1) or num_param_entries=(2,) – the last number can be implied by the remaining number of parameters.

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

unbundle_equality(self, num_param_entries=(1, ), \*\*defaults_config)[source]

From a nested forall, equate it with an equivalent form in which the parameter entries are split in number according to ‘num_param_entries’.

For example,

orall_{x, y, z | Q(x, y), R(z)} P(x, y, z)

can equate with

orall_{x, y | Q(x, y)} orall_{z | R(z)} P(x, y, z)

via bundle with num_param_entries=(2, 1) or num_param_entries=(2,) – the last number can be implied by the remaining number of parameters.

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

unfold(self, \*\*defaults_config)[source]

From this forall statement, derive an “unfolded” version dependent upon the domain of the forall, calling unfold_forall on the condition. For example, from forall_{A in BOOLEANS} P(A), derives P(TRUE) and P(FALSE).

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