~/bend-docscommunity

proofs/crypto/sha/list_proofs.bend checks

raw source on the hub · import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/list_proofs.bend as List_proofs

1 import
import Base

Laws

law append_assoc provedsource · line 3 · 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 reverse_twice provedsource · line 20 · raw

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

law reverse_append provedsource · line 35 · raw

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

law add_succ proved

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

source · line 45 · raw

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

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

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

law append_assoc_reverse provedsource · line 70 · raw

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

law add_swap proved

Also proved in bend-mathlib as algebra.nat_add_left_comm: import bend-mathlib@0.7.2.0/algebra.bend as Algebra, then Algebra.nat_add_left_comm.

source · line 82 · raw

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