Theorem

class proveit.Theorem(expr, theory, name, *, _proven_truth=None, _requirements=None, _marked_req_indices=None)

Bases: proveit.Proof

Attributes Summary

all_theorems

Methods Summary

all_dependents(self)	Returns the set of theorems that are known to depend upon this theorem directly or indirectly.
all_requirements(self, \*[, sort_key])	Returns the axioms that are required (directly or indirectly) by the theorem.
direct_dependents(self)	Returns the theorems that depend directly upon this axioms.
get_link(self)	Return the HTML link to the theorem proof file.
get_presumptions_and_exclusions(self)	Return the set of theorems and theories that are explicitly presumed by this theorem, and a set of exclusions (e.g., you could presume the proveit.logic theory but exclude proveit.logic.equality).
has_proof(self)	Returns true if and only if this theorem has a recorded proof.
is_conjecture(self)	A “Theorem” that is not fully proven is a “conjecture”.
is_fully_proven(self)	Returns true if and only if this theorem is fully proven (it has a recorded proof and all dependent theorems are fully proven, all the way to axioms which don’t require proofs).
remove_proof(self)	Remove the proof for the given theorem and all obsolete dependency links.
step_type(self)
theorem_name_and_containing_theories(self)	Yields all containing theory names and the full theorem name.
update_usability()
used_theorems(self)	Returns the set of names of axioms that are used directly (not via other theorems) in this proof.

Attributes Documentation

