~/bend-docscommunity

proofs/crypto/hash/lists.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/lists.bend as Lists

1 import
import Base

Laws

law append_nil provedsource · line 5 · raw

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

law append_assoc provedsource · line 17 · raw

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

law append_assoc_rev provedsource · line 32 · raw

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

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 42 · raw

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

law add_assoc proved

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

source · line 54 · raw

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

law length_append provedsource · line 68 · raw

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

law add_length provedsource · line 82 · raw

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

n + |xs| + |ys| == n + |xs ++ ys|