Forall

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

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 nested universal quantifiers, is known to be true, conclude via generalization.
conclude_by_cases(self, \*\*defaults_config)	Conclude this forall statement from an “unfolded” version dependent upon the domain of the forall, calling prove_by_cases on the domain.
conclude_via_domain_inclusion(self, …)	Conclude this forall statement from a similar forall statement over a broader domain.
deduce_in_bool(self, \*\*defaults_config)	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).
instantiate(self[, repl_map, …])	First attempt to prove that this Forall statement is true under the assumptions, and then call instantiate on the Judgment.
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 dependent upon the domain of the forall, calling unfold_forall on the condition.

Attributes Documentation

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

Methods Documentation

bundle(self, num_levels=2, \*\*defaults_config)

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)

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)

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)

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)

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.

deduce_in_bool(self, \*\*defaults_config)

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, \*, num_forall_eliminations=None, simplify_only_where_marked=False, markers_and_marked_expr=None, \*\*defaults_config)

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.

side_effects(self, judgment)

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

unbundle(self, num_param_entries=(1, ), \*\*defaults_config)

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)

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)

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.