~/bend-docscommunity

algebra.bend checks

raw source on the hub · import bend-mathlib@0.7.1.0/algebra.bend as Algebra

bend-mathlib/algebra.bend: abstract associativity/commutativity theorems and their Nat/Bool/List instances.

4 imports
import Base
import ./nat.bend as MNat
import ./bool.bend as MBool
import ./list.bend as MList

Laws

law op_assoc4 provedsource · line 8 · raw

@-A:Data -> @-op:(@_:A -> @_:A -> A) -> @-assoc:(@x:A -> @y:A -> @z:A -> {op(op(x, y), z) == op(x, op(y, z)) : A}) -> @+a:A -> @+b:A -> @+c:A -> @+d:A -> {op(op(op(a, b), c), d) == op(a, op(b, op(c, d))) : A}

Four-way reassociation from associativity alone.

law op_left_comm provedsource · line 23 · raw

@-A:Data -> @-op:(@_:A -> @_:A -> A) -> @-assoc:(@x:A -> @y:A -> @z:A -> {op(op(x, y), z) == op(x, op(y, z)) : A}) -> @-comm:(@x:A -> @y:A -> {op(x, y) == op(y, x) : A}) -> @+a:A -> @+b:A -> @+c:A -> {op(a, op(b, c)) == op(b, op(a, c)) : A}

Left commutation from associativity and commutativity.

law op_right_comm provedsource · line 39 · raw

@-A:Data -> @-op:(@_:A -> @_:A -> A) -> @-assoc:(@x:A -> @y:A -> @z:A -> {op(op(x, y), z) == op(x, op(y, z)) : A}) -> @-comm:(@x:A -> @y:A -> {op(x, y) == op(y, x) : A}) -> @+a:A -> @+b:A -> @+c:A -> {op(op(a, b), c) == op(op(a, c), b) : A}

Right commutation from associativity and commutativity.

law op_four provedsource · line 56 · raw

@-A:Data -> @-op:(@_:A -> @_:A -> A) -> @-assoc:(@x:A -> @y:A -> @z:A -> {op(op(x, y), z) == op(x, op(y, z)) : A}) -> @-comm:(@x:A -> @y:A -> {op(x, y) == op(y, x) : A}) -> @+a:A -> @+b:A -> @+c:A -> @+d:A -> {op(op(a, b), op(c, d)) == op(op(a, c), op(b, d)) : A}

Middle-four interchange from associativity and commutativity.

law op_comm3 provedsource · line 74 · raw

@-A:Data -> @-op:(@_:A -> @_:A -> A) -> @-comm:(@x:A -> @y:A -> {op(x, y) == op(y, x) : A}) -> @+a:A -> @+b:A -> @+c:A -> {op(op(a, b), c) == op(c, op(b, a)) : A}

Three-way commutation from commutativity alone.

law nat_add_left_comm provedsource · line 119 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}

Nat addition is left-commutative (the same statement as MNat.add_left_comm).

law nat_add_right_comm provedsource · line 129 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}

Nat addition is right-commutative (the same statement as MNat.add_right_comm).

law nat_add_four provedsource · line 139 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}

Nat addition's middle-four interchange (the same statement as MNat.add_add_add_comm).

law nat_mul_left_comm provedsource · line 150 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}

Nat multiplication is left-commutative (the same statement as MNat.mul_left_comm).

law nat_mul_right_comm provedsource · line 160 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.mul(Nat.mul(a, b), c) == Nat.mul(Nat.mul(a, c), b) : Nat}

Nat multiplication is right-commutative (the same statement as MNat.mul_right_comm).

law nat_mul_four provedsource · line 170 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) : Nat}

Nat multiplication's middle-four interchange (the same statement as MNat.mul_mul_mul_comm).

law bool_and_left_comm provedsource · line 181 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.and(a, Bool.and(b, c)) == Bool.and(b, Bool.and(a, c)) : Bool}

Bool and is left-commutative.

