bend-mathlib
Search uses release 0.8.1.0 · 1,126 definitions
Definitions (1,126)
- law reverse_cons_symReversing a cons puts its head last: reverse (x :: xs) = reverse xs ++ [x], reversed to rewrite toward the simple side.
- law take_succ_symTaking n + 1 elements of a cons keeps its head and takes n from its tail, reversed to rewrite toward the simple side.
- law drop_succ_symDropping n + 1 elements of a cons drops its head and n from its tail, reversed to rewrite toward the simple side.
- law maybe_pure_bindLeft identity: binding a pure value applies the function.
- law maybe_bind_pureRight identity: binding pure is the identity.
- law maybe_bind_assocBind is associative.
- law maybe_map_pureMapping a pure value is pure of the mapped value.
- law maybe_map_composeMapping a composition maps the composition.
- law maybe_map_idMapping the identity gives the value back.
- law maybe_bind_noneBinding a function that always fails gives None.
- law maybe_map_eq_bindMapping is binding the function followed by pure.
- law maybe_is_some_mapMapping keeps whether a value is present.
- law maybe_is_none_mapMapping keeps whether a value is absent.
- law maybe_default_mapThe default of a map, with the mapped default, is the mapped default of the original.
- law maybe_or_noneNone is a right identity for or.
- law maybe_or_assocOr is associative.
- law maybe_bind_mapBinding after a map binds the composition.
- law maybe_map_bindMapping after a bind maps inside the bound function.
- law maybe_pure_bind_symLeft identity: binding a pure value applies the function, reversed to rewrite toward the simple side.
- law maybe_bind_pure_symRight identity: binding pure is the identity, reversed to rewrite toward the simple side.
- law maybe_bind_assoc_symBind is associative, reversed to rewrite toward the simple side.
- law maybe_map_pure_symMapping a pure value is pure of the mapped value, reversed to rewrite toward the simple side.
- law maybe_map_compose_symMapping a composition maps the composition, reversed to rewrite toward the simple side.
- law maybe_map_id_symMapping the identity gives the value back, reversed to rewrite toward the simple side.
- law maybe_bind_none_symBinding a function that always fails gives None, reversed to rewrite toward the simple side.
- law maybe_map_eq_bind_symMapping is binding the function followed by pure, reversed to rewrite toward the simple side.
- law maybe_is_some_map_symMapping keeps whether a value is present, reversed to rewrite toward the simple side.
- law maybe_is_none_map_symMapping keeps whether a value is absent, reversed to rewrite toward the simple side.
- law maybe_default_map_symThe default of a map, with the mapped default, is the mapped default of the original, reversed to rewrite toward the simple side.
- law maybe_or_none_symNone is a right identity for or, reversed to rewrite toward the simple side.
- law maybe_or_assoc_symOr is associative, reversed to rewrite toward the simple side.
- law maybe_bind_map_symBinding after a map binds the composition, reversed to rewrite toward the simple side.
- law maybe_map_bind_symMapping after a bind maps inside the bound function, reversed to rewrite toward the simple side.
- law add_zeroZero is a right identity for addition: x + 0 = x.
- law zero_addZero is a left identity for addition: 0 + x = x.
- law add_succAdding a successor on the right: n + (m + 1) = (n + m) + 1.
- law succ_addAdding a successor on the left: (n + 1) + m = (n + m) + 1.
- law add_commAddition is commutative: n + m = m + n.
- law add_assocAddition is associative: (a + b) + c = a + (b + c).
- law add_left_commLeft commutativity of addition: a + (b + c) = b + (a + c).
- law add_right_commRight commutativity of addition: (a + b) + c = (a + c) + b.
- law add_add_add_commFour-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d).
- def internal_pred
- law succ_injThe successor function is injective: a + 1 = b + 1 implies a = b.
- def internal_zero_ne_succ
- law zero_ne_succZero is not a successor.
- def internal_succ_ne_zero
- law succ_ne_zeroA successor is not zero.
- law add_left_cancelAddition cancels on the left: a + b = a + c implies b = c.
- law add_right_cancelAddition cancels on the right: a + b = c + b implies a = c.
- law mul_zeroZero absorbs multiplication on the right: x * 0 = 0.
- law zero_mulZero absorbs multiplication on the left: 0 * x = 0.
- law mul_oneOne is a right identity for multiplication: x * 1 = x.
- law one_mulOne is a left identity for multiplication: 1 * x = x.
- law mul_succMultiplying by a successor on the right: n * (m + 1) = n * m + n.
- law succ_mulMultiplying by a successor on the left: (n + 1) * m = n * m + m.
- law mul_commMultiplication is commutative: n * m = m * n.
- law add_mulMultiplication distributes over addition on the right: (a + b) * c = a * c + b * c.
- law mul_addMultiplication distributes over addition on the left: a * (b + c) = a * b + a * c.
- law mul_assocMultiplication is associative: (a * b) * c = a * (b * c).
- def leThe order a <= b on naturals, as a reusable proposition.
- def ltThe strict order a < b on naturals, as a reusable proposition.
- def geThe order a >= b on naturals, as a reusable proposition.
- def gtThe strict order a > b on naturals, as a reusable proposition.
- def internal_false_ne_true
- law le_reflEvery natural is at most itself: a <= a.
- law zero_leZero is at most every natural: 0 <= b.
- law le_succEvery natural is at most its successor: n <= n + 1.
- law le_add_rightAdding on the right never decreases a natural: n <= n + k.
- law le_transThe order is transitive: a <= b and b <= c imply a <= c.
- law le_antisymmThe order is antisymmetric: a <= b and b <= a imply a = b.
- law le_totalThe order is total: a <= b or b <= a.
- law le_total_dThe order is total, as a reusable sum: a <= b or b <= a.
- law lt_irreflNo natural is less than itself.
- law lt_transThe strict order is transitive: a < b and b < c imply a < c.
- law le_of_ltA strict inequality implies the weak one: a < b implies a <= b.
- law le_of_geFlipping a >= b gives b <= a.
- law ge_of_leFlipping b <= a gives a >= b.
- law lt_of_gtFlipping a > b gives b < a.
- law gt_of_ltFlipping b < a gives a > b.
- law sub_zeroSubtracting zero changes nothing: n - 0 = n.
- law zero_subTruncated subtraction from zero is zero: 0 - n = 0.
- law sub_selfA natural minus itself is zero: n - n = 0.
- law succ_sub_succSubtracting successors: (n + 1) - (m + 1) = n - m.
- law add_sub_cancelAdding then subtracting m cancels: (n + m) - m = n.
- law add_sub_cancel_leftAdding then subtracting n cancels: (n + m) - n = m.
- law sub_add_cancelIf m <= n, subtracting and adding m back gives n: (n - m) + m = n.
- law sub_subSubtracting twice is subtracting the sum: (n - m) - k = n - (m + k).
- law sub_leTruncated subtraction never increases: n - m <= n.
- def internal_div_true_ne_false
- def internal_div_add_zero_r
- def internal_div_le_refl
- def internal_div_zero_le
- def internal_div_block_start
- def internal_div_block_step
- def internal_div_go_eq
- law div_mod_eqThe division equation, for a positive divisor 1 + b: (a / (1 + b)) * (1 + b) + a % (1 + b) = a.
- def internal_div_wit_succ
- def internal_div_le_wit
- def internal_div_go_small