~/bend-docscommunity

main.bend checks

raw source on the hub · import bend-ml-nat-lemmas@0.1.1.0/main.bend as Main

bend-ml-nat-lemmas: Nat and List lemmas, proved, that Bend's Base does not have.

import bend-ml-nat-lemmas@0.1.1.0/main.bend as NL NL.add_comm(a, b) NL.mul_assoc(a, b, c) NL.product_append(xs, ys) ...

Each law states a fact; the def right below it is the proof, checked by the kernel. How to read a proof: it is a function whose TYPE is the statement. - match does case analysis (the number is 0, or it is 1 + p). - A call to the function itself is the induction hypothesis ("I already know it holds for p, so I prove it for 1 + p"). - %e : P rewrites the goal using the equality e. - {==} closes the goal when both sides already compute to the same thing. A parameter carries + when the proof uses it more than once.

1 import
import Base

Laws

law add_zero proved

Also proved in bend-mathlib as nat.add_zero: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.add_zero.

source · line 27 · raw

@a:Nat -> {Nat.add(a, 0n) == a : Nat}

law add_succ provedsource · line 41 · raw

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

law add_comm proved

Also proved in bend-mathlib as nat.add_comm: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.add_comm.

source · line 55 · raw

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

law add_assoc provedsource · line 71 · raw

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

law mul_zero proved

Also proved in bend-mathlib as nat.mul_zero: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.mul_zero.

source · line 86 · raw

@a:Nat -> {Nat.mul(a, 0n) == 0n : Nat}

law mul_succ provedsource · line 109 · raw

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

law mul_comm proved

Also proved in bend-mathlib as nat.mul_comm: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.mul_comm.

source · line 124 · raw

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

law mul_dist provedsource · line 140 · raw

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

law mul_assoc provedsource · line 156 · raw

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

law mul_one_l proved

Also proved in bend-mathlib as nat.one_mul: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.one_mul.

source · line 173 · raw

@+a:Nat -> {Nat.mul(1n, a) == a : Nat}

law mul_one_r proved

Also proved in bend-mathlib as nat.mul_one: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.mul_one.

source · line 182 · raw

@+a:Nat -> {Nat.mul(a, 1n) == a : Nat}

law append_nil provedsource · line 195 · raw

@-A:Data -> @xs:List<&2, A> -> {List.append(&2, A, xs, []) == xs : List<&2, A>}

law append_assoc provedsource · line 209 · raw

@-A:Data -> @xs:List<&2, A> -> @ys:List<&2, A> -> @zs:List<&2, A> -> {List.append(&2, A, List.append(&2, A, xs, ys), zs) == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}

law length_append provedsource · line 225 · raw

@-A:Data -> @xs:List<&2, A> -> @ys:List<&2, A> -> {List.length(&2, A, List.append(&2, A, xs, ys)) == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat}

law product_append provedsource · line 240 · raw

@+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> {product(List.append(&2, Nat, xs, ys)) == Nat.mul(product(xs), product(ys)) : Nat}

Definitions

def product source · line 19 · raw

@xs:List<&2, Nat> -> Nat

Product of the elements of a list of Nat; the empty list is 1. It is the "number of elements" of a tensor whose shape is the list.

def add_swap source · line 100 · raw

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

x + (y + z) == y + (x + z): swaps the middle terms of a triple sum. (Auxiliary lemma; not a published law.)