law bool_and_right_comm provedsource · line 191 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.and(Bool.and(a, b), c) == Bool.and(Bool.and(a, c), b) : Bool}

Bool and is right-commutative.

law bool_or_left_comm provedsource · line 201 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.or(a, Bool.or(b, c)) == Bool.or(b, Bool.or(a, c)) : Bool}

Bool or is left-commutative.

law bool_or_right_comm provedsource · line 211 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.or(Bool.or(a, b), c) == Bool.or(Bool.or(a, c), b) : Bool}

Bool or is right-commutative.

law list_nat_append_assoc4 provedsource · line 221 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+c:List<&2, Nat> -> @+d:List<&2, Nat> -> {List.append(&2, Nat, List.append(&2, Nat, List.append(&2, Nat, a, b), c), d) == List.append(&2, Nat, a, List.append(&2, Nat, b, List.append(&2, Nat, c, d))) : List<&2, Nat>}

Four-way reassociation for List append over Nat.

law foldl_op_eq_foldr_op provedsource · line 240 · raw

@-B:Data -> @-op:(@_:B -> @_:B -> B) -> @-assoc:(@x:B -> @y:B -> @z:B -> {op(op(x, y), z) == op(x, op(y, z)) : B}) -> @-comm:(@x:B -> @y:B -> {op(x, y) == op(y, x) : B}) -> @-z:B -> @-id:(@x:B -> {op(z, x) == x : B}) -> @+xs:List<&2, B> -> {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}

Folding left equals folding right for an associative, commutative operation with a left identity (foldl_eq_foldr needs no identity).

law foldl_eq_foldr provedsource · line 273 · raw

@-B:Data -> @-op:(@_:B -> @_:B -> B) -> @-assoc:(@x:B -> @y:B -> @z:B -> {op(op(x, y), z) == op(x, op(y, z)) : B}) -> @-comm:(@x:B -> @y:B -> {op(x, y) == op(y, x) : B}) -> @+z:B -> @+xs:List<&2, B> -> {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}

Folding left equals folding right for an associative, commutative operation (Mathlib's List.foldl_eq_foldr).

law op_assoc4_sym provedsource · line 288 · raw

@-A:Data -> @-op:(@_:A -> @_:A -> A) -> @-assoc:(@x:A -> @y:A -> @z:A -> {op(op(x, y), z) == op(x, op(y, z)) : A}) -> @+a:A -> @+b:A -> @+c:A -> @+d:A -> {op(a, op(b, op(c, d))) == op(op(op(a, b), c), d) : A}

Four-way reassociation from associativity alone, reversed to rewrite toward the simple side.

law op_left_comm_sym provedsource · line 302 · raw

@-A:Data -> @-op:(@_:A -> @_:A -> A) -> @-assoc:(@x:A -> @y:A -> @z:A -> {op(op(x, y), z) == op(x, op(y, z)) : A}) -> @-comm:(@x:A -> @y:A -> {op(x, y) == op(y, x) : A}) -> @+a:A -> @+b:A -> @+c:A -> {op(b, op(a, c)) == op(a, op(b, c)) : A}

Left commutation from associativity and commutativity, reversed to rewrite toward the simple side.

law op_right_comm_sym provedsource · line 316 · raw

@-A:Data -> @-op:(@_:A -> @_:A -> A) -> @-assoc:(@x:A -> @y:A -> @z:A -> {op(op(x, y), z) == op(x, op(y, z)) : A}) -> @-comm:(@x:A -> @y:A -> {op(x, y) == op(y, x) : A}) -> @+a:A -> @+b:A -> @+c:A -> {op(op(a, c), b) == op(op(a, b), c) : A}

Right commutation from associativity and commutativity, reversed to rewrite toward the simple side.

law op_four_sym provedsource · line 330 · raw

@-A:Data -> @-op:(@_:A -> @_:A -> A) -> @-assoc:(@x:A -> @y:A -> @z:A -> {op(op(x, y), z) == op(x, op(y, z)) : A}) -> @-comm:(@x:A -> @y:A -> {op(x, y) == op(y, x) : A}) -> @+a:A -> @+b:A -> @+c:A -> @+d:A -> {op(op(a, c), op(b, d)) == op(op(a, b), op(c, d)) : A}

Middle-four interchange from associativity and commutativity, reversed to rewrite toward the simple side.

law op_comm3_sym provedsource · line 345 · raw

@-A:Data -> @-op:(@_:A -> @_:A -> A) -> @-comm:(@x:A -> @y:A -> {op(x, y) == op(y, x) : A}) -> @+a:A -> @+b:A -> @+c:A -> {op(c, op(b, a)) == op(op(a, b), c) : A}

Three-way commutation from commutativity alone, reversed to rewrite toward the simple side.

law nat_add_left_comm_sym provedsource · line 358 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}

