law foldl_eq_foldr_sym

bend-mathlib@0.8.1.0 · algebra.bend:491

import Base

491# Folding left equals folding right for an associative, commutative operation (Mathlib's List.foldl_eq_foldr), reversed to rewrite toward the simple side.
492law foldl_eq_foldr_sym:
493  for ~B: Data
494  for ~op: B -> B -> B
495  for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
496  for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
497  for +z: B
498  for +xs: List<&2, B>
499  {List.foldr(&2, B, B, op, xs, z) == List.foldl(&2, B, B, op, xs, z) : B}