law foldl_op_eq_foldr_op_sym

bend-mathlib@0.8.1.0 · algebra.bend:477

import Base

477# Folding left equals folding right for an associative, commutative operation with a left identity (foldl_eq_foldr needs no identity), reversed to rewrite toward the simple side.
478law foldl_op_eq_foldr_op_sym:
479  for ~B: Data
480  for ~op: B -> B -> B
481  for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
482  for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
483  for ~z: B
484  for ~id: @x: B -> {op(z, x) == x : B}
485  for +xs: List<&2, B>
486  {List.foldr(&2, B, B, op, xs, z) == List.foldl(&2, B, B, op, xs, z) : B}