Nat addition is left-commutative (the same statement as MNat.add_left_comm), reversed to rewrite toward the simple side.

law nat_add_right_comm_sym provedsource · line 368 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}

Nat addition is right-commutative (the same statement as MNat.add_right_comm), reversed to rewrite toward the simple side.

law nat_add_four_sym provedsource · line 378 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}

Nat 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_sym provedsource · line 389 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.mul(b, Nat.mul(a, c)) == Nat.mul(a, Nat.mul(b, c)) : Nat}

Nat multiplication is left-commutative (the same statement as MNat.mul_left_comm), reversed to rewrite toward the simple side.

law nat_mul_right_comm_sym provedsource · line 399 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.mul(Nat.mul(a, c), b) == Nat.mul(Nat.mul(a, b), c) : Nat}

Nat multiplication is right-commutative (the same statement as MNat.mul_right_comm), reversed to rewrite toward the simple side.

law nat_mul_four_sym provedsource · line 409 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> {Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) == Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) : Nat}

Nat 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_sym provedsource · line 420 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.and(b, Bool.and(a, c)) == Bool.and(a, Bool.and(b, c)) : Bool}

Bool and is left-commutative, reversed to rewrite toward the simple side.

law bool_and_right_comm_sym provedsource · line 430 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.and(Bool.and(a, c), b) == Bool.and(Bool.and(a, b), c) : Bool}

Bool and is right-commutative, reversed to rewrite toward the simple side.

law bool_or_left_comm_sym provedsource · line 440 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.or(b, Bool.or(a, c)) == Bool.or(a, Bool.or(b, c)) : Bool}

Bool or is left-commutative, reversed to rewrite toward the simple side.

law bool_or_right_comm_sym provedsource · line 450 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.or(Bool.or(a, c), b) == Bool.or(Bool.or(a, b), c) : Bool}

Bool or is right-commutative, reversed to rewrite toward the simple side.

law list_nat_append_assoc4_sym provedsource · line 460 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+c:List<&2, Nat> -> @+d:List<&2, Nat> -> {List.append(&2, Nat, a, List.append(&2, Nat, b, List.append(&2, Nat, c, d))) == List.append(&2, Nat, List.append(&2, Nat, List.append(&2, Nat, a, b), c), d) : List<&2, Nat>}

Four-way reassociation for List append over Nat, reversed to rewrite toward the simple side.

law foldl_op_eq_foldr_op_sym provedsource · line 471 · raw

@-B:Data -> @-op:(@_:B -> @_:B -> B) -> @-assoc:(@x:B -> @y:B -> @z:B -> {op(op(x, y), z) == op(x, op(y, z)) : B}) -> @-comm:(@x:B -> @y:B -> {op(x, y) == op(y, x) : B}) -> @-z:B -> @-id:(@x:B -> {op(z, x) == x : B}) -> @+xs:List<&2, B> -> {List.foldr(&2, B, B, op, xs, z) == List.foldl(&2, B, B, op, xs, z) : B}

Folding 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_sym provedsource · line 485 · raw

