bend-mathlib
Search uses release 0.8.1.0 · 1,126 definitions
Definitions (1,126)
- law op_assoc4Four-way reassociation from associativity alone.
- law op_left_commLeft commutation from associativity and commutativity.
- law op_right_commRight commutation from associativity and commutativity.
- law op_fourMiddle-four interchange from associativity and commutativity.
- law op_comm3Three-way commutation from commutativity alone.
- def internal_nat_add_assoc
- def internal_nat_add_comm
- def internal_nat_zero_add
- def internal_nat_mul
- def internal_nat_mul_assoc
- def internal_nat_mul_comm
- def internal_bool_and_assoc
- def internal_bool_and_comm
- def internal_bool_or_assoc
- def internal_bool_or_comm
- def internal_list_nat_append_assoc
- law nat_add_left_commNat addition is left-commutative (the same statement as MNat.add_left_comm).
- law nat_add_right_commNat addition is right-commutative (the same statement as MNat.add_right_comm).
- law nat_add_fourNat addition's middle-four interchange (the same statement as MNat.add_add_add_comm).
- law nat_mul_left_commNat multiplication is left-commutative (the same statement as MNat.mul_left_comm).
- law nat_mul_right_commNat multiplication is right-commutative (the same statement as MNat.mul_right_comm).
- law nat_mul_fourNat multiplication's middle-four interchange (the same statement as MNat.mul_mul_mul_comm).
- law bool_and_left_commBool and is left-commutative.
- law bool_and_right_commBool and is right-commutative.
- law bool_or_left_commBool or is left-commutative.
- law bool_or_right_commBool or is right-commutative.
- law list_nat_append_assoc4Four-way reassociation for List append over Nat.
- def internal_foldl_foldr
- law foldl_op_eq_foldr_opFolding left equals folding right for an associative, commutative operation with a left identity (foldl_eq_foldr needs no identity).
- def internal_nat_foldl_op_eq_foldr_opA Nat call: --verdict takes a ~ constant's model from a call of its law (PLAN F38).
- def internal_foldl_assoc
- def internal_foldl_eq_foldr
- law foldl_eq_foldrFolding left equals folding right for an associative, commutative operation (Mathlib's List.foldl_eq_foldr).
- law op_assoc4_symFour-way reassociation from associativity alone, reversed to rewrite toward the simple side.
- law op_left_comm_symLeft commutation from associativity and commutativity, reversed to rewrite toward the simple side.
- law op_right_comm_symRight commutation from associativity and commutativity, reversed to rewrite toward the simple side.
- law op_four_symMiddle-four interchange from associativity and commutativity, reversed to rewrite toward the simple side.
- law op_comm3_symThree-way commutation from commutativity alone, reversed to rewrite toward the simple side.
- law nat_add_left_comm_symNat addition is left-commutative (the same statement as MNat.add_left_comm), reversed to rewrite toward the simple side.
- law nat_add_right_comm_symNat addition is right-commutative (the same statement as MNat.add_right_comm), reversed to rewrite toward the simple side.
- law nat_add_four_symNat addition's middle-four interchange (the same statement as MNat.add_add_add_comm), reversed to rewrite toward the simple side.
- law nat_mul_left_comm_symNat multiplication is left-commutative (the same statement as MNat.mul_left_comm), reversed to rewrite toward the simple side.
- law nat_mul_right_comm_symNat multiplication is right-commutative (the same statement as MNat.mul_right_comm), reversed to rewrite toward the simple side.
- law nat_mul_four_symNat multiplication's middle-four interchange (the same statement as MNat.mul_mul_mul_comm), reversed to rewrite toward the simple side.
- law bool_and_left_comm_symBool and is left-commutative, reversed to rewrite toward the simple side.
- law bool_and_right_comm_symBool and is right-commutative, reversed to rewrite toward the simple side.
- law bool_or_left_comm_symBool or is left-commutative, reversed to rewrite toward the simple side.
- law bool_or_right_comm_symBool or is right-commutative, reversed to rewrite toward the simple side.
- law list_nat_append_assoc4_symFour-way reassociation for List append over Nat, reversed to rewrite toward the simple side.
- law foldl_op_eq_foldr_op_symFolding left equals folding right for an associative, commutative operation with a left identity (foldl_eq_foldr needs no identity), reversed to rewrite toward the simple side.
- law foldl_eq_foldr_symFolding left equals folding right for an associative, commutative operation (Mathlib's List.foldl_eq_foldr), reversed to rewrite toward the simple side.
- def internal_nat_foldl_op_eq_foldr_op_symCalls of the twins, as the calls above the generated section make of their laws (PLAN F38).
- law not_notNegating a boolean twice gives it back.
- law and_commBoolean and is commutative.
- law or_commBoolean or is commutative.
- law and_assocBoolean and is associative.
- law or_assocBoolean or is associative.
- law and_trueTrue is a right identity for and: a and true is a.
- law true_andTrue is a left identity for and: true and a is a.
- law and_falseFalse absorbs and on the right: a and false is false.
- law false_andFalse absorbs and on the left: false and a is false.
- law or_falseFalse is a right identity for or: a or false is a.
- law false_orFalse is a left identity for or: false or a is a.
- law or_trueTrue absorbs or on the right: a or true is true.
- law true_orTrue absorbs or on the left: true or a is true.
- law de_morgan_andDe Morgan: not (a and b) is (not a) or (not b).
- law de_morgan_orDe Morgan: not (a or b) is (not a) and (not b).
- def internal_true_ne_false
- law true_ne_falseTrue and False are different booleans.
- law and_selfAnd with itself: a and a is a.
- law or_selfOr with itself: a or a is a.
- law and_not_selfA boolean and its negation are never both true: a and (not a) is false.
- law or_not_selfA boolean or its negation is always true: a or (not a) is true.
- law and_or_distrib_leftAnd distributes over or: a and (b or c) is (a and b) or (a and c).
- law or_and_distrib_leftOr distributes over and: a or (b and c) is (a or b) and (a or c).
- law and_or_absorbAbsorption: a and (a or b) is a.
- law or_and_absorbAbsorption: a or (a and b) is a.
- law xor_commExclusive or is commutative.
- law xor_assocExclusive or is associative.
- law xor_selfA boolean xor itself is false.
- law xor_falseFalse is an identity for xor: a xor false is a.
- law xor_trueXor with true negates: a xor true is not a.
- law not_injNegation is injective: not a = not b implies a = b.
- law eq_true_of_ne_falseA boolean that is not false is true.
- def internal_false_ne_true
- law cmp_reflComparing a boolean with itself gives EQ.
- law eq_of_cmp_eqTwo booleans that compare EQ are equal.
- law false_ne_trueFalse and True are different booleans, the other way round.
- law eq_true_of_and_leftIf a and b is true then a is true.
- law eq_true_of_and_rightIf a and b is true then b is true.
- law and_eq_trueIf a and b are both true then a and b is true.
- law eq_true_of_or_eq_false_rightIf a or b is true and b is false then a is true.
- law eq_true_of_or_eq_false_leftIf a or b is true and a is false then b is true.
- law eq_false_of_not_eq_trueIf not b is true then b is false.
- law not_not_symNegating a boolean twice gives it back, reversed to rewrite toward the simple side.
- law and_comm_symBoolean and is commutative, reversed to rewrite toward the simple side.
- law or_comm_symBoolean or is commutative, reversed to rewrite toward the simple side.
- law and_assoc_symBoolean and is associative, reversed to rewrite toward the simple side.
- law or_assoc_symBoolean or is associative, reversed to rewrite toward the simple side.
- law and_true_symTrue is a right identity for and: a and true is a, reversed to rewrite toward the simple side.