law foldl_op_eq_foldr_op

bend-mathlib@0.8.1.0 · algebra.bend:242

import Base

242# Folding left equals folding right for an associative, commutative operation with a left identity (foldl_eq_foldr needs no identity).
243law foldl_op_eq_foldr_op:
244  for ~B: Data
245  for ~op: B -> B -> B
246  for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
247  for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
248  for ~z: B
249  for ~id: @x: B -> {op(z, x) == x : B}
250  for +xs: List<&2, B>
251  {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}