def internal_foldl_foldr
bend-mathlib@0.8.1.0 · algebra.bend:234
import bend-mathlib@0.8.1.0/algebra.bend as Algebra
import Base
234def internal_foldl_foldr(~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}:
235 match xs:
236 case Nil{}:
237 Equal.sym(B, op(acc, z), acc, Equal.trans(B, op(acc, z), op(z, acc), acc, comm(acc, z), id(acc)))
238 case +h <> +t:
239 %Equal.sym(B, List.foldl(&2, B, B, op, t, op(acc, h)), op(op(acc, h), List.foldr(&2, B, B, op, t, z)), internal_foldl_foldr(~B, ~op, ~assoc, ~comm, ~z, ~id, t, op(acc, h))) : {_ == op(acc, op(h, List.foldr(&2, B, B, op, t, z))) : B}
240 assoc(acc, h, List.foldr(&2, B, B, op, t, z))