def bc_eq_sym

bendtorch@1.3.0.0 · PROOF.bend:915

import Base
import bendtorch@1.3.0.0/tensor.bend as TT

915# axis by axis: the same on each axis (bc_dim_sym), and by induction on the rest; shapes of different ranks are False
916# either way round
917def bc_eq_sym(a: List<&2, Nat>, b: List<&2, Nat>, o: List<&2, Nat>) -> {TT.bc_eq(a, b, o) == TT.bc_eq(b, a, o) : Bool}:
918  match a b o:
919    case Nil{} Nil{} Nil{}:
920      {==}
921    case Nil{} Nil{} Con{z, ro}:
922      {==}
923    case Nil{} Con{y, rb} Nil{}:
924      {==}
925    case Nil{} Con{y, rb} Con{z, ro}:
926      {==}
927    case Con{x, ra} Nil{} Nil{}:
928      {==}
929    case Con{x, ra} Nil{} Con{z, ro}:
930      {==}
931    case Con{x, ra} Con{y, rb} Nil{}:
932      {==}
933    case Con{+x, +ra} Con{+y, +rb} Con{+z, +ro}:
934      and_cong(TT.bc_dim(x, y, z), TT.bc_dim(y, x, z), TT.bc_eq(ra, rb, ro), TT.bc_eq(rb, ra, ro), bc_dim_sym(x, y, z), bc_eq_sym(ra, rb, ro))