all_theorems = [proveit.logic.equality.equals_reversal, proveit.logic.booleans.in_bool_if_true, proveit.logic.booleans.unfold_is_bool, proveit.logic.booleans.fold_is_bool, proveit.logic.booleans.unfold_is_bool_explicit, proveit.logic.booleans.negation.negation_intro, proveit.logic.booleans.negation.double_negation_elim, proveit.logic.booleans.negation.not_false, proveit.logic.booleans.implication.true_implies_true, proveit.logic.booleans.implication.false_implies_true, proveit.logic.booleans.implication.not_true_via_contradiction, proveit.logic.booleans.implication.false_implies_false, proveit.logic.equality.not_equals_symmetry, proveit.logic.booleans.from_not_false, proveit.logic.equality.unfold_not_equals, proveit.logic.equality.fold_not_equals, proveit.logic.booleans.true_eq_true, proveit.logic.booleans.false_eq_false, proveit.logic.booleans.true_not_false, proveit.logic.booleans.true_is_bool, proveit.logic.booleans.false_is_bool, proveit.logic.sets.inclusion.relax_proper_subset, proveit.numbers.number_sets.integers.zero_set_within_int, proveit.numbers.number_sets.integers.zero_set_within_nonpos_int, proveit.numbers.number_sets.natural_numbers.zero_set_within_nat, proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat, proveit.numbers.number_sets.integers.nat_within_int, proveit.numbers.number_sets.integers.nat_pos_within_int, proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int, proveit.numbers.number_sets.integers.nonzero_int_within_int, proveit.numbers.number_sets.integers.neg_int_within_int, proveit.numbers.number_sets.integers.neg_int_within_nonzero_int, proveit.numbers.number_sets.integers.neg_int_within_nonpos_int, proveit.numbers.number_sets.integers.nonpos_int_within_int, proveit.numbers.number_sets.rational_numbers.zero_set_within_rational, proveit.numbers.number_sets.rational_numbers.zero_set_within_rational_nonneg, proveit.numbers.number_sets.rational_numbers.zero_set_within_rational_nonpos, proveit.numbers.number_sets.rational_numbers.nat_within_rational, proveit.numbers.number_sets.rational_numbers.int_within_rational, proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero, proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg, proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos, proveit.numbers.number_sets.rational_numbers.neg_int_within_rational_neg, proveit.numbers.number_sets.rational_numbers.nonpos_int_within_rational_nonpos, proveit.numbers.number_sets.rational_numbers.rational_nonzero_within_rational, proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational, proveit.numbers.number_sets.rational_numbers.rational_neg_within_rational, proveit.numbers.number_sets.rational_numbers.rational_nonneg_within_rational, proveit.numbers.number_sets.rational_numbers.rational_nonpos_within_rational, proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero, proveit.numbers.number_sets.rational_numbers.rational_neg_within_rational_nonzero, proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonneg, proveit.numbers.number_sets.rational_numbers.rational_neg_within_rational_nonpos, proveit.numbers.number_sets.real_numbers.zero_set_within_real, proveit.numbers.number_sets.real_numbers.zero_set_within_real_nonneg, proveit.numbers.number_sets.real_numbers.zero_set_within_real_nonpos, proveit.numbers.number_sets.real_numbers.int_within_real, proveit.numbers.number_sets.real_numbers.nat_within_real, proveit.numbers.number_sets.real_numbers.nat_pos_within_real, proveit.numbers.number_sets.real_numbers.nat_pos_within_real_pos, proveit.numbers.number_sets.real_numbers.nat_within_real_nonneg, proveit.numbers.number_sets.real_numbers.nat_pos_within_real_nonneg, proveit.numbers.number_sets.real_numbers.nonzero_int_within_real_nonzero, proveit.numbers.number_sets.real_numbers.neg_int_within_real_neg, proveit.numbers.number_sets.real_numbers.nonpos_int_within_real_nonpos, proveit.numbers.number_sets.real_numbers.rational_within_real, proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero, proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos, proveit.numbers.number_sets.real_numbers.rational_neg_within_real_neg, proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg, proveit.numbers.number_sets.real_numbers.rational_nonpos_within_real_nonpos, proveit.numbers.number_sets.real_numbers.real_pos_within_real, proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero, proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonneg, proveit.numbers.number_sets.real_numbers.real_neg_within_real, proveit.numbers.number_sets.real_numbers.real_neg_within_real_nonzero, proveit.numbers.number_sets.real_numbers.real_neg_within_real_nonpos, proveit.numbers.number_sets.real_numbers.real_nonneg_within_real, proveit.numbers.number_sets.real_numbers.real_nonpos_within_real, proveit.numbers.number_sets.real_numbers.real_nonzero_within_real, proveit.numbers.number_sets.complex_numbers.zero_set_within_complex, proveit.numbers.number_sets.complex_numbers.nat_within_complex, proveit.numbers.number_sets.complex_numbers.int_within_complex, proveit.numbers.number_sets.complex_numbers.int_nonpos_within_complex, proveit.numbers.number_sets.complex_numbers.int_neg_within_complex_nonzero, proveit.numbers.number_sets.complex_numbers.nat_pos_within_complex_nonzero, proveit.numbers.number_sets.complex_numbers.int_nonzero_within_complex_nonzero, proveit.numbers.number_sets.complex_numbers.rational_within_complex, proveit.numbers.number_sets.complex_numbers.rational_nonneg_within_complex, proveit.numbers.number_sets.complex_numbers.rational_nonpos_within_complex, proveit.numbers.number_sets.complex_numbers.rational_pos_within_complex_nonzero, proveit.numbers.number_sets.complex_numbers.rational_neg_within_complex_nonzero, proveit.numbers.number_sets.complex_numbers.rational_nonzero_within_complex_nonzero, proveit.numbers.number_sets.complex_numbers.real_within_complex, proveit.numbers.number_sets.complex_numbers.real_nonneg_within_complex, proveit.numbers.number_sets.complex_numbers.real_nonpos_within_complex, proveit.numbers.number_sets.complex_numbers.real_pos_within_complex_nonzero, proveit.numbers.number_sets.complex_numbers.real_neg_within_complex_nonzero, proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero, proveit.numbers.number_sets.complex_numbers.complex_nonzero_within_complex, proveit.numbers.number_sets.natural_numbers.natural_lower_bound, proveit.numbers.ordering.not_less_from_less_eq, proveit.logic.sets.inclusion.superset_membership_from_proper_subset, proveit.numbers.number_sets.rational_numbers.nonneg_if_in_rational_nonneg, proveit.numbers.number_sets.real_numbers.nonneg_if_in_real_nonneg, proveit.numbers.numerals.decimals.nat1, proveit.numbers.numerals.decimals.nat2, proveit.numbers.numerals.decimals.nat3, proveit.numbers.numerals.decimals.nat4, proveit.numbers.numerals.decimals.nat5, proveit.numbers.numerals.decimals.nat6, proveit.numbers.numerals.decimals.nat7, proveit.numbers.numerals.decimals.nat8, proveit.numbers.numerals.decimals.nat9, proveit.numbers.number_sets.integers.nonpos_if_in_nonpos_int, proveit.numbers.number_sets.rational_numbers.nonpos_if_in_rational_nonpos, proveit.numbers.number_sets.real_numbers.nonpos_if_in_real_nonpos, proveit.numbers.number_sets.integers.zero_is_nonpos_int, proveit.logic.sets.inclusion.unfold_subset_eq, proveit.numbers.ordering.less_eq_from_not_less, proveit.numbers.number_sets.integers.zero_is_int, proveit.numbers.number_sets.rational_numbers.zero_is_rational, proveit.numbers.number_sets.rational_numbers.zero_is_nonneg_rational, proveit.numbers.number_sets.rational_numbers.zero_is_nonpos_rational, proveit.numbers.number_sets.real_numbers.zero_is_real, proveit.numbers.number_sets.real_numbers.zero_is_nonneg_real, proveit.numbers.number_sets.real_numbers.zero_is_nonpos_real, proveit.numbers.number_sets.complex_numbers.zero_is_complex, proveit.numbers.ordering.relax_less, proveit.numbers.ordering.less_is_not_eq, proveit.numbers.ordering.not_less_eq_from_less, proveit.numbers.ordering.less_from_not_less_eq, proveit.numbers.numerals.decimals.less_0_1, proveit.numbers.numerals.decimals.less_1_2, proveit.numbers.numerals.decimals.less_2_3, proveit.numbers.numerals.decimals.less_3_4, proveit.numbers.numerals.decimals.less_4_5, proveit.numbers.numerals.decimals.less_5_6, proveit.numbers.numerals.decimals.less_6_7, proveit.numbers.numerals.decimals.less_7_8, proveit.numbers.numerals.decimals.less_8_9, proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound, proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos, proveit.numbers.number_sets.integers.nonzero_if_in_nonzero_int, proveit.numbers.number_sets.rational_numbers.nonzero_if_in_rational_nonzero, proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero, proveit.numbers.number_sets.complex_numbers.nonzero_if_in_complex_nonzero, proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos, proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos, proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos, proveit.numbers.numerals.decimals.posnat1, proveit.numbers.numerals.decimals.posnat2, proveit.numbers.numerals.decimals.posnat3, proveit.numbers.numerals.decimals.posnat4, proveit.numbers.numerals.decimals.posnat5, proveit.numbers.numerals.decimals.posnat6, proveit.numbers.numerals.decimals.posnat7, proveit.numbers.numerals.decimals.posnat8, proveit.numbers.numerals.decimals.posnat9, proveit.numbers.negation.negated_zero, proveit.numbers.number_sets.real_numbers.e_is_real_pos, proveit.numbers.number_sets.real_numbers.pi_is_real_pos, proveit.numbers.number_sets.complex_numbers.i_is_complex, proveit.numbers.number_sets.complex_numbers.i_is_complex_nonzero, proveit.abstract_algebra.fields.rational_field, proveit.abstract_algebra.fields.real_field, proveit.abstract_algebra.fields.complex_field]