@-B:Data -> @-op:(@_:B -> @_:B -> B) -> @-assoc:(@x:B -> @y:B -> @z:B -> {op(op(x, y), z) == op(x, op(y, z)) : B}) -> @-comm:(@x:B -> @y:B -> {op(x, y) == op(y, x) : B}) -> @+z:B -> @+xs:List<&2, B> -> {List.foldr(&2, B, B, op, xs, z) == List.foldl(&2, B, B, op, xs, z) : B}

Folding left equals folding right for an associative, commutative operation (Mathlib's List.foldl_eq_foldr), reversed to rewrite toward the simple side.

Definitions

def internal_nat_add_assoc source · line 88 · raw

@x:Nat -> @y:Nat -> @z:Nat -> {Nat.add(Nat.add(x, y), z) == Nat.add(x, Nat.add(y, z)) : Nat}

def internal_nat_add_comm source · line 91 · raw

@x:Nat -> @y:Nat -> {Nat.add(x, y) == Nat.add(y, x) : Nat}

def internal_nat_mul source · line 94 · raw

@x:Nat -> @y:Nat -> Nat

def internal_nat_mul_assoc source · line 97 · raw

@x:Nat -> @y:Nat -> @z:Nat -> {Nat.mul(Nat.mul(x, y), z) == Nat.mul(x, Nat.mul(y, z)) : Nat}

def internal_nat_mul_comm source · line 100 · raw

@x:Nat -> @y:Nat -> {Nat.mul(x, y) == Nat.mul(y, x) : Nat}

def internal_bool_and_assoc source · line 103 · raw

@x:Bool -> @y:Bool -> @z:Bool -> {Bool.and(Bool.and(x, y), z) == Bool.and(x, Bool.and(y, z)) : Bool}

def internal_bool_and_comm source · line 106 · raw

@x:Bool -> @y:Bool -> {Bool.and(x, y) == Bool.and(y, x) : Bool}

def internal_bool_or_assoc source · line 109 · raw

@x:Bool -> @y:Bool -> @z:Bool -> {Bool.or(Bool.or(x, y), z) == Bool.or(x, Bool.or(y, z)) : Bool}

def internal_bool_or_comm source · line 112 · raw

@x:Bool -> @y:Bool -> {Bool.or(x, y) == Bool.or(y, x) : Bool}

def internal_list_nat_append_assoc source · line 115 · raw

@x:List<&2, Nat> -> @y:List<&2, Nat> -> @z:List<&2, Nat> -> {List.append(&2, Nat, List.append(&2, Nat, x, y), z) == List.append(&2, Nat, x, List.append(&2, Nat, y, z)) : List<&2, Nat>}

Templates

template internal_foldl_foldr source · line 231 · raw

@-B:Data -> @-op:(@_:B -> @_:B -> B) -> @-assoc:(@x:B -> @y:B -> @z:B -> {op(op(x, y), z) == op(x, op(y, z)) : B}) -> @-comm:(@x:B -> @y:B -> {op(x, y) == op(y, x) : B}) -> @-z:B -> @-id:(@x:B -> {op(z, x) == x : B}) -> @+xs:List<&2, B> -> @+acc:B -> {List.foldl(&2, B, B, op, xs, acc) == op(acc, List.foldr(&2, B, B, op, xs, z)) : B}

template internal_foldl_assoc source · line 254 · raw

@-B:Data -> @-op:(@_:B -> @_:B -> B) -> @-assoc:(@x:B -> @y:B -> @z:B -> {op(op(x, y), z) == op(x, op(y, z)) : B}) -> @+xs:List<&2, B> -> @+a:B -> @+b:B -> {List.foldl(&2, B, B, op, xs, op(a, b)) == op(a, List.foldl(&2, B, B, op, xs, b)) : B}

template internal_foldl_eq_foldr source · line 262 · raw

@-B:Data -> @-op:(@_:B -> @_:B -> B) -> @-assoc:(@x:B -> @y:B -> @z:B -> {op(op(x, y), z) == op(x, op(y, z)) : B}) -> @-comm:(@x:B -> @y:B -> {op(x, y) == op(y, x) : B}) -> @+z:B -> @+xs:List<&2, B> -> {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}