Methods Documentation

all_dependents(self)

Returns the set of theorems that are known to depend upon this theorem directly or indirectly.

all_requirements(self, \*, sort_key=None)

Returns the axioms that are required (directly or indirectly) by the theorem. Also, return the set of “dead-end” theorems that are required (directly or indirectly). A “dead-end” theorem is either unproven or has an expression that matches one in the optionally provided dead_end_theorem_exprs. Conservative definitions that are not logically necessary for the proof are extracted from these sets and returned on their own.

Returns the list of axioms, “dead-end” theorems, and conservative definitions as a tuple. These will be sorted according to sort_key with the exception that a conservatively defined literal will not appear before its definition in the list of conservative definitions.

direct_dependents(self)

Returns the theorems that depend directly upon this axioms.

get_link(self)

Return the HTML link to the theorem proof file.

get_presumptions_and_exclusions(self)

Return the set of theorems and theories that are explicitly presumed by this theorem, and a set of exclusions (e.g., you could presume the proveit.logic theory but exclude proveit.logic.equality).

has_proof(self)

Returns true if and only if this theorem has a recorded proof.

is_conjecture(self)

A “Theorem” that is not fully proven is a “conjecture”.

is_fully_proven(self)

Returns true if and only if this theorem is fully proven (it has a recorded proof and all dependent theorems are fully proven, all the way to axioms which don’t require proofs).

remove_proof(self)

Remove the proof for the given theorem and all obsolete dependency links.

step_type(self)

theorem_name_and_containing_theories(self)

Yields all containing theory names and the full theorem name.

static update_usability()

used_theorems(self)

Returns the set of names of axioms that are used directly (not via other theorems) in this proof.